Erdős·erdos:74
Erdős Problem 74
No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.
Fidelity F2: The correspondence is declared through an alignment table and written divergences.
graph theory, chromatic number, cycles·Source
AI activity
How grades workNo AI contribution recorded against this statement.
Claimed on erdosproblems.com
1Proof 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.
Fidelity
How fidelity is gradedF2 declared. The correspondence is declared through an alignment table and written divergences.
Declared by the projects
1As each project's formalization.yaml states it.
Erdős problem #74: disproof
- method
- autonomous — GPT-6 Astra (pre-release version, OpenAI)
- review
- other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the benchmark harness and again in this repository's ci; preliminary informal reading of the argument by thomas f. bloom; no independent refereeing (Thomas F. Bloom)
- sorry
- 0 unproved goals declared
- sources
- Disproof of Erdős problem #74: Some f(n) → ∞ forces every graph whose n-vertex subgraphs are within f(n) edges of bipartite to have finite chromatic number. — other; Erdős problem #74 (erdosproblems.com) — background; On almost bipartite large chromatic graphs — background; FrontierMath Erdős — background
- related
- google-deepmind/formal-conjectures/blob/488aade228ec37880b8fec178c173c07d279bb53/FormalConjectures/ErdosProblems/74.lean — builds-on; epoch-research/LeanOpenProblems/blob/77882c437ca1dfefab3b27fa00f1d29788100311/apn/data/erdos/Isolated/Erdos74.erdos_74.lean — builds-on
- divergences
- The compared theorem is exactly the negation of the Formal Conjectures statement. Points a reader should be aware of: (1) `f : ℕ → ℕ` is integer-valued and `Tendsto f atTop atTop` is the formal sense of `f(n) → ∞`; (2) the graph ranges over `SimpleGraph V` for a vertex type `V` in an arbitrary universe `u`, and the theorem is universe-polymorphic; (3) `maxSubgraphEdgeDistToBipartite G n` is the supremum over *all* (not only induced) `n`-vertex subgraphs of the minimum number of edge deletions making the subgraph bipartite — since edge deletion distance is monotone in the edge set, this agrees with the maximum over induced subgraphs; it uses `sSup` on `ℕ`, which is `0` for the empty set (graphs with fewer than `n` vertices), and `sInf`, whose argument set is always nonempty; (4) `G.chromaticNumber = ⊤` is Mathlib's formalisation of infinite chromatic number. The formal statement asserts only existence of some `f → ∞`; the Lean proofs construct explicit budgets but no growth rate is advertised.
- checked by
- nobody independent of its authors yet
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themFormal material
Formal statements · 1
Also known as · 3
- https://www.erdosproblems.com/74
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/74.lean
- FormalConjectures/ErdosProblems/74.lean
Cite this record
qed.bot, “Erdős Problem 74”, https://qed.bot/s/erdos-74, as of 30 Sep 2026.