∑math20

Mathematical logic · Result 240

Shelah's eventual categoricity and the prescribed-threshold obstruction

2 papersLean

Proves Shelah's eventual categoricity conjecture in ZFC: for each bound on the Löwenheim–Skolem number, a uniform threshold makes categoricity of an abstract elementary class in one cardinal above that threshold imply categoricity throughout the same tail. Categoricity means uniqueness up to isomorphism at a given cardinality. Under the continuum hypothesis, a proposed specific Hanf threshold need not suffice.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 2

First page of A CH obstruction to a prescribed categoricity threshold

A CH obstruction to a prescribed categoricity threshold

OpenAI · September 24, 2026

Assuming the continuum hypothesis, we construct an abstract elementary class with Löwenheim–Skolem number ℵ0 that is categorical in every sufficiently large cardinal but has at least two nonisomorphic models of cardinality \(\beth_{\omega_2}\). Thus categoricity does not transfer down to the proposed bound \(\beth_{(2^{\aleph_0})^+}\), which equals \(\beth_{\omega_2}\) under CH. Consequently, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC.

Read PDF Download Source

Cite
@misc{OAI:A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026,
  author = {{OpenAI}},
  title = {{A CH obstruction to a prescribed categoricity threshold}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf}{OAI:A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026}},
  year = {2026}
}
First page of Eventual categoricity for abstract elementary classes

Eventual categoricity for abstract elementary classes

OpenAI · September 24, 2026

We prove Shelah's eventual categoricity conjecture for abstract elementary classes in ZFC. For each infinite bound on the Löwenheim–Skolem number there is a uniform threshold such that categoricity in any one cardinal at or above that threshold implies categoricity in every cardinal at or above the same threshold.

Read PDF Download Source

Cite
@misc{OAI:Eventual-Categoricity-for-Abstract-Elementary-Classes-September-24-2026,
  author = {{OpenAI}},
  title = {{Eventual categoricity for abstract elementary classes}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Eventual-Categoricity-for-Abstract-Elementary-Classes-September-24-2026/paper.pdf}{OAI:Eventual-Categoricity-for-Abstract-Elementary-Classes-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Under the continuum hypothesis, the formalized result refutes the proposed transfer of categoricity down to the Hanf threshold. It gives an abstract elementary class in a countable relational language, with Löwenheim–Skolem number \(\aleph_0\), that has two nonisomorphic models at \(\beth_{\omega_2}=h(\aleph_0)\) but is categorical in every cardinal at least \(\beth_{(2^{\aleph_1})^+}\).

No amalgamation, joint embedding, tameness, or absence-of-maximal-models assumption is imposed. The later canonical-point obstruction and the separate eventual-categoricity theorem are not included.

Comparator links

ResultComparator statement
CH categoricity-threshold obstructionCHObstruction.lean

Scope note on GitHub →