qedbot

Erdős·erdos:689

Erdős Problem 689

conjecture formal record: open source: openno 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

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

Candidate full solution

candidate A1 collaborative V3 checked F3 anchored
Reasoning and sources

Autonomy

AI collaborating with humans

Does the formal statement say what was claimed?

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

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

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

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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.

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