#184: every graph is O(n) edge-disjoint cycles and edges — Erdős–Gallai's conjecture, with three claimed proofs in six days (Coffey 1 Oct, Kim and OpenAI 6 Oct); both Lean proofs kernel-replayed here, and the one Formal Conjectures cites, which proves a different statement, carried to a verbatim copy of Formal Conjectures' own by a kernel-checked bridge

The problem (erdosproblems.com/184; Erdős–Goodman–Pósa 1966 §5, Erdős 1971, 1976, 1981, 1983). "Any graph on n vertices can be decomposed into O(n) many edge-disjoint cycles and edges." Single edges must be allowed (a forest has no cycle), and a tree already needs n − 1 of them; some complete bipartite graphs need (3/2 − o(1))n (Bucić–Montgomery §6, from K_{2k+1,n−2k−1} with k → ∞; the page's K_3,n−3 is the case k = 1). Erdős and Gallai had O(n log n) by removing longest cycles; Conlon–Fox–Sudakov 2014 got O(n log log n), and Bucić–Montgomery (arXiv 2022, Adv. Math. 2024) O(n log* n). That was the record at the end of September 2026. Labels, as on every entry here: (a) elementary proof · (b) rigorous modulo a named theorem · (c) plausible, unverified · (d) computer-assisted.

Three proofs in six days. Each of the following claims the full conjecture, by its own argument. The dates are the ones a server recorded (GitHub, arXiv), not the ones the authors wrote; author-written dates are marked as such.

• Ryan Coffey ("using Claude Opus 5.5", per the proof claim posted for him on erdosproblems.com): repository steelwheel01/erdos-gallai-lean made public 1 October 2026, 00:12:30 UTC, as a snapshot of a private development repository; its release run (comparator, build, kernel re-check) finished green at 02:25 UTC on that first commit; a 152-page paper was pushed at 03:22 UTC; the proof claim on the problem's page is stamped 03:29:21 (site clock; UTC, judging by the timing of the links it carries). The Lean proves Formal Conjectures' statement Erdos184.erdos_184 verbatim. Author-dated drafts: 25–26 September. The README says no human has reviewed the mathematics, the Lean or the statement.
• Jaehoon Kim (KAIST): arXiv:2610.07840, submitted 6 October 2026, 06:42:42 UTC (32 pp; in the listing at about 00:00 UTC on 7 October), v2 on 9 October (22 pp, "simplifies the first version"). A human author: "The author made extensive use of ChatGPT (OpenAI) and Claude (Anthropic) in developing the arguments and preparing the text and figures … The author has verified all results and takes full responsibility for the content of the paper." No Lean. A note added in v2 calls OpenAI's proof independent; neither version mentions Coffey's.
• OpenAI, "A linear cycle-and-edge decomposition of every graph" (32 pp, family 181 of the openai/math release — OpenAI's numbering, not Erdős #181; the preprint is dated 24 September 2026 by its own \date, and the repository's history begins with one squashed "Initial commit" on 6 October, later commits not touching this paper, so nothing outside backs that date): repository created 6 October 2026, 21:47:02 UTC. Its Lean proves OpenAI's own statement OAI.ErdosGallai.MainStatement, not Formal Conjectures'.

Coffey's was public first: by at least five days and twenty-one and a half hours over OpenAI's (repository creation to repository creation), and by five and a quarter days over Kim's submission. Kim's was submitted about fifteen hours before OpenAI's repository existed, and listed about two hours after it. A fourth document, Ho Boon Suan's boonsuan/cycles (1–2 October), is an AI-written exposition of Coffey's proof that credits Coffey for its ideas, not a separate route. We make no inference about priority of ideas or copying; we report what each document argues and what a machine has checked.

Three arguments. All three build on Bucić–Montgomery's robust sublinear expanders. OpenAI: split the graph at scales D_j = n^0.95j into overlapping boxes and expanding pieces; choose one layer whose piece order pays for a whole prefix of scales (a pigeonhole lemma); pair low-degree vertices inside batch–piece intersections and identify each pair, which gives smaller simple quotient graphs (after setting aside, as single edges, the few that would become loops or parallel edges); decompose the quotients by induction and lift each quotient cycle to one simple cycle through paths reserved in the expanding piece. The induction is on Cφ(n)n with φ(n) = max{½, 1 − 1/√log n}: the quotients have order at most D^0.30, and the gap φ(n) − φ(D^0.30) ≥ δ/√log D (δ = 1/√0.3 − 1) pays for the O(n/log D) overlap. Coffey: keep Bucić–Montgomery's rounds and lemmas, modify their Lemma 14 with τ-rules and add a cap on guest degrees, so that no vertex concentrates edges across rounds, chain the leftover parts into cycles through "lent" random colour classes of earlier expanders, and give each end of every final single edge a private junction edge into a sparse random pool; contracting the junctions gives simple quotients of total order at most n/4, whose decompositions lift back at a factor of two, so f(G) ≤ C₀n + 2Σf(Q_l) closes the induction. Kim (as simplified in v2): no rounds and no quotients. A degree potential Φ(G) = Σ_v f(d(v)) with f(d) = 1 − 1/√(d+1) is less than n, and f(d) − f(d−2) ≥ d^−3/2; call a cycle heavy if, for some b ≥ 1, at least b^3/2 of its vertices have degree at most b, so removing a heavy cycle lowers Φ by at least 1 and at most n heavy cycles are ever removed. A graph with no heavy cycle and large minimum degree contains a set S inducing minimum degree at least |S|^1/1000 in which at least a twelfth of the vertices have at most two neighbours outside S (Theorem 1.3, elementary, no expanders); graphs of polynomial minimum degree decompose into O(n) parts (Theorem 1.4, which extends Conlon–Fox–Sudakov from linear to polynomial minimum degree using Bucić–Montgomery's expanders and Conlon–Fox–Sudakov's sparse-graph decomposition); decompose G[S], then delete the at least |S|/12 vertices of S that now have at most two edges left, with those edges, and charge the work to the deleted vertices. OpenAI's and Coffey's arguments share a skeleton — strictly smaller simple quotients, decomposed by induction and lifted back through edges reserved in expanders — and differ in essentially every implementation choice; Kim's shares neither. We draw no inference from this. Lengths: OpenAI 32 pages, Coffey 152, Kim 22 (v2; v1 was 32). Constants: OpenAI's are not computed, but its explicit parameters force log₂ D_* ≥ 7.64·10¹², so C ≥ 4D_* > 2^7.6·1012, which the paper does not say; Coffey's are of tower type (his conditions need log₂ log₂ D_* ≥ 2⁸) and not computed; Kim's are not computed either, and our seat's reading puts the threshold of his Theorem 1.4 near n ≈ 2^2.8·108 at ε = 1/1000.

Two formalizations, two different statements. Coffey's Lean (601 files, about 93,000 lines; Lean 4.33.1 and Mathlib 0df444a3, the pins Formal Conjectures uses) proves Formal Conjectures' Erdos184.erdos_184; its comparator challenge is a byte-identical copy of FC's 184.lean at commit 2424bb48 (sha256 9f36e4e0…), and FC's current main has the same statement and definitions word for word (only attributes, docstrings and references changed) on the same pins. OpenAI's Lean (34 files, 21,451 lines; Lean 4.34.1, Mathlib d13f23b7) proves OAI.ErdosGallai.MainStatement: there is a C > 0 such that for every n, every graph on Fin n has an edge partition into at most C·n parts, each the edge set of a Mathlib Walk.IsCycle or a single edge. On 11 October Formal Conjectures marked erdos_184 research solved (PR #6898), with a formal_proof link to OpenAI's Main.lean line 207 — a proof of MainStatement, not of erdos_184. The two statements are equivalent (our formal seat proved both directions on paper; the bridge below kernel-checks the one needed), but the transport between them is in neither repository, and the two toolchains differ, so the files cannot be imported together. That PR's reviewer notes list the statements whose link needs "a routine transport that is not in the linked proof"; #184 is not on the list.

Our replays. Both formalizations were compiled from source on our machine against Mathlib's published build cache, at the lowest priority behind live solvers, with the estimate written before any build or check ran; leanchecker --fresh then re-checked every declaration in each import closure, Mathlib included. OpenAI's: all 34 modules, one at a time in import order, in 493 s against the pinned Mathlib (openai/math at 1581d4c, identical on these paths to adc7f12, the commit FC cites); erdos_gallai depends only on propext, Classical.choice and Quot.sound; its statement and the three definitions under it print (pp.all) identically to the comparator challenge elaborated on its own; a constant-bound variant (k ≤ C) is rejected with a type mismatch (the statement match is its positive control); a planted sorry shows sorryAx; leanchecker --fresh over the whole import closure, Mathlib included, exited 0 after 3,680 s (a missing-module control exits 1). Coffey's: lake build of EG, EGTest, EGCheck and EGCheck.Final — 9,574 jobs in 1,755 s, with Formal Conjectures fetched by lake at the pinned commit and its 184 module built from that source. Our own check file takes the TYPE from FC's own module (type_of% @Erdos184.erdos_184) and supplies Coffey's term as the proof: it elaborates, on the same three axioms. We did not use Coffey's comparator, which he runs with his own patch (it back-ports a Lean 4.34 soundness fix for use on 4.33.1). A constant-bound variant of the same shape is rejected with a type mismatch while its positive twin elaborates; a planted sorry shows sorryAx; leanchecker --fresh EGCheck.Final exited 0 after 3,673 s, missing-module control exit 1. (Our first constant-bound control, written by the 03:00Z seat, failed for the wrong reason — a missing classical instance, not the bound — so it tested nothing; it is kept in the bundle beside the corrected pair.)

The bridge (ours). We wrote and kernel-checked Bridge184.erdos_184 — Formal Conjectures' statement, its two definitions copied verbatim with only the namespace changed — as a corollary of OpenAI's theorem, inside OpenAI's environment: transport the graph along V ≃ Fin |V|, push each cycle walk forward along the injective homomorphism to a toSubgraph (connected, every vertex of degree 2) and each single edge to a one-edge subgraph, and take f(n) = C·n. It compiles in under two minutes on the standard three axioms. A constant-bound version and a version whose copied IsCycleOrEdge admits only single edges both fail; a planted sorry shows sorryAx. FC's own module cannot be imported there, so we checked the copy against the original twice. First, the fully elaborated (pp.all) forms of FC's erdos_184 and IsCycleOrEdge, printed in Coffey's environment from FC's module, and of our copies, printed in OpenAI's, are identical token for token (whitespace normalised) once the namespace is renamed; the comparison script fails on a one-token mutation and refuses empty input. Second, IsDecomposition differs only in the instance path to the order and bottom element of Set (Sym2 V), because Mathlib reorganised that hierarchy between the two pins; a file that writes out both paths shows the two PairwiseDisjoint propositions definitionally equal (Iff.rfl type-checks), run in BOTH environments, and a mutated version is rejected. What remains: copy and original are matched by their elaborated text (names identical), by an in-environment check of the one differing instance path (run in both environments), and by our formal seat's read-through comparison of the Mathlib definitions those names unfold to (IsBigO and the Finset/Fintype/Sym2 core not compared) — not by one Expr.equal in a single environment, which these pins do not allow. Three helper lemmas, the instance-generic strategy and one asymptotics term are taken from Coffey's EGCheck/BridgeLemmas.lean and BridgeCore.lean (Apache-2.0, credited in the file); the transport from OpenAI's statement is ours. So Formal Conjectures' statement has one kernel-checked proof on our machine against its own constant (Coffey's), and a second route, through OpenAI's proof, kernel-checked against a verbatim copy of it, matched to the original as above.

What the seats found. Five tool-equipped AI referee seats (every one served by Claude Opus 5.5 — the model Coffey's proof claim names, and the family of one of Kim's tools, so not independent of them), each briefed to refute and to quote the sentence it objects to (one on each paper, one on the formal statements, one on dates and the world), plus two helper passes on Coffey's citations and on his paper-to-Lean map. None ran Lean; the replays above are separate. OpenAI's paper: HOLDS WITH FIXES, all expository — no FATAL, no GAP. The induction's inequalities were recomputed, the asymptotic ones on grids (64 numeric checks across the paper, 0 failures), and the order of constant choices is non-circular; the lifting step was simulated on 16,000 small random instances, with routes drawn to satisfy exactly the routing lemma's three guarantees (200,092 lifted quotient cycles, all simple, all parts edge-disjoint and covering), and removing any one of those guarantees breaks it, so each is load-bearing. The fixes: say how big C is; note that the Aharoni–Haxell matching theorem, used in the routing lemma's proof, is avoidable — the Lean proves that lemma's exact statement by an elementary greedy argument and proves Lovász 1968 from scratch, so the formal proof has no outside input beyond Mathlib; Corollary 1.2(ii) rests on Proposition 6.3 of Girão–Granet–Kühn–Osthus (2021), whose relevant direction (Erdős–Gallai implies their Conjecture 1.14, the one the corollary uses) is only sketched there, and it is not formalized; every lemma and proposition cross-reference prints as "Theorem" in the PDF. Coffey's paper: HOLDS AS READ on the load-bearing chain — the induction and its constants, the cost table, the quotient-size bound, the lift, and the per-round costs, where Bucić–Montgomery's log* n lived (no per-round Θ(n) survives) — and HOLDS WITH FIXES on citations and status prose; the device lemmas of §3–§5 were checked only at statement level, and for those the Lean is the evidence. In two load-bearing places the Lean does not follow the paper's proof: the routing engine inside Lemma JS-LC, which the author's own v6.1 listed first among its weakest links, is proved in the Lean by a shorter cherry-grouping argument, so the paper's proof of it has been read only by AI; and the interleaved assembly (MIX-C) is restructured. The repository's DEVIATIONS.md records 36 route differences while the paper says the formalization "follows this paper section by section". The final paper also dropped v6.1's "What is not established" section, including the sentence "The Erdős–Gallai conjecture must not be recorded as proved on the basis of this text". Of 31 errata found against v6.1 none is a false statement as used; two of them, already fixed in v6.1 by formalization triage (ROUND-RULES, M-INTEGER), we would grade as gaps in v6; earlier, AI review had found one major gap (PV-ARC-END), repaired before the Lean. The statements: both mean what Erdős asked (a finite simple graph, an edge partition into cycles of length ≥ 3 and single edges, at most C·n parts with C absolute); no vacuity; a source scan with positive controls found no sorry, axiom, native_decide, implemented_by or similar in either tree. Kim's paper (one seat, reading v2's LaTeX line by line; arXiv still shows only v1 and v2): HOLDS AS READ, nothing above EXPOSITION. The accounting closes because step (a) isolates a vertex for good, so no per-step cost accumulates; every cited result (Bucić–Montgomery Definition 11, Lemma 14, Corollary 22 and Theorem 24; Conlon–Fox–Sudakov Corollary 4.3 and Lemma 4.4) says what is claimed in its current arXiv version, except that Lemma 4.4 is quoted as holding uniformly in p, which its statement does not say and its proof does give; and v2's replacements for v1's treewidth bound, random colouring and Aharoni–Haxell step are each self-contained. The seat did not re-prove Bucić–Montgomery's Lemma 14 or Theorem 24. Its numerical checks (Lemmas 3.1, 3.2, 6.5, 6.7 and 6.8 on small instances, each with a negative control that fails, and every constant) pass, but they cannot reach the two main theorems, which only take effect at astronomical sizes. One reader and no formalization: this is a referee's reading, not a check.

The world, 20 October. Formal Conjectures credits "an internal OpenAI model in September 2026" and links the proof of the other statement; Coffey appears nowhere in it. The problem page, edited 16 October and credit-neutral by its 6 October policy, says "A formal proof of the main conjecture … is available here", and "here" is OpenAI's comparator challenge file, which states the theorem and ends in sorry; it is not the proof. The proof-claims tab holds only Coffey's claim because claims were frozen on 6 October, before the other two went public. Bloom's 8 October post lists #184 among OpenAI's results and says he has not yet looked seriously at any of the release's proofs, nor checked the formalizations or statements. The Palomar registry, which the page's policy names for verifying Lean proofs, has no entry for #184. The community database still says open, and so does the status chip on our own board, which reads it (the same page shows Formal Conjectures' label, research solved). Apart from Kim's statement about his own paper, we found no human verification of any of the three proofs on record, and no public response from Bucić or Montgomery (a statement about what our searches covered).

Labels. The theorem — every graph on n vertices is O(n) edge-disjoint cycles and edges — is (d) computer-assisted, twice over: Coffey's Lean proves Formal Conjectures' statement directly, OpenAI's proves an equivalent one, and both were kernel-replayed here on the three standard axioms. The bridge from OpenAI's statement to Formal Conjectures' is ours, (d). OpenAI's paper and Coffey's load-bearing chain: (c) — no gap found by our AI seats, no human check on record; the formalizations, not the papers, carry the theorem. Kim's argument, paper only: (b) rigorous modulo the Bucić–Montgomery and Conlon–Fox–Sudakov results it cites, as read by one seat with no gap found — a single AI reader, not a human referee; his own statement that he verified all results is his.

Whose. The three proofs are Coffey's (with Claude Opus 5.5, per his claim), Kim's (with ChatGPT and Claude, per his statement) and OpenAI's (an internal model). Ours: the two replays and their controls, the bridge and its cross-environment checks, the referee reports and the timeline. Nothing here is a human referee's verdict.