Independent machine-checked reproduction of 141 Lean formalisations of Erdos problem resolutions, with disclosed trusted bases

We independently recompiled 141 Lean 4 artifacts formalising resolutions of Erdos problems, in a stated toolchain, with warnings escalated to errors so that an incomplete proof is a hard failure, and recorded for each artifact the complete axiom closure of its results. All 141 reproduce and none contained an incomplete proof: 132 depend only on the three standard kernel axioms, 9 depend on additional axioms which we enumerate, and 9 are self-declared partial formalisations recorded as such. 151,633 lines and 8,429 declarations were checked in 55.6 minutes of compute.

A reproduction here means exactly one thing: on our machine, in a stated toolchain, the artifact elaborates and typechecks with no incomplete proof, and these are the axioms its results rest on. It does NOT claim the informal mathematics is correct, that the formal statement faithfully captures the problem it is labelled with, or that any author's account of their process is accurate. Statement fidelity is the more important question and this study does not address it.

The main contribution is methodological. 15 artifacts failed on the first pass and ALL 15 were faults in our own environment rather than defects in the artifacts: every one failed in under four seconds, during import resolution, before any proof-checking began, because our environment had the main mathematical library prebuilt but not the projects' own supporting libraries. One failure was caused by our own probe, which required a dependency that an artifact with no imports at all did not provide. After building the dependency closure, all 15 reproduced. Reported as-is, that first pass would have produced 15 false non-reproductions against named researchers. We therefore propose a rule: a failure fast enough to precede elaboration is an environment fault until proven otherwise; build the dependency closure before judging any artifact; and treat a false non-reproduction as exactly as damaging as a false verdict.

We also compared each artifact's machine-derived axiom dependencies against its authors' own declared assumptions, where declared. Six match exactly. One artifact OVER-declares, listing an assumed theorem that is in fact proved within the same project, so its result is stronger than its own header claims. One declares two conditions where the kernel shows a single bundled axiom. One carries a non-kernel axiom without a status header, though its author recorded the axiom name in a source comment. The correct reading is that this corpus is unusually honest and that independent recomputation adds precision to already-honest declarations. We recommend machine-derived axiom-closure checking as routine practice for formalisation repositories.

METHOD. Each artifact was compiled with `lake env lean -DwarningAsError=true`. This is load-bearing rather than hygienic: in Lean an incomplete proof is a warning, so a stubbed proof exits successfully without the flag, and every result here would be void if it were dropped. A probe appended to each file enumerates that file's own declarations rather than the roughly 200,000 imported library constants, computes the axiom closure of each via the compiler's own axiom collector, and reports the union together with any declaration depending on the incomplete-proof axiom. This yields a whole-file guarantee rather than covering only those declarations an author chose to print. Results were written to disk per artifact as each completed. Only artifacts declaring the same toolchain as the build tree were attempted; a second cohort of 56 declaring an older toolchain was excluded rather than failed, since a version mismatch is not a defect in the artifact.

This report names no individuals by design.