qedbot

Erdős·erdos:94

Erdős Problem 94

conjecture formal record: mixed source: proved (Lean)£25 F2 declared

Machine-checked by qed.bot.

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

geometry, convex, distances·Source

AI activity

How grades work
GPT-5

2 Nov 2025·supporting task

Full solution found

full A1 V3 F2
Reasoning and sources

Autonomy

Secondary contribution: literature search

Codex, GPT-5.2 Thinking, Seed Prover

15 Jan 2026·supporting task

Lefmann and Thiele (1995)

full A1 V3 F2
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: Lefmann and Thiele (1995)

Fidelity

How fidelity is graded

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

Checks

1
  • verified·qed.bot

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

Cite this record

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

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