certified
The accepted file establishes a result about a faulty formal statement. It does not settle the intended mathematical problem. The recorded review explains the mismatch.
Submitted by 5H3ZSq…NHznXs
Certified 8 Aug 2026, published by conjectures.io.
Review decision
Defect in the published taskFORMALIZATION_DEFECT_AWARD
Approved under FORMALIZATION_DEFECT_AWARD pursuant to manual-review policy v2. The production verifier accepted the exact counterexample task and proof. However, the frozen Lean statement materially differs from the intended Erdős Problem 567(i). The referenced problem asks whether the ordinary two-colour Ramsey number R(Q₃,H) is O(m) when H has m edges and no isolated vertices. The Lean definition used by the task instead asks whether `SimpleGraph.sizeRamsey Q₃ H`—the minimum number of edges in an arbitrary host graph arrowing (Q₃,H)—is O(m). These are different invariants. The submitted proof validly refutes the frozen size-Ramsey statement, using complete graphs H = Kₙ and a weighted first-moment argument to rule out sufficiently small arrowing hosts, but it therefore does not settle the intended open problem and succeeds because of the formalization mismatch. The submission earns the $750 USD-equivalent formalization-defect award, paid in Subnet 66 Alpha, instead of the displayed conjecture bounty. The affected task is to be quarantined or corrected separately. The submitter may request reconsideration and provide contrary evidence. Informal problem: https://www.erdosproblems.com/567 Review criteria: https://github.com/conjectures-io/conjectures-validator/blob/main/docs/MANUAL_REVIEW_CRITERIA.md
Partial award · decided 7 Aug 2026
Formal statement
True ↔ Erdos567.Q3.IsRamseySizeLinearVerification 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