# AlphaProof miniF2F on Lean 4.26

## Source lock

- `google-deepmind/miniF2F`:
  `f0a20e14c1eeccd859d51bb4c2b3ee487889c303`
- `google-deepmind/formal-conjectures` tag `v4.26.0`:
  annotated tag object `d9688f52ac268192db13556e3f8cd5f53872fb2d`,
  peeled commit `84450b941eee69d63d9e5f27e626fc58de767d75`
- Mathlib tag `v4.26.0`:
  `2df2f0150c275ad53cb3c90f7c98ec15a56a1a67`
- Lean tag `v4.26.0`:
  `d8204c9fd894f91bbb2cdfec5912ec8196fd8562`

## Upstream project port

No benchmark source file changes are required. Apply only the package pins:

```diff
--- a/lean-toolchain
+++ b/lean-toolchain
@@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.26.0
```

```diff
--- a/lakefile.lean
+++ b/lakefile.lean
@@
-require "google-deepmind" / "formal_conjectures"
+require "google-deepmind" / "formal_conjectures" @ git "v4.26.0"
```

Then regenerate the dependency lock and build:

```bash
lake update
lake exe cache get
lake build
```

The verification run completed all 7,750 Lake jobs and built
`MiniF2F.ProblemImports`, `MiniF2F.Test`, and `MiniF2F.Valid` successfully.

## Dataset build

The builder requires a Lean 4.26 Mathlib checkout and a matching built
`leanprover/repl` binary. Example:

```bash
python port/build_dataset.py \
  --source-dir /path/to/google-deepmind-miniF2F \
  --formal-conjectures-dir /path/to/formal-conjectures-v4.26.0 \
  --mathlib-dir /path/to/mathlib4-v4.26.0 \
  --repl-bin /path/to/repl-v4.26.0 \
  --output-dir /path/to/dataset-output
```

The build fails closed unless:

- source, Lean, Mathlib, and Formal Conjectures commits match the manifest pins;
- each split contains exactly 244 unique canonical theorem names;
- split names are disjoint;
- exact AlphaProof source and Hub runtime forms both elaborate;
- all 488 paired goal states are byte-identical;
- every UUID matches `sha256(canonical(goal_state))[:16]`;
- Parquet round-trip preserves the exact three-column schema and row counts.

The twelve excluded validation variants and both output shard hashes are listed
in the root `manifest.json`.