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.

Does the formal statement say what was claimed?

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

declares divergences from its source reviewed by its authors only

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

Checks

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

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

Get an email when this problem moves

A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.

Discussion and bounties for this problem load here.

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