# QEDGen Generated Proofs

This directory contains Lean 4 proof artifacts generated by [QEDGen](https://qedgen.dev), Mistral's proof engineering model.

## Files

- **Best.lean** - The selected proof candidate
- **prompt.txt** - The original verification prompt
- **metadata.json** - Generation metadata (timing, tokens, rankings)
- **attempts/** - All completion attempts for comparison
- **validation/** - Optional local build logs when generation was run with `--validate`
- **lean_solana/** - Local Lean support library used by generated proofs

## Verifying the Proofs

### Prerequisites

Install [Lean 4](https://leanprover.github.io/lean4/doc/setup.html):

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
```

### Build and Verify

```bash
# Build the best proof
lake build Best

# Or build everything
lake build
```

If the build succeeds with no errors, the proof is formally verified!

## Notes

- The first `mathlib` build is slow. On a typical laptop, expect roughly 15 to 45 minutes.
- Zero `sorry` markers do not guarantee the file elaborates. Lean compilation is the real check.
- If Lake reports that `.lake/packages/mathlib` cannot resolve `HEAD`, remove `.lake/packages/mathlib` and rerun `lake build`.

### Checking for Incomplete Proofs

Search for `sorry` markers (incomplete proof steps):

```bash
grep -r "sorry" Best.lean attempts/
```

A proof with zero `sorry` markers is a useful signal, but not a substitute for `lake build`.

## Generated by

Generated by [qedgen-solana-skills](https://github.com/qedgen/solana-skills)
