Erdős·erdos:355

Erdős Problem 355

problem formal record: solved source: proved (Lean) 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 statement corpus cites this proof against its own statement.

number theory, unit fractions·Source

AI activity

Aristotle, Gemini 3

13 Mar 2026·supporting task

van Doorn and Kovač (2025) (almost the entirety)

full A1 V1 F2

Reasoning and sources

Secondary contribution: formalization

proof to formalize: van Doorn and Kovač (2025) (almost the entirety)

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

Follow this problem

An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.

Discussion and bounties for this problem load here.

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

Formal statements · 1

FormalConjectures/ErdosProblems/355.lean
1 declarations, 1 unproved goals·research solved

Cited proofs · 1

Woett/Lean-files/blob/main/ErdosProblem355.lean
139 theorems, 0 unproved goals, 0 declared axioms

Also known as · 3

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

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

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