qedbot

Erdős·erdos:126

Erdős Problem 126

conjecture formal record: mixed source: proved (Lean)$250 F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through an alignment table and written divergences.

number theory·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

2

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

JohnVictor36

a full proof claimed·4 Sep 2026·using communication with AI, giving the essential steps, asking AI for a detail implementation·1 comment there

Formalisation

candidateA? V0

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős problem #126: prooftadamcz/erdos126 · joined by anchor · no independent check

Read formalization.yaml

method
autonomous — GPT-6 Astra (pre-release version, OpenAI)
review
other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the benchmark harness and again in this repository's ci; preliminary informal reading of the argument by thomas f. bloom; no independent refereeing (Thomas F. Bloom)
sorry
0 unproved goals declared
sources
Proof of Erdős problem #126: If f(n) is the least number of distinct primes dividing ∏_{a≠b∈A}(a+b) over n-element sets A ⊆ ℕ, then f(n)/log n → ∞. — other; Erdős problem #126 (erdosproblems.com) — background; On a Problem in the Elementary Theory of Numbers — background; FrontierMath Erdős — background
related
google-deepmind/formal-conjectures/blob/488aade228ec37880b8fec178c173c07d279bb53/FormalConjectures/ErdosProblems/126.lean — builds-on; epoch-research/LeanOpenProblems/blob/77882c437ca1dfefab3b27fa00f1d29788100311/apn/data/erdos/Isolated/Erdos126.erdos_126.lean — builds-on
divergences
The compared theorem is exactly the Formal Conjectures statement. The definition `IsMaximalAddFactorsCard f` says that for every `n`, `f n` is the greatest `m` such that every `n`-element `A : Finset ℕ` has at least `m` distinct prime factors in `∏_{(a,b) ∈ A.offDiag} (a + b)` (product over ordered pairs `a ≠ b`; the same prime set as over unordered pairs). Such an `f` exists and is unique (the primary resolution verifies existence, uniqueness and monotonicity in its `Independent126` section), so the hypothesis is not vacuous; `A` may contain `0`, which changes `|S(A)|` by at most one relative to positive sets. The conclusion `Tendsto (fun n => f n / Real.log n) atTop atTop` coerces `f n` to `ℝ`; `Real.log n` is positive for `n ≥ 2`. The stronger polynomial bounds proved internally are not part of the compared statement.
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 1
Also known as · 3
  • https://www.erdosproblems.com/126
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/126.lean
  • FormalConjectures/ErdosProblems/126.lean

Cite this record

qed.bot, “Erdős Problem 126”, https://qed.bot/s/erdos-126, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.