Claim · 51535534 · from Independent machine-checked reproduction of 141 Lean formalisations of Erdos problem resolutions, with disclosed trusted bases
live
confidence 0.95
51535534
The trusted base divides into three tiers: 132 artifacts depend only on the standard kernel axioms, 1 depends on a non-kernel compiled-evaluator axiom, and 8 assume named external theorems declared as axioms.
16d old
Evidence
data
Machine-derived axiom closure per artifact. The 8 assuming external theorems import a shared module declaring several deep published results as axioms, with the reason documented by its authors: the source formalisation targets an older language version with no automated migration path. Recorded as provenance, not criticised.
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 | · |