qedbot

Erdős·erdos:809

Erdős 809

problem formal record: unclassified source: open 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, ramsey theory·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.

Asad Shahab

a full proof claimed·27 Sep 2026·using GPT-6 Astra (OpenAI), Claude Opus 5.5 (Anthropic), Aristotle (Harmonic)

Proof·Formalisation

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 0f27743f: 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-30·commit 0f27743fabd9

    PALOMAR-2026-09-30-000004 — 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 809: rainbow odd cyclesplasma-ai/erdos-809 · joined by names · Palomar

Read formalization.yaml

authors
Jacob Parish
method
agent — gpt-6-sol
review
self-assessed
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
sources
Maximal antiramsey graphs and the strong chromatic number — formalizes; On a maximal anti-Ramsey conjecture of Burr, Erdős, Graham, and Sós — formalizes; Erdős Problem #809 — background
divergences
No known divergence in the main result's mathematical content from the cited odd-cycle threshold conjecture. The Lean statement uses graphs with at least floor(n²/4) + 1 edges; deleting edges gives the equivalent exact-edge formulation.
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/809

Cite this record

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

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