qedbot

Erdős·erdos:647

Erdős Problem 647

conjecture formal record: mixed source: verifiable£25 F1 unaudited

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

A Palomar registration names this problem. It is shown below but not counted as a check of the claim.

Fidelity F1: A formal artifact exists, but nothing records that its statement says what the claim says.

number theory·Source

AI activity

How grades work
ChatGPT Deep research, DeepSeek DeepThink, Gemini

2026-01-28

Incorrect proof found

incorrect A3 autonomous V1 write-up F1 unaudited
Reasoning and sources

Autonomy

AI standalone; human involvement recorded as non-significant

Does the formal statement say what was claimed?

F1 unaudited A formal artifact exists, but nothing records that its statement says what the claim says.

a thin wrapper around another repository

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 776a5817: Comparator confirmed 1 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

    project registered at a pinned commit·2026-09-04·commit 776a5817bffc

    PALOMAR-2026-09-04-000003 — names this problem; not counted as a check of the claim

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.

A kernel-checked exclusion certificate for Erdős Problem 647, to 10^8ibrahimmian36/palomar-decanus · joined by names · Palomar

Read formalization.yaml

authors
Ibrahim Mian, Shayaan Siddique
method
manual
review
other — internal
sources
A Kernel-Checked Exclusion Certificate for Erdős Problem 647 — formalizes; Erdős Problem 647 — formalizes; Formal Conjectures: ErdosProblems/647 — background; Erdős problem 647: certificate data and verification artifacts — background
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Recorded elsewhere

Compare the registries
  • palomar — A kernel-checked exclusion certificate for Erdős Problem 647, to 10^8

    checked·their labels: registered

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