Mathematical Logic

Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

$$NPComplete SAT$$

under the decider and reduction hypotheses.

Motivation

A Diophantine representation translates membership in a computably enumerable set into solvability of one polynomial equation. The source asks whether the entire auxiliary witness can always be made unique. The source is OpenAI's September 2026 manuscript.

Setting

A single-fold representation uses an integer polynomial evaluated at natural-number inputs and witnesses. An input belongs to the represented set exactly when a witness makes the polynomial zero, and any two complete witnesses at the same input must coincide.

Formalization targets

$$a\in S\ \Longleftrightarrow\ \exists w\in\mathbb N^m:\ P(a,w)=0,\qquad P(a,w)=P(a,v)=0\ \Longrightarrow\ w=v.$$

The proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w.

The goal is OAI.SingleFold.main.

Significance

The target strengthens mere existential representation by enforcing uniqueness across every auxiliary coordinate. It covers all recursively enumerable sets of positive-length natural tuples. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Encoding a computation with extra witnesses can introduce many choices that do not affect the represented input. Every such auxiliary choice must be controlled, rather than leaving hidden coordinates outside the uniqueness assertion.

Formalization scope

The input length and witness length are positive naturals. REPred expresses recursive enumerability. Polynomial coefficients and evaluation are integral, while variables range over naturals cast into the integers. The goal is existential and does not require one fixed universal polynomial.

The shared definitions are supplied by SingleFold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Single-fold Diophantine representations, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation: categoricity transfer beyond first-order logic

A class of structures is categorical in a cardinal $\lambda$ if it has exactly one model of size $\lambda$ up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with $H(K)=\beth_{(2^{\mathrm{LS}(K)})^+}$ (the Hanf number for existence of arbitrarily large models), categoricity in some $\lambda\ge H(K)$ should imply categoricity in every $\mu\ge H(K)$. Deciding which form holds is a central question in non-elementary model theory.

Timeline

• 1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
• 1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
• 1990 — Hart and Shelah show categoricity in $L_{\omega_1,\omega}$ can stop at $\aleph_k$ while holding for $\aleph_0,\dots,\aleph_{k-1}$, using finite-support group constructions (Israel J. Math. 1990).
• 1999 — Shelah proves categoricity transfer for AECs with amalgamation and records $H(K)$ as the existence bound (APAL 1999).
• 2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
• 2017 — Vasey proves downward transfer from a successor cardinal $\ge H(K)$ under amalgamation and tameness (APAL 2017).
• 2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
• 2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
• 2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
• 2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with $\mathrm{LS}(K)=\aleph_0$, categorical on a tail but with two nonisomorphic models at $H(K)=\beth_{\omega_2}$; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Work with relational structures in a finitary relational language $L$ (a set of relation symbols, each with a finite arity). An abstract elementary class is a class $K$ of $L$-structures with a relation $M\preceq_K N$ ("strong substructure") such that: $\preceq_K$ is a partial order on $K$ refining substructure; $K$ and $\preceq_K$ are closed under isomorphism; coherence holds ($M_0\subseteq M_1$, $M_0\preceq_K M_2$, $M_1\preceq_K M_2$ imply $M_0\preceq_K M_1$); unions of $\preceq_K$-chains are in $K$, are $\preceq_K$-extensions of each member, and are $\preceq_K$-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number $\mathrm{LS}(K)\ge\aleph_0+|L|$, the least $\theta$ such that every subset $A$ of a model $M$ lies in some $N\preceq_K M$ with $|N|\le|A|+\theta$.

$K$ is categorical in $\mu$ if it has a model of size $\mu$ and any two models of size $\mu$ are isomorphic. The beth numbers are $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits. CH is $2^{\aleph_0}=\aleph_1$.

Formalization targets

Goal: the CH counterexample (Theorem 1.1)

Assume CH. There is a countable finitary relational language $L$ and an AEC $K$ in $L$ such that

$$\mathrm{LS}(K)=\aleph_0,\qquad \beth_{\omega_2}=H(K)=\beth_{(2^{\aleph_0})^+},$$

$K$ has two nonisomorphic models of cardinality $\beth_{\omega_2}$, and, with $\Lambda=\beth_{(2^{\aleph_1})^+}$,

$$K\ \text{is categorical in every cardinal } \mu\ge\Lambda .$$

Hence $\Lambda^+>H(K)$ is a categoricity cardinal from which downward transfer to $H(K)$ fails, while eventual categoricity holds for this $K$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.

Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.

Difficulty

Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound $\beth_{\omega_2}$ while categoricity holds on a tail, with $\mathrm{LS}(K)=\aleph_0$. One must build two nonisomorphic models at $\beth_{\omega_2}$ and simultaneously rule out any two nonisomorphic models above $\Lambda$, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.

Formalization scope

• Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; $L:\mathbb N\to$ Type with $\Sigma_n L_n$ countable.
• ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
• HasLSNumber ℵ₀ asserts both that $\aleph_0$ is a Löwenheim–Skolem bound and that it is the least one.
• hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
• Categorical μ includes existence of a model of size $\mu$; TwoModels asks for two nonisomorphic models of the given size.
• CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.

Selected references

• M. Morley, Categoricity in power, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0175782-0
• K. Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Nat. Acad. Sci. USA (1938). https://doi.org/10.1073/pnas.24.12.556
• B. Hart and S. Shelah, Categoricity over P for first order T or categoricity for φ∈L_{ω1ω} can stop at ℵ_k while holding for ℵ_0,…,ℵ_{k−1}, Israel J. Math. (1990). https://doi.org/10.1007/BF02807869
• S. Shelah, Categoricity for abstract classes with amalgamation, Ann. Pure Appl. Logic (1999). https://doi.org/10.1016/S0168-0072(98)00016-5
• S. Vasey, Downward categoricity from a successor inside a good frame, Ann. Pure Appl. Logic (2017). https://doi.org/10.1016/j.apal.2016.10.003
• W. Boney and S. Vasey, A survey on tame abstract elementary classes, 2017. https://arxiv.org/abs/1512.00060
• A. Kolesnikov and C. Lambie-Hanson, The Hanf number for amalgamation of coloring classes, J. Symb. Logic (2016). https://doi.org/10.1017/jsl.2015.48
• J. Šaroch and J. Trlifaj, Deconstructible abstract elementary classes of modules and categoricity, Bull. London Math. Soc. (2024). https://doi.org/10.1112/blms.13172
• C. Espíndola, A complete classification of categoricity spectra of accessible categories with directed colimits, preprint, 2023. https://arxiv.org/abs/2301.13167
• OpenAI, A CH obstruction to a prescribed categoricity threshold, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf

Motivation

In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).

This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.

Setting

A cognitive-consequence space is a set $C$ of mental representations (thoughts) with a consequence operator $\mathrm{Cn} : \mathcal P(C) \to \mathcal P(C)$ and an implication connective $X \Rightarrow Y$ satisfying Tarski's axioms as listed in the paper (p. 5):

1. $C$ is countable;
2. $A \subseteq \mathrm{Cn}(A)$;
3. $A \subseteq B \Rightarrow \mathrm{Cn}(A) \subseteq \mathrm{Cn}(B)$;
4. $\mathrm{Cn}(\mathrm{Cn}(A)) = \mathrm{Cn}(A)$;
5. if $X \in \mathrm{Cn}(A)$ then $X \in \mathrm{Cn}(B)$ for some finite $B \subseteq A$;
6. if $Y \in \mathrm{Cn}(A \cup \{X\})$ then $(X \Rightarrow Y) \in \mathrm{Cn}(A)$;

together with the paper's standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$ (p. 5, after Definition 3.2).

A set $A$ is deductive if $\mathrm{Cn}(A) = A$. The cognitive-consequence topology is

$$\tau = \{A \subseteq C : \mathrm{Cn}(C \setminus A) = C \setminus A\},$$

and members of $\tau$ are consequence-wise open (CWO). The cognitive closure $\mathrm{Cl}^{\square}(A)$ is the intersection of all deductive sets containing $A$.

Separately, a cognitive similarity distance is a function $\mathrm{Cog} : C \times C \to [0,1]$ together with a relation $x \approx y$ ("$x$ and $y$ cognitively coincide") such that $\mathrm{Cog}(x,y) = 0 \iff x \approx y$, $\mathrm{Cog}$ is symmetric, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality holds. A sequence of thoughts $(x_n)$ converges to $x$ if for every $\varepsilon \in (0,1)$ we have $\mathrm{Cog}(x, x_n) < \varepsilon$ for all large $n$.

Formalization targets

Goal: "human intelligence is limitless" (Theorems 3.3 and 3.4)

For every cognitive-consequence space,

$$\Bigl(\exists f \in C\ \forall A \in \tau,\ f \notin A\Bigr) \ \wedge\ \Bigl(\exists f \in C\ \exists A \in \tau,\ f \in A\Bigr).$$

Milestones

Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology $\tau$ and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter $f_d$) and Theorem 5.1 (Gödel's incompleteness black hole).

Significance

The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about $\tau$, cognitive closure and cognitive limits.

Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$. The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with $\mathrm{Cn}(A) = C$ for every $A$, on a one-point language, satisfies all of them and has $\tau = \{\varnothing\}$. The goal is therefore expected to be resolved by a disproof.

Difficulty

The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from $C$ (a consistent theory). The paper's argument for Theorem 3.4 derives $\bigcap_i A_i = \varnothing$ and calls this a contradiction; nothing in the axioms forbids it.

Formalization scope

• CogCons.CognitiveConsequenceSpace C bundles $\mathrm{Cn}$, the connective imp, axioms (i)–(vi) and $\mathrm{Cn}(\varnothing) \neq \varnothing$. The syntax $\sigma$ and interpretation $I$ of the paper are not modelled beyond imp.
• The paper also asserts $\mathrm{Cn}(C) \neq C$ (p. 5). This contradicts axiom (ii), since $C \subseteq \mathrm{Cn}(C) \subseteq C$; including it would make every statement vacuously true, so it is omitted. For the same reason the second half of Corollary 3.4 ($\mathrm{Cl}^{\square}(C) \neq C$) is not included.
• Theorem 4.4 (the family $\{A : f \in \mathrm{Cn}(A)\}$ is a filter) is not included: closure under intersection fails in a four-element model satisfying all the axioms.
• Results relying on informal notions (the practical topology of Section 2, Theorems 3.9–3.11 and 3.13, Theorems 4.1–4.2, and the "solution space" of Section 5) are not formalized.
• CogCons.CognitiveSimilarityDistance C is independent of $\mathrm{Cn}$; sequences are indexed by $\mathbb N$ starting at $0$; $\approx$ is an arbitrary relation constrained only by the listed axioms.

Selected references

• S. Acharjee, U. Gogoi, The limit of human intelligence, arXiv:2310.10792v2 [math.GM], 2023. https://arxiv.org/abs/2310.10792
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20(2), 7–15, 1998. https://doi.org/10.1007/BF03025291

Motivation

How large can the power set of an infinite set be? For a regular cardinal $\kappa$ (one that is not the supremum of fewer than $\kappa$ smaller ordinals) the answer is: almost anything. Easton's theorem (1970) shows that the function $\kappa \mapsto 2^{\kappa}$ on regular cardinals can be prescribed arbitrarily in any model of ZFC, subject only to monotonicity and König's inequality $\operatorname{cf}(2^{\kappa}) > \kappa$. For a long time it was expected that singular cardinals — those that are such a supremum, like $\aleph_{\omega}$ — would behave the same way.

They do not. In 1974 Jack Silver proved that the Generalized Continuum Hypothesis cannot fail for the first time at a singular cardinal of uncountable cofinality: if $2^{\alpha} = \alpha^{+}$ for every infinite $\alpha < \kappa$ and $\operatorname{cf}\kappa > \omega$, then $2^{\kappa} = \kappa^{+}$. This was the first ZFC theorem constraining the continuum function at singular cardinals, and it opened the area now called the singular cardinal problem.

A short timeline:

• 1970 — Easton: the continuum function on regular cardinals is essentially arbitrary.
• 1974 — Silver (ICM Vancouver): GCH cannot first fail at a singular cardinal of uncountable cofinality; more generally the Singular Cardinal Hypothesis is decided at cofinality $\omega$.
• 1975 — Galvin and Hajnal: elementary inequalities for cardinal powers at singular cardinals of uncountable cofinality.
• 1976–77 — Baumgartner and Prikry, and independently Jensen, give elementary (non-forcing, non-ultrapower) proofs of Silver's theorem; the proof reproduced in Jech's Chapter 8 is of this kind.
• 1977 — Magidor: it is consistent, relative to large cardinals, that GCH holds below $\aleph_{\omega}$ while $2^{\aleph_{\omega}} > \aleph_{\omega+1}$ — so Silver's restriction to uncountable cofinality is necessary.
• 1980s onwards — Shelah's pcf theory, whose flagship result $\aleph_{\omega}^{\aleph_0} < \aleph_{\omega_4}$ (when $\aleph_\omega$ is a strong limit) grows out of exactly the stationary-set machinery assembled here.

This mission is the first in a series formalizing Thomas Jech, Set Theory (Third Millennium Edition, Springer 2003). It covers Chapter 8, "Stationary Sets" (pp. 91–98).

Setting

Fix a regular uncountable cardinal $\kappa$ and regard it as the well-ordered set of ordinals below it. A set $C \subseteq \kappa$ is closed unbounded, or a club, if it is unbounded in $\kappa$ and contains all of its limit points below $\kappa$ (an ordinal $\alpha > 0$ is a limit point of $C$ when $\sup(C \cap \alpha) = \alpha$). A set $S \subseteq \kappa$ is stationary if $S \cap C \neq \emptyset$ for every club $C$. Clubs are closed under intersections of fewer than $\kappa$ of them, so they generate a $\kappa$-complete filter, the club filter; its dual is the nonstationary ideal.

The club filter has a second closure property with no analogue for ordinary filters. The diagonal intersection of a $\kappa$-indexed family is

$$\mathop{\triangle}_{\alpha<\kappa} X_\alpha \;=\; \Bigl\{ \xi < \kappa \;:\; \xi \in \bigcap_{\alpha<\xi} X_\alpha \Bigr\},$$

and a filter closed under diagonal intersections is called normal. A function $f$ defined on $S \subseteq \kappa$ is regressive if $f(\alpha) < \alpha$ for all nonzero $\alpha \in S$.

For cardinal arithmetic, $\operatorname{cf}\kappa$ denotes the cofinality of $\kappa$ (the least length of an unbounded sequence in $\kappa$), $\kappa^{+}$ the cardinal successor, and $\kappa$ is singular when $\operatorname{cf}\kappa < \kappa$. The Singular Cardinal Hypothesis (SCH) is the assertion that $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$ for every singular $\kappa$ with $2^{\operatorname{cf}\kappa} < \kappa$. A sequence of cardinals is normal if it is strictly increasing and continuous at limits.

Formalization targets

Goal — Silver's theorem (Jech 8.12)

$$\kappa \text{ singular},\ \operatorname{cf}\kappa > \omega,\ \bigl(\forall \alpha \ \aleph_0 \le \alpha < \kappa \Rightarrow 2^{\alpha} = \alpha^{+}\bigr) \;\Longrightarrow\; 2^{\kappa} = \kappa^{+}.$$

This is the weakest statement of the chapter that still needs the full machinery: it fixes no particular $\kappa$ and no particular cofinality, and it stays correct no matter how the singular cardinal problem develops above it.

Milestones, in dependency order

1. Lemma 8.4 — the diagonal intersection of $\kappa$ clubs is a club; equivalently the club filter is normal.
2. Theorem 8.7 (Fodor) — a regressive function on a stationary set is constant on a stationary subset.
3. Theorem 8.10 (Solovay) — every stationary subset of $\kappa$ is the union of $\kappa$ pairwise disjoint stationary sets.
4. Lemma 8.14 — if $\langle \kappa_\alpha\rangle$ is normal with limit $\kappa$, $\lambda^{\operatorname{cf}\kappa} < \kappa$ for $\lambda < \kappa$, and $\{\alpha : \kappa_\alpha^{\operatorname{cf}\kappa_\alpha} = \kappa_\alpha^{+}\}$ is stationary in $\operatorname{cf}\kappa$, then $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$.
5. Theorem 8.13 (Silver) — SCH at every cardinal of cofinality $\omega$ implies SCH everywhere.

Significance

Silver's theorem is the boundary between the two halves of cardinal arithmetic. Above it sit the ZFC theorems of pcf theory; below it sit the consistency results (Magidor, Prikry, Radin forcing) that show how much freedom is left, and they are confined to cofinality $\omega$ precisely because Theorems 8.12 and 8.13 close off everything else. Its proof also packages tools used throughout set theory: the normality of the club filter, Fodor's pressing-down lemma, and the technique of bounding almost disjoint families of functions by a stationary-set argument.

Formalization status: Mathlib already has clubs and stationary sets in an arbitrary well-ordered type (IsClub, IsStationary), with the finite and $<\kappa$-indexed intersection lemmas — Jech's Lemma 8.2 and Theorem 8.3. It does not have diagonal intersections, Fodor's theorem, Solovay's splitting theorem, or any singular cardinal arithmetic beyond the definitions of regular and singular cardinals. Each milestone below is therefore a genuine addition, and the first three are reusable well outside this mission.

Difficulty

The naive route to the goal — induct on $\alpha < \kappa$ and pass to the limit — fails immediately: $2^{\kappa}$ for singular $\kappa$ is not determined by the values $2^{\alpha}$ for $\alpha < \kappa$ in any elementary way; that is exactly the content of the independence results. What the proof must do instead is bound the number of functions on $\operatorname{cf}\kappa$, and it gets that bound from a stationary set rather than from a club: uncountable cofinality is what makes the set of relevant stages stationary, and stationarity is what survives the diagonal argument. Cofinality $\omega$ breaks this at the first step, since every subset of $\omega$ that is unbounded is already a club and Fodor's theorem is empty.

The two hard pieces are Lemma 8.14 and, inside it, Lemma 8.16: given an almost disjoint family $F$ of functions with $f(\alpha) \in A_\alpha$ and $|A_\alpha| \le \aleph_\alpha$ on a stationary set of $\alpha$, one must show $|F| \le \aleph_{\omega_1}$ by assigning to each $f$ a pair (stationary set, bounded restriction) and checking the assignment is injective. That argument uses Fodor's theorem on a set of functions, and the bookkeeping does not simplify.

Formalization scope

The ambient order is Mathlib's type of ordinals below a cardinal, k.ord.ToType (written Below k in the mission's definition bundle); clubs and stationary sets are Mathlib's IsClub and IsStationary on that type, so a set is closed in the sense of being closed under suprema of directed subsets — equivalent, for a well-order with the order topology, to Jech's "contains its limit points". Families indexed by "$\alpha < \kappa$" are functions out of that same type, which is what makes the diagonal intersection typecheck without a side condition. Cardinal exponentiation, cofinality (Ordinal.cof of k.ord) and the successor cardinal (Order.succ) are Mathlib's.

One trivializing formalization is ruled out explicitly: the GCH hypothesis of the goal is stated for infinite cardinals $\alpha < \kappa$ only. Quantified over all cardinals it would be unsatisfiable — $2^{2} = 4 \neq 3 = 2^{+}$ — and Silver's theorem would become vacuous.

A complete development needs: diagonal intersections and the normality of the club filter; Fodor's theorem; the sets $E^{\kappa}_{\lambda} = \{\alpha < \kappa : \operatorname{cf}\alpha = \lambda\}$ and their stationarity; Solovay's splitting theorem via Lemmas 8.8 and 8.9; almost disjoint families of ordinal functions and the counting Lemmas 8.15 and 8.16; and Theorem 5.22(ii) on cardinal powers, which Jech's proof of Theorem 8.13 cites. Contributions of any of these as separate reductions are welcome, as are alternative proofs of the goal (for instance via a generic elementary embedding) that bypass some of the chain.

Selected references

• Thomas Jech, Set Theory, The Third Millennium Edition, revised and expanded. Springer Monographs in Mathematics, Springer, 2003 (ISBN 3-540-44085-2). Chapter 8, "Stationary Sets", pp. 91–98 — the source of every statement in this mission.
• Jack Silver, On the singular cardinals problem. Proceedings of the International Congress of Mathematicians (Vancouver, 1974), vol. 1, pp. 265–268.
• William B. Easton, Powers of regular cardinals. Annals of Mathematical Logic 1 (1970), pp. 139–178.
• Fred Galvin and András Hajnal, Inequalities for cardinal powers. Annals of Mathematics 101 (1975), pp. 491–498.
• James E. Baumgartner and Karel Prikry, Singular cardinals and the generalized continuum hypothesis. American Mathematical Monthly 84 (1977), pp. 108–113.
• Menachem Magidor, On the singular cardinals problem I. Israel Journal of Mathematics 28 (1977), pp. 1–31.

Motivation

Cantor's continuum problem asks for the value of $2^\kappa$, the cardinality of the power set of an infinite cardinal $\kappa$. For regular cardinals ZFC says almost nothing: by Easton's theorem (1970) the function $\kappa\mapsto 2^\kappa$ on regular cardinals can be essentially any non-decreasing function with $\operatorname{cf}(2^\kappa)>\kappa$. For singular cardinals the picture is different, and the singular cardinals hypothesis (SCH) is the natural statement of "GCH-like behaviour at singular cardinals". It arose from the question whether the least cardinal at which GCH fails can be singular.

Timeline.

• Scott (1961): if GCH holds on a set of measure one below a measurable cardinal $\kappa$, then $2^\kappa=\kappa^+$.
• Solovay (1974): above a strongly compact cardinal, SCH holds.
• Silver (1975): if $\kappa$ is singular of uncountable cofinality and $2^\lambda=\lambda^+$ for all infinite $\lambda<\kappa$, then $2^\kappa=\kappa^+$. Consequently the least failure of SCH has countable cofinality.
• Silver, Prikry: from a supercompact cardinal, a model of $\neg$SCH (Prikry forcing over a measurable $\kappa$ with $2^\kappa>\kappa^+$).
• Gitik (1989–1991), building on Woodin: $\mathrm{ZFC}+\neg\mathrm{SCH}$ is equiconsistent with a measurable cardinal of Mitchell order $\kappa^{++}$.
• Todorcevic, Veličković (1980s): the proper forcing axiom implies $2^{\aleph_0}=\aleph_2$.
• Viale (2006): the proper forcing axiom implies SCH.

Setting

All cardinals live in one universe. For a cardinal $\kappa$, $\kappa^+$ is its successor cardinal and $\operatorname{cf}\kappa$ its cofinality (the cofinality of the initial ordinal of $\kappa$). A cardinal is singular if it is infinite and $\operatorname{cf}\kappa<\kappa$, and a strong limit if $\kappa\neq0$ and $2^\lambda<\kappa$ for all $\lambda<\kappa$.

• GCH: $2^\kappa=\kappa^+$ for every infinite $\kappa$.
• SCH (first form, following Mitchell 1992): $2^\kappa=\kappa^+$ for every singular strong limit $\kappa$.
• SCH$_2$ (second form): for every singular $\kappa$, $2^{\operatorname{cf}\kappa}<\kappa$ implies $\kappa^{\operatorname{cf}\kappa}=\kappa^+$.

A normal measure on $\kappa$ is a nonprincipal $\kappa$-complete ultrafilter on $\kappa$ under which every regressive function is constant on a measure-one set; $\kappa$ is measurable if it is uncountable and carries one. $\kappa$ is strongly compact if it is uncountable and every proper $\kappa$-complete filter on any set extends to a $\kappa$-complete ultrafilter. The proper forcing axiom (PFA) asserts that for every proper poset $P$ and every $\aleph_1$ dense subsets of $P$ there is a filter meeting all of them.

Formalization targets

Goal: Silver's reduction

$$\Bigl(\forall\lambda\ \text{singular strong limit},\ \operatorname{cf}\lambda=\aleph_0\Rightarrow 2^\lambda=\lambda^+\Bigr)\ \Longrightarrow\ \mathrm{SCH}.$$

SCH itself is independent of ZFC, so it cannot be a goal; the goal is the ZFC theorem that SCH can only first fail at countable cofinality.

Milestones (in order)

1. GCH $\Rightarrow$ SCH.
2. $\kappa^{\operatorname{cf}\kappa}=2^\kappa$ for every singular strong limit $\kappa$.
3. SCH$_2$ $\Rightarrow$ SCH.
4. Silver's theorem: $\kappa$ singular, $\operatorname{cf}\kappa>\aleph_0$, GCH below $\kappa$ $\Rightarrow$ $2^\kappa=\kappa^+$ (already published and proved on the platform as JechSetTheory.silver).
5. The second-form reduction: SCH$_2$ at all $\lambda$ of countable cofinality implies SCH$_2$ everywhere (published, open, as JechSetTheory.sch_of_sch_cof_aleph0).
6. The least counterexample to SCH has cofinality $\aleph_0$.
7. Scott's theorem: $D$ a normal measure on $\kappa$ and $\{\alpha<\kappa: 2^{|\alpha|}=|\alpha|^+\}\in D$ imply $2^\kappa=\kappa^+$.
8. Solovay's theorem: if $\kappa$ is strongly compact, then $2^\mu=\mu^+$ for every singular strong limit $\mu>\kappa$.
9. PFA $\Rightarrow 2^{\aleph_0}=\aleph_2$.
10. PFA $\Rightarrow$ SCH.

Significance

The goal locates the first possible failure of SCH: any model of $\neg$SCH must have a counterexample of countable cofinality, which is why Prikry-type forcing (which adds an $\omega$-sequence) is the standard tool for producing failures, and why $\aleph_\omega$ is the canonical test case. Milestones 1, 7, 8 and 10 show that very different hypotheses (GCH, large cardinals, forcing axioms) all imply SCH, while milestone 9 shows PFA does so without GCH.

These results are classical and have complete published proofs (Jech, Set Theory, Chapters 8, 20, 24, 31). Silver's theorem is already machine-checked on this platform; the rest, including the stationary-set form of Silver's theorem needed for the goal, are not yet formalized here.

Difficulty

The naive attempt at the goal, "apply Silver's theorem at the least counterexample", fails: Silver's theorem as stated needs GCH at all infinite cardinals below $\kappa$, but SCH below $\kappa$ says nothing about regular cardinals or non-strong-limits. The proof needs the stronger, stationary-set version of Silver's theorem (Galvin–Hajnal style), applied to the stationary set of singular strong limits of countable cofinality below $\kappa$. Scott's and Solovay's theorems need ultrapower arguments, and PFA $\Rightarrow$ SCH needs reflection and covering-type combinatorics; none of these exist in Mathlib.

Formalization scope

• Cardinals are Mathlib Cardinal.{u}; singularity is Cardinal.IsSingular, strong limit is Cardinal.IsStrongLimit, cofinality is κ.ord.cof, successor is Order.succ κ. The second form reuses the published predicate JechSetTheory.SCHAt.
• A measure on $\kappa$ is an ultrafilter on Ordinal.{u} containing the ordinals below $\kappa$; completeness quantifies over index types of universe u. "Proper filter" in the definition of strong compactness is Filter.NeBot; without it no cardinal would be strongly compact and Solovay's theorem would be vacuous.
• Properness of a poset is encoded by the Gray–Shelah game characterization (names for ordinals in maximal-antichain form, forcing unfolded into predensity), because Mathlib has no forcing relation; this encoding deserves particular scrutiny. Posets are nonempty preorders with $q\le p$ meaning $q$ is stronger.
• Not formalized: the consistency and equiconsistency results (Gitik, Prikry forcing, Silver's supercompact construction, inner-model lower bounds) and the strictness of "SCH$_2$ is stronger than SCH"; these are statements about models of ZFC rather than theorems of ZFC.
• Reusable infrastructure welcome: clubs and stationary sets on cardinals (partly available in Def_JechStationary), ultrapowers by normal measures, Fodor's lemma, Galvin–Hajnal bounds.

Selected references

• W. J. Mitchell, On the singular cardinal hypothesis, Trans. Amer. Math. Soc. 329(2), 507–530, 1992.
• J. Silver, On the singular cardinals problem, Proc. ICM Vancouver 1974, 265–268, 1975.
• T. Jech, Set Theory, 3rd millennium ed., Springer, 2003.
• M. Gitik, The strength of the failure of the singular cardinal hypothesis, Ann. Pure Appl. Logic 51, 215–240, 1991.
• M. Viale, The proper forcing axiom and the singular cardinal hypothesis, J. Symbolic Logic 71(2), 473–479, 2006.
• S. Shelah, Proper and Improper Forcing, Springer, 1998.
• Wikipedia, Singular cardinals hypothesis, revision 1349753131. https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131

Motivation

The separable quotient problem asks whether every infinite-dimensional Banach space admits a separable infinite-dimensional quotient. The selected statement isolates a negative result under the continuum hypothesis. The pinned manuscript supplies the research context.

Setting

A quotient is encoded as a surjective bounded linear map between Banach spaces over the same scalar field. The target considers both real and complex scalars.

Formalization target

The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is

$$\mathrm{CH}\quad\Longrightarrow\quad\neg\mathrm{SQ}(\mathbb R)\land\neg\mathrm{SQ}(\mathbb C).$$

The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.

Significance and status

CH is an explicit assumption. The published goal does not state relative consistency, a positive model, or the complete independence assertion in the manuscript title. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Relative independence of the separable quotient problem, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A finite algebra has a lattice of congruences, ordered by inclusion. The source studies which finite lattices arise in this way, and the available goal captures its colored-graph characterization. The source is OpenAI's September 2026 manuscript.

Setting

A congruence is an equivalence relation preserved by every basic operation of an algebra. A graph witness assigns lattice-valued colors to pairs of finitely many vertices, with symmetry, diagonal, triangle, separation, and seed-connectivity conditions.

Formalization targets

$$\operatorname{Representable}(L)\quad\Longleftrightarrow\quad\operatorname{HasGraphWitness}(L).$$

For any finite type Lat carrying a lattice structure with a least element ⊥, Lat is Representable if and only if it HasGraphWitness. Representable means that there is a positive size n and an algebra on Fin n (a finite list of operations, each of some finite arity, acting on the carrier) such that Lat is order-isomorphic to the poset of congruences of that algebra, where a congruence is an equivalence relation compatible with every operation: if corresponding arguments are related coordinatewise, the outputs are related; congruences are ordered by the inherited order on equivalence relations. HasGraphWitness means that there is a positive size n and a Lat-valued coloring color of ordered pairs from Fin n satisfying five conditions: color is symmetric; color(a,b)=⊥ exactly when a=b; color(a,b) ≤ color(a,m) ⊔ color(m,b) for all a, b, m; whenever lower ≰ upper in Lat, some pair has color ≤ lower but not ≤ upper; and for every nonempty finite set of seed pairs, any pair whose color is at most the join of the seed colors is connected to the seeds. Connected is the equivalence closure of the relation Marked, where a,b are Marked if some self-map p of the vertices satisfies color(p x,p y) ≤ color(x,y) for all x,y and sends some seed pair (s,t) to (a,b).

The goal is OAI.FiniteCongruence.graph_criterion.

Significance

The equivalence provides a finite combinatorial certificate for representation as an entire congruence lattice. It is the characterization component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Representing a lattice inside a congruence lattice is weaker than obtaining all congruences. The witness’s seed-connectivity condition must capture this fullness and work in both directions.

Formalization scope

The lattice is finite and has a least element. The algebra carrier and graph witness carrier each have positive finite size. Operations have finite arities, and representation is an order isomorphism. The manuscript’s undecidability conclusions are not among the attached targets.

The shared definitions are supplied by FiniteCongruenceGraph. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Finite congruence lattices: characterization and undecidability, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).

Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.

Timeline

• 1982. Immerman and Vardi capture polynomial time on ordered structures by fixed-point logic (doi:10.1145/800070.802187, doi:10.1145/800070.802186); Chandra and Harel raise the unordered question (doi:10.1016/0022-0000(82)90012-5).
• 1988. Gurevich formulates the question of a logic capturing polynomial time and conjectures that none exists.
• 1992. Cai, Fürer and Immerman construct polynomial-time graph queries beyond fixed-point logic with counting (doi:10.1007/BF01305232).
• 1999, 2002. Blass, Gurevich and Shelah introduce choiceless polynomial time and study CFI and linear-algebra instances as potential separating examples (doi:10.1016/S0168-0072(99)00005-6, doi:10.2178/jsl/1190150152).
• 2000. Shelah claims noncapture for counting extensions; later accounts continue to list the problem as open.
• 2008. Dawar, Richerby and Rossman show that CFI queries over ordered base graphs are CPT-definable, and that bounded-rank CPT with counting fails on them (doi:10.1016/j.apal.2007.11.011).
• 2010–2023. Rossman and Pago prove functional lower bounds for CPT (no construction of hyperplanes, no fine preorders on hypercubes) (doi:10.1007/978-3-642-15025-8_28, doi:10.4230/LIPIcs.CSL.2021.33); Grädel, Pakusa, Schalthöfer and Kaiser characterize CPT by iterated first-order interpretations (doi:10.1109/LICS.2015.68).
• 2025. Dawar, Grädel, Kullmann and Pago still record the capture problem as open (doi:10.4230/LIPIcs.MFCS.2025.40).

The source of this mission is an OpenAI preprint dated September 23, 2026.

Setting

Fix the field $\mathbb F=\mathbb F_3$ and the vocabulary of eight binary relation symbols $\tau=\{\mathrm{Ed},\mathrm{Cf},\mathrm{EB},\mathrm{VB},I,Z_0,Z_1,Z_2\}$. For a finite $\tau$-structure $A$ put

$$Y=\{y:\mathrm{Ed}(y,y)\},\quad X=\{a:\mathrm{Cf}(a,a)\},\quad X_t=\{a\in X:\mathrm{VB}(t,a)\}\ (t\in X),$$ $$C(y,a)=\sum_{x\in Y,\ I(a,x)}\ \sum_{\delta\in\mathbb F,\ Z_\delta(y,x)}\delta .$$

With unknowns $(\lambda_a)_{a\in X}$ and $(\mu_y)_{y\in Y}$ (separate families), the system consists of

$$\sum_{a\in X_t}\lambda_a=1\quad(t\in X),\qquad \mu_y=\sum_{a\in X_t}\lambda_a\,C(y,a)$$

for every $(t,y)\in X\times Y$ such that some $a\in X_t$ and $x\in Y$ satisfy $I(a,x)$ and $\mathrm{EB}(y,x)$. The query $Q(A)$ says this system is consistent over $\mathbb F_3$. No promise is imposed on the input.

A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of $A$, using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program defines $Q$ if for fixed polynomials $T,S$, on every input of size $n$ it halts within $T(n)$ steps, touches at most $S(n)$ hereditarily finite objects, and accepts exactly when $Q(A)$ holds. No bound on set rank is imposed.

Formalization targets

Goal: Theorem 1

$$Q\ \text{is isomorphism-invariant},\qquad Q\in\mathrm{P}\ \text{(from an ordered encoding)},\qquad Q\notin\mathrm{CPT}.$$

The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.

Significance

The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because $Q$ is expressible in fixed-point logic with a solvability or rank operator over $\mathbb F_3$ (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.

Formalization scope

• Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.
• OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.
• FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.
• This is the original operational formulation; the paper's proof passes through the interpretation characterization of CPT (Grädel–Pakusa–Schalthöfer–Kaiser), which a formal proof must either formalize or bypass.

A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.

Selected references

• OpenAI, Choiceless polynomial time with counting does not capture polynomial time, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf
• A. Blass, Y. Gurevich, S. Shelah, Choiceless polynomial time, Ann. Pure Appl. Logic, 1999. https://doi.org/10.1016/S0168-0072(99)00005-6
• A. Blass, Y. Gurevich, S. Shelah, On polynomial time computation over unordered structures, J. Symbolic Logic, 2002. https://doi.org/10.2178/jsl/1190150152
• J.-Y. Cai, M. Fürer, N. Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica, 1992. https://doi.org/10.1007/BF01305232
• A. Dawar, D. Richerby, B. Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Ann. Pure Appl. Logic, 2008. https://doi.org/10.1016/j.apal.2007.11.011
• E. Grädel, W. Pakusa, S. Schalthöfer, Ł. Kaiser, Characterising choiceless polynomial time with first-order interpretations, LICS, 2015. https://doi.org/10.1109/LICS.2015.68
• B. Rossman, Choiceless computation and symmetry, 2010. https://doi.org/10.1007/978-3-642-15025-8_28
• B. Pago, Choiceless computation and symmetry: limitations of definability, CSL, 2021. https://doi.org/10.4230/LIPIcs.CSL.2021.33
• N. Immerman, Relational queries computable in polynomial time, STOC, 1982. https://doi.org/10.1145/800070.802187
• A. K. Chandra, D. Harel, Structure and complexity of relational queries, J. Comput. System Sci., 1982. https://doi.org/10.1016/0022-0000(82)90012-5

Motivation: how many nested stars does a regular language need?

A regular expression describes a set of words using letters, union, concatenation and the Kleene star $P^*$ (any finite repetition of words from $P$). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.

Timeline

• 1963 — Eggan connects ordinary star height with the cycle structure of transition graphs and raises the question of its unboundedness (Michigan Math. J. 1963).
• 1965 — Schützenberger characterizes the star-free languages (generalized height $0$) as those recognized by finite aperiodic monoids (Inform. Control 1965).
• 1966 — Dejean and Schützenberger show that ordinary star height is unbounded already over a two-letter alphabet (Inform. Control 1966).
• 1992 — Pin, Straubing and Thérien prove generalized height at most one for languages recognized by finite nilpotent groups of class two and for further monoid classes (Inform. Comput. 1992, Theorems 7.3 and 7.8).
• 2002 — Straubing distinguishes the questions "is generalized star height bounded?" and "is it at most one?" in his account of the problem (LATIN 2002, p. 537).
• 2016–2017 — Bourne and Ruškuc prove height-one bounds for subword-counting languages with factors of length at most three (Theor. Comput. Sci. 2016); Bourne extends this to arbitrary fixed factors in his thesis (St Andrews, 2017, hdl:10023/12024).
• 2026 — Companion OpenAI preprints prove uniform bounds of thirteen (Finite Monoid Computations and a Uniform Generalized Star-Height Bound) and four (Generalized Star Height at Most Four).
• 2026 — The OpenAI preprint Generalized Star Height at Most Three (OpenAI Math Release, September 25, 2026) claims the bound three. It has not been peer reviewed and its theorem is not formally verified. Whether height one always suffices remains open; no language of generalized height greater than one is known.

Setting

Fix a finite alphabet $\Sigma$ and let $\Sigma^*$ be the set of finite words. A generalized regular expression over $\Sigma$ is built from the constants $0$ (denoting $\emptyset$) and $1$ (denoting $\{\varepsilon\}$), single letters $a\in\Sigma$, union $P\cup Q$, concatenation $PQ$, complement $\neg P$ (taken in $\Sigma^*$), and star $P^*$. Its height is defined by

$$h(0)=h(1)=h(a)=0,\quad h(P\cup Q)=h(PQ)=\max\{h(P),h(Q)\},\quad h(\neg P)=h(P),\quad h(P^*)=1+h(P).$$

For a regular language $L\subseteq\Sigma^*$, the generalized star height $h_\Sigma(L)$ is the least height of an expression over $\Sigma$ denoting $L$.

In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language $L$ and height at most $n$.

Formalization targets

Goal: generalized star height at most three (Theorem 1.1)

For every finite alphabet $\Sigma$ and every regular language $L\subseteq\Sigma^*$,

$$h_\Sigma(L)\le 3 .$$

The goal is published on the platform with status Open.

Significance

The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.

Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.

Difficulty

The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from $\Sigma^*$ to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo $n$ and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.

Formalization scope

• The alphabet is any Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).
• Expressions must use letters of the same alphabet, so no auxiliary letters may be introduced; complement is relative to all words over that alphabet.
• height charges $1$ only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.
• Needed infrastructure: recognition of regular languages by finite monoids, prefix codes and unique factorization, and closure of bounded-height expressions under Boolean operations. The generalized-expression layer is reusable for the companion bounds (four and thirteen) and for formal work on star-free languages.

Selected references

• L. C. Eggan, Transition graphs and the star-height of regular events, Michigan Math. J. 10 (1963). https://doi.org/10.1307/mmj/1028998975
• M.-P. Schützenberger, On finite monoids having only trivial subgroups, Inform. Control 8 (1965). https://doi.org/10.1016/S0019-9958(65)90108-7
• F. Dejean and M.-P. Schützenberger, On a question of Eggan, Inform. Control 9 (1966). https://doi.org/10.1016/S0019-9958(66)90083-0
• J.-É. Pin, H. Straubing and D. Thérien, Some results on the generalized star-height problem, Inform. Comput. 101 (1992). https://doi.org/10.1016/0890-5401(92)90063-L
• H. Straubing, On logical descriptions of regular languages, LATIN 2002, LNCS 2286. https://doi.org/10.1007/3-540-45995-2_46
• T. Bourne and N. Ruškuc, On the star-height of subword counting languages and their relationship to Rees zero-matrix semigroups, Theor. Comput. Sci. 653 (2016). https://doi.org/10.1016/j.tcs.2016.09.024
• T. Bourne, Counting subwords and other results related to the generalised star-height problem for regular languages, PhD thesis, University of St Andrews, 2017. https://hdl.handle.net/10023/12024
• OpenAI, Generalized Star Height at Most Three, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Generalized-Star-Height-at-Most-Three-September-25-2026/article.pdf

Motivation

When are two scientific theories "the same theory in different words"? Philosophers of science have used two formal criteria. Definitional equivalence (Glymour) is strict: it requires a common definitional extension and therefore cannot relate theories with different numbers of sorts. Categorical equivalence (Halvorson, Weatherall) is liberal: it asks only that the categories of models be equivalent. It has been applied to classical mechanics, electromagnetism and Newtonian gravitation (Weatherall 2016; survey in Weatherall 2019).

Barrett and Halvorson (2016) proposed Morita equivalence as a syntactic criterion between these two. It allows definitions of new sorts (products, coproducts, subsorts, quotients) in addition to the usual definitions of new predicates and function symbols. Their main results place the new criterion strictly between the other two:

• Morita equivalence implies categorical equivalence (their Theorem 5.1).
• The converse fails (their Theorem 5.2).

This mission formalizes that comparison: the semantic core of Morita extensions, the implication, the separating example, and the paper's motivating "two kinds of things" example.

Setting

A signature $\Sigma$ (Sig) consists of a type of sorts, function symbols $f : \sigma_1\times\dots\times\sigma_m\to\sigma$ and predicate symbols $p\subseteq\sigma_1\times\dots\times\sigma_m$. Formulas (Formula L Γ) are built in a typed context $\Gamma$ from $\bot$, $=$, predicates, $\to$ and $\forall$. A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory $T$ is a set of formulas in context, each read as its universal closure; a model of $T$ is a structure satisfying them all.

The category $\mathrm{Mod}(T)$ (Model T) has the models of $T$ as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories $T_1,T_2$ are categorically equivalent (CategoricallyEquivalent) if $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$.

A Morita extension of a $\Sigma$-theory $T$ (MoritaData L T) adds to $\Sigma$:

• new sorts, each with its defining symbols:
  • a product $\sigma$ of $\sigma_1,\sigma_2$, with projections $\pi_1,\pi_2$;
  • a coproduct, with injections $\rho_1,\rho_2$;
  • a subsort cut out by a $\Sigma$-formula $\varphi(x)$, with an injection $i$;
  • a quotient by a $\Sigma$-formula $\varphi(x_1,x_2)$, with a projection $\varepsilon$;
• new predicates and function symbols, each explicitly defined by a $\Sigma$-formula.

Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension $T^+$ (D.ext) is $T$ together with these axioms. Each definition must satisfy its admissibility condition in every model of $T$:

Definition	Condition
subsort	$\exists x\,\varphi(x)$
quotient	$\varphi$ is an equivalence relation
function symbol	$\forall x\,\exists!y\,\varphi(x,y)$

The reduct gives a functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (D.proj).

$T_1$ and $T_2$ are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ and $T_2\rightsquigarrow T_2'$ (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.

Formalization targets

Goal: Morita equivalence implies categorical equivalence

$$T_1 \text{ Morita equivalent to } T_2 \;\Longrightarrow\; \mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2).$$

Milestones

1. Unique expansion. Every model $M$ of $T$ has an expansion $N\models T^+$ with $\Pi N\cong M$, and any two such expansions are isomorphic.
2. $\Pi$ is faithful.
3. $\Pi$ is full.
4. Conservativity. For every $\Sigma$-formula $\alpha$: $T\models\alpha$ iff $T^+\models\alpha$.
5. Translation. Every $\Sigma^+$-formula whose free variables all have old sorts is $T^+$-equivalent to a $\Sigma$-formula.
6. Two kinds of things. $T_1=\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ over one sort is Morita equivalent to the empty theory over two sorts.
7. Separating example, first half. $T_1=\{\exists^{=1}x\,(x=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$, over one sort and countably many unary predicates, are categorically equivalent.
8. Separating example, second half. These two theories are not Morita equivalent.

Milestones 1–3 together say that $\Pi$ is an equivalence of categories. Milestones 6–8 are not needed for the goal; they record the paper's examples, which show that Morita equivalence relates theories with different numbers of sorts and is strictly stronger than categorical equivalence.

Significance

The result itself. The goal makes Morita equivalence a syntactic sufficient condition for categorical equivalence: an explicit dictionary of definitions yields an equivalence of model categories. Milestone 8 shows the converse fails, so categorical equivalence is strictly weaker. Milestone 6 shows that Morita equivalence, unlike definitional equivalence, can relate theories with different numbers of sorts. Together these locate the criterion that later philosophy-of-physics work uses to compare formulations with different ontologies, such as different numbers of kinds of objects.

Formalizing it. The results are proved on paper and, as far as is known, have no machine-checked proofs. Mathlib's ModelTheory library is single-sorted, so none of this is available there. The mission produces a reusable many-sorted first-order logic with:

• syntax, semantics and signature maps;
• elementary embeddings and the category of models;
• Morita extensions with their reduct functors.

The paper's arguments for conservativity and translation are informal in places; for example, the translation in the appendix uses coding of new-sorted variables. A formal proof fixes these details.

Difficulty

The obvious route to the goal composes the reduct functors along the chains. The work lies in showing that each reduct is an equivalence when the arrows are elementary embeddings.

• Fullness. An elementary embedding of reducts extends uniquely to the new sorts. Showing that the extension is again elementary requires the translation of Milestone 5: every $\Sigma^+$-formula has to be pulled back to a $\Sigma$-formula, including formulas that quantify over the new sorts.
• Coproduct and quotient sorts. Quantifiers over these sorts must be eliminated in favour of quantifiers over the old sorts.

For Milestone 8 the difficulty is reversed. One must rule out every pair of chains, including chains that introduce arbitrary new sorts. The paper's proof argues with a single common Morita extension. The definition, however, allows chains, and the paper notes that a chain need not collapse to a single extension. The argument must therefore be run through conservativity and translation along each chain.

Formalization scope

• Self-contained logic. Signatures have dependent arities (Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.
• Theories. A theory is a Set (Axiom L), each axiom being a formula in context read as its universal closure. Because sorts are nonempty, this agrees with the sentence version.
• Nonempty sorts. Every structure has nonempty carriers. This is the paper's convention, and without it Milestone 6 is false: the empty theory over two sorts would have models with an empty sort.
• Morita extensions are built, not recognized. MoritaData L T lists the new sorts and symbols and their defining $\Sigma$-formulas. The signature $\Sigma^+$ (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of $T$. Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.
• A common signature up to renaming. MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of $T_2'$ iff its F-reduct is a model of $T_1'$.
• Universes. Models live in Type.
• Separating example. The paper writes $T_2$ with fresh symbols $q_i$; here $T_1$ and $T_2$ share the signature with predicates $p_i$, which only renames symbols.
• No trivialization. None of the targets holds vacuously: Morita extensions require genuine admissibility proofs, and the arrows are elementary embeddings, not arbitrary maps. Milestone 6 needs explicit chains and an explicit renaming, with arity casts.

A complete development will need:

• the substitution and weakening lemmas for de Bruijn formulas;
• the realization of signature maps;
• the construction of expansions;
• a translation function from $\Sigma^+$-formulas to $\Sigma$-formulas.

These pieces are reusable for any later work on interpretations or theoretical equivalence. Alternative proofs of Milestone 8, for example by counting finitely axiomatized subtheories, are welcome.

Selected references

• T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556–582. arXiv:1506.04675. Source of all targets: §3–§5 and the appendix; Example 4 and Theorems 4.1–4.3, 5.1, 5.2.
• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. arXiv:1411.5757.
• J. O. Weatherall, Theoretical Equivalence in Physics, Philos. Compass 14 (2019). arXiv:1810.08192.
• H. Halvorson, The Logic in Philosophy of Science, Cambridge University Press, 2019. doi:10.1017/9781316275603.

Comparing undecidable problems

Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input $n$ is whether $n$ belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.

The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.

Sets, enumeration, and oracle access

A set $A\subseteq\mathbb N$ is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input $n$, the procedure halts exactly when $n\in A$. The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.

For each set $A$, define its characteristic function by

$$\chi_A(n)=\begin{cases}1&n\in A,\\0&n\notin A.\end{cases}$$

An oracle for $A$ answers requests for this function's values. It always supplies an answer, even if membership in $A$ cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.

Write $A\le_T B$ when an algorithm with access to the membership oracle for $B$ computes $\chi_A$ on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both $A\not\le_T B$ and $B\not\le_T A$; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.

Formalization target

The goal is the following unconditional existence statement:

$$\exists A,B\subseteq\mathbb N,\qquad A\text{ is c.e.}\ \land\ B\text{ is c.e.}\ \land\ A\not\le_T B\ \land\ B\not\le_T A.$$

Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.

Mathematical and formal significance

The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.

The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.

Difficulty of simultaneous requirements

The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.

Formalization scope

The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.

The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.

A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.

Selected references

• Richard M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944), Proceedings of the National Academy of Sciences of the USA 43(2), 236–238, 1957. DOI; free archived paper.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms (Russian: Неразрешимость проблемы сводимости теории алгоритмов), Doklady Akademii Nauk SSSR 108(2), 194–197, 1956. Math-Net bibliography, 1956 entry.
• Arnold W. Miller, Lecture notes in Recursion Theory, University of Wisconsin–Madison, version dated December 3, 2008, Section 26, Theorem 26.2, pages 51–54. Author-hosted PDF.