A giant number search becomes checkable proof
- What it is
- A Lean 4 formalization claims to exclude a bounded class of repeating odd-period schedules that cover every integer.
- Who did it
- Ibrahim Mian and Shayaan Siddique
- What it could mean
- A computer search can say ‘nothing works.’ This work aims to turn that verdict into a replayable proof: no qualifying odd-period cover with combined period at most 10,000—not the whole conjecture.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of (ℤ) Has lcm Exceeding 10000 ↗See the proposed checks
Clean pinned Lean replay, axiom closure, source-to-Lean statement correspondence, and verification of the finite Chinese-remainder certificates; highest risk is scope correspondence, especially that the formal statement matches the intended covering-system exclusion.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- Lean 4 kernel formalization of the finite exclusion (operatornamelcm>10000) for odd distinct-modulus covers, with 63 public theorems and stated no-sorry/no-nativedecide trust boundary.
- Why this could matter
- A giant number search becomes checkable proof Imagine covering every integer with repeating schedules that use distinct odd periods. The grand puzzle remains open, but this work machine-checks that no such system can have a combined period of 10,000 or less—a milestone for reviewable computational proof.
- If it holds up
- Methods: it demonstrates one reproducible route from search-generated certificates to Lean-kernel theorems for this bounded exclusion; broader reuse needs separate evidence.
- If it does not
- A scope or trust-base mismatch would show why compiled code is not enough and protect later searches from inheriting a false foundation.
- Impact horizon
- Methods · Formal proof · Number theory · Verified computation
- Version
- submitted 2026-07-28 12:10:26 UTC.
- Why we tracked it
- a high-value formal-proof artifact, though the authors state that its mathematical exclusion is known and its advance is epistemic/formal.
- Highest-risk dependency
- scope correspondence, especially that the formal statement matches the intended covering-system exclusion.
- Available artifacts
- The paper links Lean sources, certificates, and CI on GitHub; no current social signal used.
- Current boundary
- Intake record only; examination not started.