qedbot

Erdős·erdos:649

Erdős Problem 649

conjecture formal record: mixed source: disproved (Lean) F2 declared

Checked, not verified. 1 independent check 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

How grades work
Aristotle, GPT

1 Jun 2026·supporting task

Tong; Sampaio

full A1 V1 F2
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: Tong; Sampaio

Fidelity

How fidelity is graded

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

Checks

1
  • not self-contained·qed.bot

    imports project modules: ErdosProblems.Erdos368b

    proof rebuilt and axioms inspected·2026-08-21

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/649
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/649.lean
  • FormalConjectures/ErdosProblems/649.lean

Cite this record

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

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