Shelah's eventual categoricity conjecture
From OpenAI Aftermath
Shelah's eventual categoricity conjecture asserts that, for abstract elementary classes, categoricity in one sufficiently large cardinal implies categoricity in every sufficiently large cardinal, above a threshold that depends only on a bound for the Löwenheim–Skolem number. Two manuscripts dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim a proof of the conjecture in ZFC and, under the continuum hypothesis, a counterexample to a proposed specific threshold. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Morley's theorem is the first-order prototype: a countable first-order theory categorical in one uncountable cardinal is categorical in every uncountable cardinal. Shelah introduced abstract elementary classes, which keep a coherent notion of strong substructure and closure under unions of chains without a first-order axiomatization, and formulated the eventual categoricity conjecture for them. A prescribed-threshold form asks for the specific bound h(LS(K)), where h(κ) = ℶ(2κ)+.
- Special cases were known: Makkai and Shelah for infinitary theories when a strongly compact cardinal exists; Grossberg and VanDieren for tame classes with amalgamation, joint embedding and arbitrarily large models; Boney for all classes with a successor starting cardinal, assuming a proper class of strongly compact cardinals; Vasey for universal classes in ZFC and for tame classes with primes; Shelah and Vasey for excellent classes in ZFC, with broader results under strongly compact cardinals or a weak form of the generalized continuum hypothesis.
- C. Espíndola has announced a proof of eventual categoricity for arbitrary abstract elementary classes (arXiv:1906.09169) and a transfer at the prescribed threshold, Theorem 4.1 of arXiv:2301.13167. The manuscripts describe these as separate public claims from which they import nothing.
The original results
- Claim (eventual categoricity). Theorem 1.1 of Eventual categoricity for abstract elementary classes states that for every infinite cardinal λ there is a cardinal μ(λ) ≥ λ such that every abstract elementary class K with LS(K) ≤ λ that is categorical in some κ ≥ μ(λ) is categorical in every κ′ ≥ μ(λ). No amalgamation, joint embedding, tameness or no-maximal-models hypothesis is assumed, and the starting cardinal may be a successor, a regular limit or a singular cardinal. The threshold is shown to exist; no numerical bound is given. The manuscript notes that one threshold μ(ℵ0) then serves for all sentences of Lω1,ω in countable languages.
- Claim (CH obstruction). Theorem 1.1 of A CH obstruction to a prescribed categoricity threshold states that, under the continuum hypothesis, there is an abstract elementary class K in a countable finitary relational language with LS(K) = ℵ0 that has two nonisomorphic models of cardinality ℶω2 = h(ℵ0) but is categorical in every cardinal at least ℶ(2ℵ1)+. Categoricity therefore does not transfer down to the prescribed threshold, and, if ZFC is consistent, the prescribed-threshold form is not provable in ZFC. The class is categorical on a higher tail, which is consistent with the first claim. The manuscript states that its conclusion is the opposite of Espíndola's Theorem 4.1, and its last section describes an obstruction to the canonical-point step of that proof.
- Sources (openai/math repository, commit
1581d4c): Eventual categoricity for abstract elementary classes and A CH obstruction to a prescribed categoricity threshold. - Formalization, as described by the repository. The scope note states that the formalized result is the CH obstruction, with no amalgamation, joint embedding, tameness or no-maximal-models assumption, and that the canonical-point obstruction and the eventual categoricity theorem are not included. The Comparator statement is
CHObstruction.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 27 October 2026) |
|---|---|---|---|---|
| 2026-10-07 to 2026-10-17 | Exchange on X between A. Chernikov, J. Rute and C. Espíndola (thread; Espíndola's reply), collected in the notes of the community revision mathcommunity/oai-math-revised, issue 31 | Remark (status of earlier work) | On Espíndola's earlier claimed proof of eventual categoricity, which the first manuscript cites as a separate claim: Chernikov writes that, to his understanding, it is not currently accepted by the small community working on abstract elementary classes. Espíndola replies that this community has no topos theorists, that two people who understand topos theory have agreed to serve as external reviewers of his habilitation thesis, and that his papers are being formalized in Lean. Rute asks whether only the obstruction, and not the main theorem, has a Lean formalization. | Public exchange, as recorded by the community revision. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, fidelity table at commit 227b04a, 19 October 2026) |
Review (fidelity of the formal statement) | Rates the family "partial": only the CH obstruction is formalized and the headline eventual categoricity theorem is not stated in Lean. It notes that abstract elementary classes are defined for the purpose, following the standard axioms, and lists these definitions among those to check. Records a sandboxed Comparator pass for CHObstruction. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the CHObstruction solution, in 109 seconds. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists no entry for CHObstruction, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_164 of the eventual categoricity manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap in a partial audit of the manuscript of about 9,500 lines. Sections 1–4, 6, 10 and 14 and parts of Sections 9 and 11–13 were read closely; Sections 5, 7 and 8 and parts of Sections 11 and 12 were skimmed or not read, and several sampled steps rely on them as black boxes. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-17 | C. Espíndola, reply on X, collected in the notes of the community revision, issue 30 | Critique (author of the disputed earlier claim) | Espíndola writes that the CH manuscript's Proposition 7.2, on models in a categoricity cardinal not factoring through the double-negation subtopos, contradicts one of his results in the explicit-thresholds paper. He also writes that he has identified errors that should invalidate its claims even with a Lean certification: in his reading, Proposition 5.7 rests on a bound from Lemma 5.2 for a smaller cardinal, so the two nonisomorphic models could occur only below the prescribed threshold. | Public dispute, unresolved as of 27 October 2026. |
| 2026-10-25 | Espíndola's objections to A CH obstruction to a prescribed categoricity threshold: an AI-only investigation, a document added to the notes of the community revision (pull request 42) | Review (AI-generated) | Reports on the two objections and proofreads Espíndola's Theorem 4.1 with GPT-6 Astra and Claude Opus 5.5 instances. Its judge report states that Proposition 5.7 asserts a different bound from the one attributed to it in the objection, that the endpoint models come from a separate construction, and that it found no gap there. It reports a Comparator acceptance of the Lean statement, which it finds matches Theorem 1.1. It states that the two theorems have incompatible conclusions under CH, that Proposition 7.2 gives an obstruction on the original category, and that its bearing on the modified category mentioned in Espíndola's reply is unresolved. | The document states that it is not a verdict, that it has not been checked by any person and that its mathematical conclusions may be wrong; the maintainers write that an expert is needed. |
Notes
- The background is recounted from the introductions of the two manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
