qedbot

Erdős·erdos:625

Erdős 625

problem formal record: unclassified source: solved$1000 F2 declared

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 F2: The correspondence is declared through an alignment table and written divergences.

graph theory, chromatic number·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

2

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.

Fayçal Serraj

a full proof claimed·9 Sep 2026·using GPT-5.6 Sol (OpenAI Codex)

Proof

candidateA? V0

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source reviewed by its authors only

Checks

1
  • verified·Palomar

    Registered by Palomar at 9702b5e7: Comparator confirmed 2 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-02·commit 9702b5e73462

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

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős Problem 625: chromatic versus cochromatic number of a random graphSamPetkov/Erdos625-formalization · joined by names · Palomar

Read formalization.yaml

method
agent — OpenAI GPT-5 family
review
self-assessed — self-assessed with independent kernel replay; not peer-reviewed
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
sources
Erdős Problem 625: manuscript and Lean formalization — other, authors participated; Some Problems and Results in Cochromatic Theory — background, authors n/a; The Difference Between the Chromatic and the Cochromatic Number of a Random Graph — background, authors not-contacted
divergences
The formal theorem matches the manuscript's uniform quantitative result. It omits only the stronger nonconstant phase-resolved refinement, as stated explicitly in the scope field.
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 · 0

No formal statement located.

Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 1
  • https://www.erdosproblems.com/625

Cite this record

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

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