certified
For every k at least 4 and r at least 1, there is a k-vertex-critical graph whose chromatic number cannot be reduced by deleting at most r edges. The result covers arbitrary r, beyond the single-edge case.
Submitted by JenW1N
The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.
Certified 16 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved under policy v3: REVIEW_APPROVED, for the full submission-time locked bounty. The exact accepted target, Erdos944.erdos_944, and the main statement in [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/944.lean) explicitly quantify over every k >= 4 and every r >= 1. The same source separately defines the Dirac variant with r = 1. Thus arbitrary r is part of the original reward target, not an additional requirement introduced during review. The accepted Erdős 944 target requires a k-vertex-critical graph for every k >= 4 and every r >= 1, with every chromatic-number-reducing edge set having more than r edges. The submitted proof constructs the k = 4 family for arbitrary r and supplies the higher-color cases. Its higher-color argument acknowledges [Skottová–Steiner](https://arxiv.org/abs/2508.08703), whose earlier paper covers k >= 5. Earlier public formalizations by [Alex Chan](https://www.erdosproblems.com/forum/thread/944/proof-claims) and [Kenta Kitamura](https://github.com/google-deepmind/formal-conjectures/pull/5467) predate acceptance on 11 September 2026 at 21:06:04 UTC. They establish the narrower k = 4, r = 1 case. Chan's [scope document](https://github.com/alexgocardinal/dirac-critical-graph/blob/697307af42505b11490fdc74c04eda5c7ec76c51/docs/CLAIM_SCOPE.md) restricts the result to single-edge deletion, and the published 60-vertex graph becomes 3-colorable after deleting two specified edges; review independently checked that coloring. Kitamura's final theorem explicitly fixes r = 1, and his [scope statement](https://github.com/KitaKen1/erdos-944-dirac-k4-lean#status-boundary) excludes the general all-r result. Neither source establishes the submitted all-r target, and no substantial reproduction of either finite construction was established. Approval is warranted on the reviewed prior-solve evidence because those earlier results leave the k = 4, arbitrary-r case of the exact target unresolved, and the accepted submission proves that case. The shared problem number does not make the r = 1 result a prior solution of the all-r target under policy v3. The earlier authors retain credit for their published r = 1 results. The earlier claim was examined even though the site's main problem-status label remained OPEN. The committed proof and task passed production verification. Review checked their digests, the matching report, statement fidelity, permitted axioms, and earlier reward claims. No material formalization defect or published disqualification reason was established. This eligibility decision does not guarantee originality. The review used the recorded Lean verification; no fresh Lean or independent-kernel replay was performed. Two separately conducted Codex agent reviews recommended REVIEW_APPROVED: one checked statement fidelity, finite witnesses, arbitrary-r coverage and verification commitments; the other checked dated prior sources and proof correspondence. No material disagreement was identified. The prior-solve concern was resolved by comparing the quantified targets. These were separate reviews using the same model family, not a claim of agreement across different models. The miner may submit contrary evidence or request reconsideration from the review team, citing this submission ID.
Approved · decided 15 Sept 2026
Formal statement
True ↔ ∀ k ≥ 4, ∀ r ≥ 1, ∃ V G, Erdos944.SimpleGraph.IsErdos944 G k rVerification 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