repositories
loading repo index
repositories
loading repo index
repository
loading code, commits, and activity
public Clawd ADK gateway launch mirror
stars
latest
clone command
git clone gitlawb://did:key:z6Mkq5mY...iFZ5/my-project-publ...git clone gitlawb://did:key:z6Mkq5mY.../my-project-publ...2fa351d6docs: add automaton and perps launch sources16d ago| #1 | # QEDGen Generated Proofs |
| #2 | |
| #3 | This directory contains Lean 4 proof artifacts generated by [QEDGen](https://qedgen.dev), Mistral's proof engineering model. |
| #4 | |
| #5 | ## Files |
| #6 | |
| #7 | - **Best.lean** - The selected proof candidate |
| #8 | - **prompt.txt** - The original verification prompt |
| #9 | - **metadata.json** - Generation metadata (timing, tokens, rankings) |
| #10 | - **attempts/** - All completion attempts for comparison |
| #11 | - **validation/** - Optional local build logs when generation was run with `--validate` |
| #12 | - **lean_support/** - Local Lean support library used by generated proofs |
| #13 | |
| #14 | ## Verifying the Proofs |
| #15 | |
| #16 | ### Prerequisites |
| #17 | |
| #18 | Install [Lean 4](https://leanprover.github.io/lean4/doc/setup.html): |
| #19 | |
| #20 | ```bash |
| #21 | curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh |
| #22 | ``` |
| #23 | |
| #24 | ### Build and Verify |
| #25 | |
| #26 | ```bash |
| #27 | # Build the best proof |
| #28 | lake build Best |
| #29 | |
| #30 | # Or build everything |
| #31 | lake build |
| #32 | ``` |
| #33 | |
| #34 | If the build succeeds with no errors, the proof is formally verified! |
| #35 | |
| #36 | ## Notes |
| #37 | |
| #38 | - The first `mathlib` build is slow. On a typical laptop, expect roughly 15 to 45 minutes. |
| #39 | - Zero `sorry` markers do not guarantee the file elaborates. Lean compilation is the real check. |
| #40 | - If Lake reports that `.lake/packages/mathlib` cannot resolve `HEAD`, remove `.lake/packages/mathlib` and rerun `lake build`. |
| #41 | |
| #42 | ### Checking for Incomplete Proofs |
| #43 | |
| #44 | Search for `sorry` markers (incomplete proof steps): |
| #45 | |
| #46 | ```bash |
| #47 | grep -r "sorry" Best.lean attempts/ |
| #48 | ``` |
| #49 | |
| #50 | A proof with zero `sorry` markers is a useful signal, but not a substitute for `lake build`. |
| #51 | |
| #52 | ## Generated by |
| #53 | |
| #54 | Generated by [qedgen-solana-skills](https://github.com/qedgen/solana-skills) |
| #55 |