qedbot

Erdős·erdos:689

Erdős Problem 689

conjecture formal record: open source: open F3 anchored

Machine-checked by Palomar.

Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

number theory·Source

AI activity

How grades work
Codex, GPT-5.2, GPT-5.5 Pro

29 Oct 2025·with Boris Alexeev, Przemek Chojecki, Dogmachine, jleng01, Mehtaab Sawhney, Terence Tao, Malek Zribi

Candidate full solution

candidate A1 V3 F3
Reasoning and sources

Autonomy

AI collaborating with humans

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

F3 anchored. The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

Anchored to google-deepmind/formal-conjectures/blob/f19cf7f60d9bc650ff58462f540e236caf3a6a67/FormalConjectures/ErdosProblems/689.lean

reviewed by an agent

Checks

1
  • verified·Palomar

    Registered by Palomar at 54f27258: Comparator confirmed 1 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel

    project registered at a pinned commit·2026-09-20·commit 54f272582dd7

    PALOMAR-2026-09-20-000002

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős 689: eventual double covering by prime residue classeslinrock/math-proofs/erdos-689 · joined by anchor · Palomar

Read formalization.yaml

authors
Linmiao Xu
method
agent
review
agent-reviewed
results
1 main results named, checked with Comparator
sources
Some unconventional problems in number theory (1979), p. 79 — other; A greedy matching proof of Erdős’s two-fold residue-class problem (working manuscript, 27 April 2026) — formalizes; Erdős problem 689 discussion — background
related
google-deepmind/formal-conjectures/blob/f19cf7f60d9bc650ff58462f540e236caf3a6a67/FormalConjectures/ErdosProblems/689.lean — other; antoshashakov/Principia-Math-Solutions/tree/c9910942522fbd3a07c034ac57947f56df6f0f6d/erdos1054 — builds-on
checked by
Palomar

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 · 2
Cited proofs · 0

No proof artifact cited by the formal record.

Recorded elsewhere

Compare the registries
  • palomar — Erdős 689: eventual double covering by prime residue classes

    checked·their labels: registered

Also known as · 5
  • https://www.erdosproblems.com/689
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/689.lean
  • FormalConjectures/ErdosProblems/689.lean
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/45.lean
  • FormalConjectures/GreensOpenProblems/45.lean

Cite this record

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

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