certified
A Lean-verified submission was approved for this target. Read the recorded review for its precise mathematical scope.
Submitted by EthanYang
Certified 28 Oct 2026, published by conjectures.io.
Solver
EthanYangWho this proof is credited to.
The run
Provenance
Review decision
Approved in reviewREVIEW_APPROVED
APPROVED — REVIEW_APPROVED, policy v4. Accepted 2026-10-24T05:20:16.694610+00:00; production verification completed 2026-10-24T05:22:10.187555+00:00. Erdős problem #1032, counterexample mode: the submitted proof refutes the existence of a fixed ε > 0 with arbitrarily large edge-critical four-chromatic simple graphs of minimum degree at least ε·n; equivalently, every such critical graph on n vertices has minimum degree o(n). The committed statement (FullOldProblems.ErdosCriticalMinimumDegree: chromatic number 4, chromatic number 3 after deleting any single edge, degree as neighbour-set cardinality on Fin n) matches the problem as stated at erdosproblems.com/1032. Production run 60 passed the Lean kernel, Comparator, task-commitment, trusted-hash and permitted-axiom checks (propext, Quot.sound, Classical.choice) under landrun+seccomp; a fresh exact-input replay on 2026-10-25 (108 s) also passed. The argument was read at the lemma level: a bounded-depth branching search in which every branch removes a colour from at least half the minimum degree of neighbour lists, 2-SAT for two-list vertices and unsatisfiable cores with at most two unit clauses yield a non-3-colourable subgraph with O_ε(n) edges; edge-criticality forces that subgraph to be the whole graph, and the degree-sum identity contradicts linear minimum degree for large n. The full locked bounty of 1711.022154144 Alpha applies, subject to acceptance of the required chat logs and normal payout processing. No earlier eligible claimant, material formalization defect or published disqualification reason was established. Prior work considered: the erdosproblems.com entry lists the problem as open (last updated 23 January 2026); the forum thread holds only Lech Mazur's partial bound δ ≤ (3/10+o(1))n (7 May 2026, Lean) building on Luo–Ma–Yang; Simonovits and Toft (1972) give constructions with minimum degree ≫ n^(1/3). None establishes the sublinear conclusion. Three advisory agent assessments from different model families (Codex, 25 October 2026; Claude Fable 5.1 and Claude Opus, 26 October 2026) support approval with no material disagreement. The human reviewer authorized this decision. Review was not a line-by-line audit or an exhaustive priority certification; Nanoda was disabled. Sources: https://www.erdosproblems.com/1032, https://github.com/lechmazur/erdos_1032. The miner may request reconsideration from the Conjectures review team, referencing this submission and contrary evidence.
Approved · decided 26 Oct 2026
Formal statement
FullOldProblems.ErdosCriticalMinimumDegreeVerification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice