certified

Erdős problem 579

Formal result accepted

A Lean-verified submission was approved for this target. Read the recorded review for its precise mathematical scope.

Read Lean proof Download Lean source Verification report Review decision

Submitted by Jordan

Lean verification:: Passed
Conjectures review:: Approved
Reward:: Paid

Certified 6 Oct 2026, published by conjectures.io.

Review decision

Approved in reviewREVIEW_APPROVED

APPROVED — REVIEW_APPROVED, policy v3. Accepted 2026-10-03 18:12:32 UTC; production verification completed 18:19:42 UTC. This submission refutes Erdős Problem 579: for every c>0 and lower bound N, it constructs a finite ordinary K2,2,2-free graph on n>=N vertices with at least (3/2048)n^2 edges and independence number below c*n. The exact committed statement matches the intended conjecture. Production verification and a separate isolated replay passed the Lean kernel, Comparator, task-commitment and permitted-axiom checks under landrun+seccomp. The full locked bounty of 7015.124566494 Alpha applies, subject to normal payout processing. No earlier eligible claimant, material formalization defect, or qualifying disqualification evidence was established. Supporting Boolean-analysis code credits TCSlib and FABL; those sources were not shown to solve the exact target. Two Codex/GPT-6 assessments from separate October 3 and October 6 contexts support approval with no material disagreement; they share evidence and are not blinded or model-diverse. The human reviewer authorized this binding decision. Review covered critical interfaces and bounded prior-work searches, not every auxiliary lemma or an exhaustive novelty audit. Nanoda was disabled. Sources: https://www.erdosproblems.com/579 ; https://real.mtak.hu/110562/1/Erdos1983_Article_MoreResultsOnRamseyTuranTypePr.pdf (p.72); https://ems.press/content/serial-article-files/51716 (Problem C). The miner may request reconsideration from the Conjectures review team, referencing this submission and contrary evidence.

Approved · decided 6 Oct 2026

Formal statement

True ↔
  ∀ (δ : ℝ),
    0 < δ →
      ∃ c,
        0 < c ∧
          ∀ᶠ (n : ℕ) in Filter.atTop,
            ∀ (G : SimpleGraph (Fin n)),
              Erdos579.octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → c * ↑n ≤ ↑G.indepNum

Verification report

Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.

The task it was checked against

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.

The submission and the sandbox

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.

The trusted build

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.

The kernel's verdict

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

Bounty.target

Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice