Erdős·erdos:12

Erdős Problem 12

conjecture formal record: mixed source: openno F2 declared

Checked, not verified. 3 independent checks recorded, with verdict not self-contained. The checks are set out below.

Fidelity F2: The statement corpus cites this proof against its own statement.

number theory·Source

AI activity

DeepMind prover agent

2026-04-07

Partial result (Lean) (solutions to first part and second part)

partial A2 directed V2 artifact F2 declared

Reasoning and sources

AI building on literature supplied to it

literature: 🟡 Erdős and Sárközy (1970)

GPT-5.4 Thinking

2026-04-07·with Nat Sothanaphan, Terence Tao

Partial result

partial A1 collaborative V1 write-up F2 declared

Reasoning and sources

AI collaborating with humans

F2 declared The statement corpus cites this proof against its own statement.

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

not self-contained qed.bot
imports project modules: FormalConjectures.Util.ProblemImports

proof rebuilt and axioms inspected·2026-08-21
not self-contained qed.bot
imports project modules: FormalConjectures.Util.ProblemImports

proof rebuilt and axioms inspected·2026-08-21
not self-contained qed.bot
imports project modules: FormalConjectures.Util.ProblemImports

proof rebuilt and axioms inspected·2026-08-21

Get an email when this problem moves

A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.

Discussion and bounties for this problem load here.

Formal statements · 1

FormalConjectures/ErdosProblems/12.lean
9 declarations, 10 unproved goals·research open, research solved, textbook

Cited proofs · 3

vibemathed — Erdős Problem #12
checked·machine-led·their labels: lean-verified, ai-discovered

Also known as · 3

https://www.erdosproblems.com/12
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/12.lean
FormalConjectures/ErdosProblems/12.lean