Subjects

Mathematical logic

6 results from OpenAI’s math release. 6 explained so far. OpenAI has published Lean proofs for 6: 5 of the main theorem, 1 of part of the claim.

See these in the full list, with search and filters.

• 240 Shelah's eventual categoricity and the prescribed-threshold obstruction

  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.

  2 papers ▶Episode, 5:05 OpenAI published a Lean proof of part of the claim.

• 241 Rigidity of the Turing degrees

  Every order automorphism of the Turing degrees is the identity, resolving their rigidity problem. Thus no nontrivial relabeling of degrees preserves the ordering by relative computability.

  ▶Episode, 4:35 OpenAI published a Lean proof of the main theorem.

• 242 Single-fold Diophantine representations and undecidability under an at-most-one-solution promise

  Every recursively enumerable set of tuples of natural numbers has a Diophantine representation with exactly one auxiliary solution for each member and none for nonmembers. This proves the single-fold conjecture and hence the finite-fold conjecture. Diophantine solvability over the nonnegative integers remains undecidable even with an at-most-one-solution promise.

  ▶Episode, 4:12 OpenAI published a Lean proof of the main theorem.

• 243 Separating choiceless counting from polynomial time and witnessed choice

  Confirms the Blass–Gurevich–Shelah noncapture conjecture: consistency of a linear system over 𝔽₃ defines a polynomial-time query on unordered finite structures that choiceless polynomial time with counting cannot express. A separate result shows that adding witnessed symmetric choice strictly increases expressive power. Both separations hold for the full counting formalism, allowing hereditarily finite sets of arbitrary finite rank.

  2 papers ▶Episode, 4:32 OpenAI published a Lean proof of the main theorem.

• 244 The Partition Principle does not imply Choice

  Assuming ZF is consistent, constructs a model in which every surjective image of a set injects into that set, yet the axiom of choice fails. Choice for ordinal-indexed families still holds. From any countable transitive model of ZFC, a separate construction gives a transitive symmetric extension with these properties and no new countable sequences of ground-model elements.

  ▶Episode, 4:16 OpenAI published a Lean proof of the main theorem.

• 245 Weak normalization implies strong normalization in pure type systems

  Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts.

  ▶Episode, 4:22 OpenAI published a Lean proof of the main theorem.

Summary and paper titles from OpenAI’s catalog, used under the Apache License 2.0. Last checked October 19, 2026.