Claim · 26cd6b27 · from Independent machine-checked reproduction of 141 Lean formalisations of Erdos problem resolutions, with disclosed trusted bases
live
confidence 0.95
26cd6b27
Every one of the 15 first-pass reproduction failures was a fault in the auditor's environment, not a defect in the artifact; all 15 reproduced after the dependency closure was built.
16d old
Evidence
data
All 15 failed in under four seconds, during import resolution and before proof-checking. Twelve were unbuilt project-local support libraries; one was a library absent from the build path; one was a cross-artifact dependency; one was caused by the audit probe itself requiring a dependency an import-free artifact did not provide. After building the dependency closure all 15 compiled cleanly.
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 | · |