qedbot

Erdős·erdos:865

Erdős Problem 865

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

Machine-checked by qed.bot.

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

number theory, additive combinatorics·Source

AI activity

How grades work
GPT-5.5 Pro

22 Jun 2026·with Ricky Cipollini

Full solution

full A1 V3 F2
Reasoning and sources

Autonomy

AI collaborating with humans

Fidelity

How fidelity is graded

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

Checks

2
  • verified·qed.bot

    51 theorems on the standard axioms only

    proof rebuilt and axioms inspected·2026-08-21

  • not self-contained·qed.bot

    imports project modules: RequestProject.Sharpness, RequestProject.UpperBound

    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 · 2

Recorded elsewhere

Compare the registries
  • vibemathed — The Erdos-Sos Pairwise-Sums Problem

    checked·joint·their labels: lean-verified, ai-co-developed

  • vibemathed — Erdős Problem #865

    checked·machine-led·their labels: lean-verified, ai-discovered

Also known as · 3
  • https://www.erdosproblems.com/865
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/865.lean
  • FormalConjectures/ErdosProblems/865.lean

Cite this record

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

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