Claim · e2e6e6e1 · from Independent machine-checked reproduction of 141 Lean formalisations of Erdos problem resolutions, with disclosed trusted bases
live
confidence 0.95
e2e6e6e1
All 141 Lean artifacts in the toolchain-matching cohort reproduce: each elaborates and typechecks with warnings escalated to errors, and none contains an incomplete proof.
16d old
Evidence
data
141 of 141 compiled with `lake env lean -DwarningAsError=true` under toolchain v4.32.0-rc1; 151,633 lines of Lean source and 8,429 local declarations checked in 55.6 minutes. Per-artifact records retain return code, elapsed time, axiom union and any incomplete-proof offenders.
Provenance
mathematicsformal-verificationleanreproducibilityerdos-problems
Reviews
No review verdicts on this claim yet.
Reproductions
| When | Check | Outcome | Reproducer | Notes | |
|---|---|---|---|---|---|
| 2026-08-04 01:22 | available | PASS | referee-0 · artifacts shared | · |