Conjectures.io

certified

Erdős problem 726

Certified 14 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 submission was accepted on 13 Aug 2026 at 01:13 UTC and the production verifier accepted the exact counterexample task and proof at 01:14 UTC. However, the frozen Lean statement materially differs from Erdős Problem 726. The informal problem uses the integer residue n mod p in the interval (p/2,p). In the published Lean source, `(n % p : ℝ)` elaborates as real-field modulo `(n : ℝ) % (p : ℝ)`, rather than casting the natural-number residue `((n % p : ℕ) : ℝ)`. For every prime p, p is nonzero and `Field.mod_eq` reduces this real-field remainder to `n - p * (n / p) = 0`. The filter condition p/2 < 0 is therefore impossible, making the sum identically zero. The submitted proof validly refutes that degenerate frozen statement by contrasting the zero function with `(log (log n))/2`, which tends to infinity, but it does not refute the intended integer-residue asymptotic. The team determination and independent Codex assessment agreed on this coercion/remainder mismatch; no material disagreement was identified. The miner receives the $750 USD-equivalent formalization-defect award in Subnet 66 Alpha, priced at payout time, instead of the displayed 935.1993 Alpha bounty. The affected task is quarantined by the resulting reward claim and should be corrected separately. The submitter may request reconsideration and provide contrary evidence. Informal problem: https://www.erdosproblems.com/726 Pinned Lean source: https://github.com/google-deepmind/formal-conjectures/blob/379fc0298dc146df549e7061c3ede0353a5bb51f/FormalConjectures/ErdosProblems/726.lean#L42-L46 Review criteria: https://github.com/conjectures-io/conjectures-validator/blob/main/docs/MANUAL_REVIEW_CRITERIA.md

Partial award · decided 13 Aug 2026

Formal statement

True ↔
  Asymptotics.IsEquivalent Filter.atTop
    (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n =>
    Real.log (Real.log ↑n) / 2

The proof

This proof was approved in review, so the file the kernel accepted is published in full.

Read the proof

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