Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The bounty site Conjectures.io lists among its certified results
for Problem 726 a 24-line Lean
proof, attacked as a disproof, of the negation of the formal-conjectures
statement Erdos726.erdos_726 as frozen at the catalog commit of
the pinned source.
The solver is pseudonymous on the record (a truncated account key), and
the record is published and attributed by the site, hence the claimant
slug. The site's kernel accepted the proof on 13 August 2026 with the
axioms propext, Quot.sound and Classical.choice (one kernel; the
site's second kernel was not run), and the record was certified on 14
August 2026.
Why it is rejected. The frozen statement filtered the primes by
(p : ℝ) / 2 < (n % p : ℝ), which Lean elaborates as the real-field
remainder (n : ℝ) % (p : ℝ), identically zero in Mathlib, so the formal
sum was the zero function and its asymptotic equivalence to
was trivially false. The proof rewrites the remainder
to zero and contrasts the zero function with a divergent one. It refutes
that degenerate statement and nothing else: the problem's sum takes the
integer residue , as the site's statement says and as the
formal-conjectures file has said since its correction of 11 September 2026
(pull request #5508). The bounty site's own manual review, decided 13
August 2026, says the frozen statement "materially differs" from the
problem and that the proof "does not refute the intended integer-residue
asymptotic"; it approved the record as a formalization-defect award, with
a partial award in place of the bounty, and labels it "Formalization
defect" on the result page. As a claim about Problem 726 it is therefore
rejected by the record that carries it, and the problem's standing is
untouched by it. The record is kept here so that the site's listing of
Problem 726 among its results is not misread.
Depends on. No page of this wiki.