qedbot

Erdős·erdos:762

Erdős Problem 762

problem formal record: solved source: disproved (Lean) F2 declared

Machine-checked by qed.bot.

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

graph theory, chromatic number·Source

AI activity

How grades work
Aristotle, Claude Opus 4.7, GPT

3 Jun 2026·supporting task

Steiner (2024)

full A1 V3 F2
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: Steiner (2024)

Fidelity

How fidelity is graded

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

Checks

1
  • verified·qed.bot

    46 theorems on the standard axioms only

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

Cite this record

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

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