Mathematical Logic

Motivation

The continuum hypothesis (CH) asks how large the set of real numbers is. Cantor proved that $|\mathbb Z|=|\mathbb Q|<|\mathbb R|$, and in 1878 he conjectured that no set has cardinality strictly between that of the integers and that of the reals. Settling CH was the first of Hilbert's problems at the 1900 International Congress of Mathematicians. The question was answered by showing that it cannot be answered from the standard axioms: CH is independent of Zermelo–Fraenkel set theory with choice (ZFC).

Timeline (as recorded in the source):

• 1878 — Cantor formulates the (weak) continuum hypothesis; in 1882 he states CH in its modern form.
• 1900 — Hilbert lists CH as the first of his problems.
• 1906 — Kőnig proves a theorem that, combined with Hausdorff's notion of cofinality (1908), shows $2^{\aleph_0}\neq\aleph_\alpha$ whenever $\alpha$ has cofinality $\omega$.
• 1930 — Patai: if $2^\kappa$ is the $\gamma$-th successor of $\kappa$ for every infinite $\kappa$, then $\gamma$ is finite.
• 1938/1940 — Gödel proves that AC and GCH hold in the constructible universe $L$, so $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$.
• 1947 — Sierpiński proves that ZF + GCH implies AC.
• 1963 — Cohen invents forcing and proves $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$.
• 1986 — Freiling shows that $\neg$CH is equivalent to his axiom of symmetry.

Setting

A cardinal measures the size of a set; $|A|\le|B|$ means there is an injection $A\to B$, and $|A|=|B|$ a bijection. $\aleph_0=|\mathbb N|$, $2^\kappa=|\mathcal P(X)|$ for $|X|=\kappa$, so $|\mathbb R|=2^{\aleph_0}$. $\aleph_\alpha$ is the $\alpha$-th infinite cardinal, $\beth_\alpha$ is defined by $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits, and $\mathrm{cf}$ denotes cofinality.

• CH: there is no $S\subseteq\mathbb R$ with $\aleph_0<|S|<2^{\aleph_0}$ (CH).
• GCH: for every infinite cardinal $\kappa$ there is no cardinal strictly between $\kappa$ and $2^\kappa$ (GCH).

Independence is a statement about a first-order theory. The language of set theory has one binary relation symbol $\in$ (setLang). ZF (ZF) consists of extensionality, foundation, pairing, union, power set, infinity, and all instances of the separation and replacement schemas; ZFC (ZFC) adds the axiom of choice (acSentence). CH and GCH are also written as first-order sentences (chSentence, gchSentence): CH says that every subset of $\mathcal P(\omega)$ injects into $\omega$ or receives an injection from $\mathcal P(\omega)$. A theory is consistent if it has a model, and $T\models\sigma$ means $\sigma$ holds in every model of $T$; by Gödel's completeness theorem these coincide with the proof-theoretic notions.

Formalization targets

Goal: independence of CH from ZFC

$$\mathrm{Con}(\mathrm{ZFC})\ \Longrightarrow\ \mathrm{ZFC}\not\models\mathrm{CH}\ \text{ and }\ \mathrm{ZFC}\not\models\neg\mathrm{CH}.$$

Milestones

1. $|\mathbb Z|=|\mathbb Q|<|\mathbb R|$.
2. $\mathrm{CH}\iff 2^{\aleph_0}=\aleph_1$.
3. (Gödel) $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$.
4. $\mathrm{ZFC}+\mathrm{GCH}\models\mathrm{CH}$.
5. (Cohen) $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$.
6. (Kőnig) $2^{\aleph_0}\neq\aleph_\alpha$ when $\mathrm{cf}(\alpha)=\omega$; and $\mathrm{cf}(2^{\aleph_0})>\aleph_0$.
7. (Sierpiński) $\mathrm{ZF}+\mathrm{GCH}\models\mathrm{AC}$.
8. $\mathrm{GCH}\iff\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+1}\iff\forall\alpha,\ \aleph_\alpha=\beth_\alpha$.
9. Under GCH: $A<B\Rightarrow 2^A<2^B$ for infinite $A$, and the three-case formula for $\aleph_\alpha^{\aleph_\beta}$.
10. (Patai) $\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+\gamma}$ implies $\gamma<\omega$.
11. (Freiling) the axiom of symmetry is equivalent to $\neg$CH.

Significance

The independence theorem shows that the ZFC axioms do not determine the size of the continuum, and it was among the first independence results for a mathematical statement. Its two halves introduced the two main tools of modern set theory: inner models (Gödel's $L$) and forcing (Cohen). Many statements in analysis, topology and measure theory were subsequently shown to be independent by the same methods.

For formalization, the goal requires a model theory of ZF inside Lean: interpreting the first-order theory, building $L$ inside an arbitrary model of ZF, and building forcing extensions of an arbitrary model of ZFC. The independence of CH was formalized in Lean 3 by the Flypitch project (Han and van Doorn, 2019–2020); no Lean 4 / Mathlib formalization is known to this mission. The cardinal-arithmetic milestones (2, 6, 8–11) are theorems of ZFC that can be proved directly in Lean's cardinal library.

Difficulty

Neither half follows from cardinal arithmetic in Lean: Lean's foundations prove that models of ZFC exist, but (assuming they are consistent) they prove neither CH nor its negation about Lean's own Cardinal, so an argument inside Lean's cardinal arithmetic alone cannot produce the required models. Gödel's half needs relativization of formulas to a definable inner class and absoluteness of the construction of $L$; Cohen's half needs a generic extension in which a new family of $\aleph_2$ reals is added while cardinals are preserved (the countable chain condition). Both require a theory of definability inside arbitrary, possibly non-well-founded, models of a first-order theory.

Formalization scope

• Syntax and semantics are Mathlib's first-order logic (FirstOrder.Language, Theory.IsSatisfiable, Theory.ModelsBoundedFormula written ⊨ᵇ). Formulas name their variables by natural numbers; close φ is the universal closure. Equality is the built-in equality of first-order logic.
• Consistency is satisfiability and provability is semantic consequence over models with universe in Type. By the completeness theorem these agree with the syntactic notions.
• The first-order CH uses $\mathcal P(\omega)$ in place of $\mathbb R$ (they are equinumerous in ZF). The first-order GCH is the choice-free form "$|S|\le|T|\le|\mathcal P(S)|\Rightarrow|T|=|S|$ or $|T|=|\mathcal P(S)|$, for $S$ infinite".
• The consistency results carry their hypotheses $\mathrm{Con}(\mathrm{ZF})$ or $\mathrm{Con}(\mathrm{ZFC})$ explicitly, even though these are provable in Lean. A solution may not replace a model of ZF by Lean's own universe in a way that assumes CH or its negation.
• Results that need large-cardinal hypotheses or class forcing (Easton, Solovay, Foreman–Woodin, Merimovich) are not part of this mission.

Reusable infrastructure: the language of set theory with standard abbreviations (pairs, functions, $\omega$, power set), satisfaction lemmas for the abbreviations, relativization, absoluteness, the constructible hierarchy, and forcing over models of ZFC.

Selected references

• G. Cantor, Ein Beitrag zur Mannigfaltigkeitslehre, J. Reine Angew. Math. 84 (1878) 242–258. https://doi.org/10.1515/crll.1878.84.242
• K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis, PNAS 24 (1938) 556–557. https://doi.org/10.1073/pnas.24.12.556
• K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Annals of Math. Studies 3, Princeton, 1940.
• P. J. Cohen, The independence of the Continuum Hypothesis I, II, PNAS 50 (1963) 1143–1148; 51 (1964) 105–110. https://doi.org/10.1073/pnas.50.6.1143, https://doi.org/10.1073/pnas.51.1.105
• C. Freiling, Axioms of symmetry: throwing darts at the real number line, J. Symbolic Logic 51 (1986) 190–200. https://doi.org/10.2307/2273955
• L. Gillman, Two classical surprises concerning the Axiom of Choice and the Continuum Hypothesis, Amer. Math. Monthly 109 (2002) 544–553. https://doi.org/10.2307/2695444
• K. Kunen, Set Theory: An Introduction to Independence Proofs, North-Holland, 1980.
• Wikipedia, Continuum hypothesis (revision 1376315189). https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189

Motivation

Bounded-depth Frege systems are the proof systems of propositional logic in which every formula of a proof has depth bounded by a fixed constant $d$; the resulting system is written $F_d$. They are the proof-theoretic counterpart of the circuit class $\mathrm{AC}^0$ and of the bounded arithmetic theories $I\Delta_0$ and its relatives: short $F_d$-proofs of a family of tautologies correspond to proofs of the corresponding first-order statement in bounded arithmetic. Lower bounds for $F_d$ are among the strongest lower bounds known for any natural proof system.

A basic structural question is whether the depth hierarchy $F_1 \subseteq F_2 \subseteq F_3 \subseteq \dots$ is strict in a strong sense. It is known that one extra level of depth can give an exponential speed-up, but in all known separations the tautologies themselves have depth growing with $d$. J. Krajíček asked whether there is a single fixed depth $k$ at which tautologies witnessing the separation of $F_{d+1}$ from $F_d$ exist for every $d$ (Open Problem Garden, F_d versus F_{d+1}; [Krajíček 1995, p. 243]). The question is closely related to conservativity relations among bounded arithmetic theories.

Timeline.

• 1987 — Buss: the pigeonhole principle $\mathrm{PHP}^{n+1}_n$ has polynomial-size Frege proofs (of unbounded depth).
• 1988 — Ajtai: $\mathrm{PHP}^{n+1}_n$ has no polynomial-size $F_d$-proofs for any fixed $d$.
• 1993/1995 — Pitassi–Beame–Impagliazzo and Krajíček–Pudlák–Woods: $F_d$-proofs of $\mathrm{PHP}^{n+1}_n$ require size $2^{n^{\varepsilon_d}}$.
• 1994 — Krajíček: for each $d$ there are tautologies of depth $d$ with polynomial-size $F_{d+1}$-proofs requiring exponential-size $F_d$-proofs, i.e. the problem is solved when $k$ may depend on $d$ ($k := d$).
• 2002 — Impagliazzo–Krajíček relate the question to conservativity among bounded arithmetic theories.

Setting

Formulas. A formula is in negation normal form over variables $p_0, p_1, \dots$: a literal $p_i$ or $\neg p_i$, a conjunction $\bigwedge(A_1,\dots,A_m)$ or a disjunction $\bigvee(A_1,\dots,A_m)$ of any finite number $m \ge 0$ of formulas. The depth of a literal is $0$, and the depth of $\bigwedge(A_1,\dots,A_m)$ or $\bigvee(A_1,\dots,A_m)$ is $1+\max_j \operatorname{depth}(A_j)$ (so clauses have depth $1$ and CNFs depth $2$). The size $|A|$ is the number of symbols (literals and connectives). A tautology is a formula true under every assignment. The negation $\overline{A}$ of a formula is obtained by De Morgan's laws.

The system $F_d$. Lines of a proof are sequents: finite lists $\Gamma$ of formulas, read as their disjunction. The rules are: (axiom) any $\Gamma$ containing both $p_i$ and $\neg p_i$; ($\wedge$) from $A, \Gamma$ for every $A \in \{A_1,\dots,A_m\}$ infer $\bigwedge(A_1,\dots,A_m), \Gamma$; ($\vee$) from $A_j, \Gamma$ infer $\bigvee(A_1,\dots,A_m), \Gamma$; (weakening) from $\Gamma$ infer any $\Delta$ containing every member of $\Gamma$; (cut) from $A,\Gamma$ and $\overline{A},\Gamma$ infer $\Gamma$. An $F_d$-proof of $A$ is a sequence of sequents, each following from earlier ones by a rule (lines may be reused), in which every formula has depth at most $d$, and which contains the sequent consisting of $A$ alone. Its size is the total size of all formulas in it.

Formalization targets

Write $\tau = (\tau_m)_{m\in\mathbb N}$ for a family of tautologies of depth at most $k$ with $|\tau_m| \ge m$. It requires exponential $F_d$-size if for some $\varepsilon>0$ and all large $m$ every $F_d$-proof of $\tau_m$ has size at least $2^{|\tau_m|^{\varepsilon}}$.

Goal

$$\exists k\ \forall d \ge k\ \exists \tau:\quad \tau_m \text{ has } F_{d+1}\text{-proofs of size } 2^{C(\log_2|\tau_m|)^C} \text{ and } \tau \text{ requires exponential } F_d\text{-size.}$$

The goal takes the weaker of the two upper bounds allowed by the problem (quasi-polynomial); the polynomial version implies it.

Milestones

1. Soundness of $F_d$: every formula with an $F_d$-proof is a tautology.
2. Completeness of $F_d$ for depth-$d$ formulas: every tautology of depth $\le d$ has an $F_d$-proof.
3. Exponential $F_d$ lower bound for $\mathrm{PHP}^{n+1}_n$: size $\ge 2^{n^{\varepsilon_d}}$.
4. The depth-dependent separation: for all large $d$, depth-$d$ tautologies with polynomial-size $F_{d+1}$-proofs requiring exponential $F_d$-size.

Significance

A positive answer would show that the extra power of depth $d+1$ over depth $d$ is visible already on formulas of a fixed, small depth, in particular that the hierarchy of bounded-depth Frege systems does not collapse on (for example) CNF tautologies. Through the correspondence with bounded arithmetic it bears on conservativity of theories of increasing quantifier complexity over a fixed class of low-complexity statements. A negative answer would say that for low-depth tautologies the bounded-depth Frege hierarchy collapses up to quasi-polynomial size.

Status: the goal is open. Milestones 1–2 are standard; milestones 3–4 are published theorems that, to the best of current knowledge, have no machine-checked proofs. Formalizing them requires switching-lemma machinery that would be reusable across proof complexity.

Difficulty

The known lower bounds for $F_d$ go through switching lemmas that simplify depth-$d$ formulas under random restrictions. In the known separations of $F_{d+1}$ from $F_d$ the hard tautologies have depth growing with $d$. Keeping the formulas at one fixed depth $k$ while $d$ ranges over all values requires a lower-bound argument whose strength depends on the depth of the proof lines alone, uniformly in $d$; the switching-lemma arguments used for depth-dependent separations do not directly provide this.

Formalization scope

Formulas are the Lean inductive type FdVersusFdSucc.Formula over variables ℕ, with conjunctions and disjunctions of lists (so and [] is true and or [] is false). Depth counts literals as $0$. $F_d$ is the dag-like one-sided sequent calculus described above; sequents are lists, weakening is by list inclusion. Proof size counts symbols of all formulas in all lines. Exponential lower bounds are asked only for all sufficiently large indices. The goal quantifies over $d \ge k$: for $d+1 < k$ no $F_{d+1}$-proof of a depth-$k$ formula exists, so "every $d$" cannot be meant literally. A family whose formulas have depth $> d$ would satisfy the lower bound vacuously; this is excluded because the formulas must have depth at most $k \le d$. The size condition $|\tau_m| \ge m$ rules out finite families.

Contributions welcome: proofs of soundness and completeness, a formalized switching lemma, and the classical lower bounds.

Selected references

• J. Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59(1), 1994, 73–86.
• J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995 (p. 243).
• Open Problem Garden, F_d versus F_{d+1}, http://www.openproblemgarden.org/op/f_d_versus_f_d_1
• M. Ajtai, The complexity of the pigeonhole principle, FOCS 1988.
• J. Krajíček, P. Pudlák, A. Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures & Algorithms 7(1), 1995.
• T. Pitassi, P. Beame, R. Impagliazzo, Exponential lower bounds for the pigeonhole principle, Computational Complexity 3, 1993.
• S. Buss, Polynomial size proofs of the propositional pigeonhole principle, J. Symbolic Logic 52, 1987.
• R. Impagliazzo, J. Krajíček, A note on conservativity relations among bounded arithmetic theories, Math. Logic Quarterly 48, 2002.

Motivation

Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012) proved that virtual-black-box obfuscation is impossible in general: there are programs from which any obfuscated copy leaks something that oracle access to the program does not. The definition being refuted asks that whatever can be computed from the obfuscated code can also be computed by a simulator that only has oracle access to the program and is told an upper bound on its size.

Appendix A of the paper studies the computability analogue of this definition, where running time is unbounded. Rice's theorem says that no non-trivial property of the function computed by a Turing machine is decidable. The appendix asks a relative version: if a property of programs depends only on the computed function and is decidable from the code on a promise, can it also be decided from black-box access alone? Theorem A.2 answers yes when the simulator is given the size $1^{|M|}$. Theorem A.4, the goal of this mission, shows that the size cannot be dropped. The result says which part of the simulator's interface is essential: an upper bound on program length is needed already in the computability setting, not only to pay for running time.

Setting

A machine $M$ is a one-tape Turing machine over the tape alphabet $\{0,1\}$, with $0$ the blank, and with states $0,1,\dots,q$; state $0$ is initial. In state $s$ reading symbol $a$ the machine either halts or moves to a new state and performs one action (move left, move right, or write a symbol). One such transition is one step. The size $|M|=q+1$ is the number of states.

Inputs are natural numbers in unary: input $x$ is the tape $1^x$, so $|x|=x$. When $M$ halts, its output is the number of consecutive $1$s starting at the head. The computed function $[M]:\mathbb N\rightharpoonup\mathbb N$ is defined where $M$ halts. The step-bounded function is

$$\langle M\rangle(1^t,x)=\begin{cases}y&\text{if } M(x)\text{ halts with output } y \text{ after at most } t \text{ steps},\\ \bot&\text{otherwise.}\end{cases}$$

A promise problem $\Pi=(\Pi_Y,\Pi_N)$ is a pair of disjoint sets of machines. It is closed under $[\cdot]$ if $[M]=[M']$ implies $M\in\Pi_Y\iff M'\in\Pi_Y$ and $M\in\Pi_N\iff M'\in\Pi_N$. It is decidable if a program $T$ reading the description $\ulcorner M\urcorner$ outputs $1$ on $\Pi_Y$ and $0$ on $\Pi_N$; outside $\Pi_Y\cup\Pi_N$, $T$ may diverge.

An oracle machine $S$ may query $\langle M\rangle$: it asks $(t,x)$ and receives $\langle M\rangle(1^t,x)$. $S^{\langle M\rangle}()$ is its output with this oracle and no input. In particular $S$ does not know $|M|$.

Conjecture A.3 (Rice's theorem, third generalization) asserts: for every promise problem $\Pi$ closed under $[\cdot]$ and decidable, there is an oracle machine $S$ with

$$M\in\Pi_Y\Rightarrow S^{\langle M\rangle}()=1,\qquad M\in\Pi_N\Rightarrow S^{\langle M\rangle}()=0.$$

The proof uses the description complexity of a partial function, $\mathrm{KC}(f)=\min\{|M|:[M]=f\}$.

Formalization targets

Goal: Theorem A.4

$$\neg\,\text{Conjecture A.3}.$$

There is a decidable promise problem closed under $[\cdot]$ that no oracle machine without the size can decide. The witness is

$$\Pi_Y=\{M: M\text{ always halts and } \exists x<\mathrm{KC}([M]),\ [M](x)=1\},\qquad \Pi_N=\{M: M\text{ always halts and } [M]\equiv 0\}.$$

Milestones, in the order of the paper's proof

1. $\Pi$ is closed under $[\cdot]$.
2. $\mathrm{KC}([M])\le|M|$.
3. $\Pi$ is decidable.
4. The machine $Z$ that reads its input and returns $0$ satisfies $\langle Z\rangle(1^t,x)=\bot$ for $t<|x|$ and $0$ otherwise, and $Z\in\Pi_N$.
5. If $S^{\langle M_0\rangle}()=\sigma$, there is $n$ such that every $M$ agreeing with $M_0$ on all $\langle\cdot\rangle(1^t,x)$ with $t,|x|\le n$ also has $S^{\langle M\rangle}()=\sigma$.
6. For all $n,r$ some machine computes $N_{n,r}(x)=0,1,r$ (for $|x|\le n$, $|x|=n+1$, $|x|\ge n+2$) and has the same step profile as $Z$ on all $|x|\le n$.
7. For every $n$ some $r$ has $\mathrm{KC}(N_{n,r})>n+1$, so machines computing $N_{n,r}$ lie in $\Pi_Y$.

Significance

The result. Theorem A.4 separates two interfaces for a simulator. With $1^{|M|}$, every decidable promise problem closed under $[\cdot]$ is decided from black-box access (Theorem A.2). Without it, some are not. The size bound in the virtual-black-box definition is therefore doing real work even when complexity is ignored, and any computability-theoretic notion of obfuscation must hand the simulator a bound on the program's length.

Formalizing it. The theorem is proved in the paper in a few lines, and the proof rests on facts the paper does not argue: that a halting oracle computation reads only finitely many oracle values, that a machine with a prescribed function and a prescribed running time on short inputs exists, and that some $N_{n,r}$ has description complexity above $n+1$. The paper says only "Let r be a string of Kolmogorov complexity 2n"; the counting argument behind it is left implicit. No machine-checked proof of Theorem A.4 or of Theorem A.2 is known to exist. This mission produces one in a model with literal step counts, together with reusable statements about step-bounded Turing machines and the use principle for oracle programs.

Difficulty

The obvious attempt at Conjecture A.3 is to search for a machine consistent with the observed values of $\langle M\rangle$ and run $T$ on it. Without a size bound the search space is infinite, and a finite prefix of $\langle M\rangle$ never pins down $[M]$. The difficulty of the formal proof is elsewhere. It has to build $N_{n,r}$ as an actual Turing machine with an exact step count on short inputs, and to prove that its description complexity exceeds $n+1$. Both need the step semantics to be exact. A fuel-based semantics in which larger programs need more fuel on the same input does not support the construction of $N_{n,r}$.

Formalization scope

Machines are Mathlib's Post–Turing machines Turing.TM0.Machine Bool (Fin (q+1)), with the blank false and initial state 0. $[M]$ is TM0.eval followed by the head read-out; $\langle M\rangle(1^t,x)$ iterates TM0.step at most $t$ times. $|M|$ is the number of states, so there are finitely many machines of each size. Inputs are unary, $|x|=x$. This is forced, because the proof compares inputs both with numbers ($x<\mathrm{KC}([M])$, $N_{n,r}(n+1)=1$) and with lengths ($|x|\le n$, $t<|x|$). The paper's string $r$ is a natural number. The description $\ulcorner M\urcorner$ is the encoding of $q$ and the transition table, and the decider $T$ is a Mathlib Nat.Partrec.Code acting on it. $\mathrm{KC}$ is sInf over $\mathbb N$, which would be $0$ for a function no machine computes; that case does not arise for $f=[M]$, and milestone 7 asserts $\mathrm{KC}>n+1$ outright.

Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval. A query $(t,x)$ is coded Nat.pair t x, and the answers $\bot$ and $y$ are coded $0$ and $y+1$. $S^{\langle M\rangle}()$ runs $S$ on the fixed input $0$.

The simulator is a single program chosen before $M$, and it only sees the values of $\langle M\rangle$ it queries. A formalization in which $S$ is an arbitrary function of the whole oracle, or receives $|M|$, would make the goal false, and one in which the oracle is $[M]$ changes the statement. Both are excluded here.

Needed infrastructure: computability of simulating a TM0 machine from its description (for milestone 3), the use principle for oracleEval with a total oracle (milestone 5), explicit construction and step analysis of $Z$ and $N_{n,r}$ (milestones 4 and 6), and a counting bound on machines of bounded size (milestone 7). The first two are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159 (Appendix A, Conjecture A.3 and Theorem A.4, p. A:42 of the author's copy).
• H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the AMS 74(2), 1953. https://doi.org/10.1090/S0002-9947-1953-0053041-6

Motivation

Program obfuscation asks for a compiler that turns a program into one computing the same function while revealing nothing beyond what black-box access to the function reveals. Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012; conference version CRYPTO 2001) showed that this "virtual black box" notion cannot be achieved in general. Part of their motivation is an informal reading of Rice's Theorem: since every non-trivial semantic property of programs is undecidable from the code, "the only useful thing you can do with a machine is run it". Section 5 of the paper asks whether a complexity-theoretic analogue holds, and Appendix A asks what the right computability-theoretic statement is once one passes from languages to promise problems.

Classical Rice's Theorem (Rice, 1953) concerns languages: a decidable set of machines closed under functional equivalence is empty or everything. For promise problems the naive analogue (Conjecture A.1 of the paper) is false: the problem "halts everywhere and outputs 1 on 0" versus "halts everywhere and outputs 0 on 0" is decidable, non-trivial, and closed under functional equivalence. Appendix A replaces "trivial" by "decidable by a simulator that only runs the machine", proves that version (Theorem A.2), and shows that the size bound given to the simulator cannot be dropped (Theorem A.4, a separate mission in this series). This mission formalizes Theorem A.2.

Setting

A machine $M$ is a program for a partial recursive function, identified with its description, a natural number $\ulcorner M\urcorner$. Its computed function $[M]:\mathbb N\rightharpoonup\mathbb N$ is possibly partial, and $[M]\equiv[M']$ means equality of partial functions. The size $|M|$ is the length of the binary description of $M$; there are at most $2^s$ machines of size $s$.

The bounded run of $M$ is

$$\langle M\rangle(1^t,x)=\begin{cases} y & \text{if } M(x)\text{ halts with output } y \text{ within budget } t,\\ \bot&\text{otherwise.}\end{cases}$$

An oracle machine $S$ may query $\langle M\rangle$ at any pair $(t,x)$ of its choice; $S^{\langle M\rangle}(z)$ is its output on input $z$. Oracle access to $\langle M\rangle$ is what running $M$ provides: one may choose inputs and budgets, but one never sees the code.

A promise problem $\Pi=(\Pi_Y,\Pi_N)$ is a pair of disjoint sets of machines. A machine $T$ decides $\Pi$ if $T(\ulcorner M\urcorner)=1$ for $M\in\Pi_Y$ and $T(\ulcorner M\urcorner)=0$ for $M\in\Pi_N$; nothing is asked of $T$ outside $\Pi_Y\cup\Pi_N$. $\Pi$ is closed under $[\cdot]$ if $[M]\equiv[M']$ implies $M\in\Pi_Y\Leftrightarrow M'\in\Pi_Y$ and $M\in\Pi_N\Leftrightarrow M'\in\Pi_N$.

A machine $N$ is $n$-compatible with $M$ if $\langle N\rangle(1^t,x)=\langle M\rangle(1^t,x)$ for all $t\le n$ and all $x$ with $|x|\le n$, and $S_n$ denotes the set of machines of size $|M|$ that are $n$-compatible with $M$.

Formalization targets

Goal: Theorem A.2 (p. A:41)

If $\Pi$ is closed under $[\cdot]$ and decidable, then there is one oracle machine $S$ such that for every machine $M$

$$M\in\Pi_Y\Rightarrow S^{\langle M\rangle}(1^{|M|})=1,\qquad M\in\Pi_N\Rightarrow S^{\langle M\rangle}(1^{|M|})=0 .$$

Milestones (proof of Theorem A.2, pp. A:41–A:42)

1. Fact (1): $n$-compatibility with $M$ is decidable by one oracle machine with oracle $\langle M\rangle$, uniformly in $M$, $N$, $n$.
2. Fact (3): if $[M]\not\equiv[N]$, there is $n'$ with $N$ not $n$-compatible with $M$ for every $n>n'$.
3. There is $n''$ such that every $N\in S_n$ with $n>n''$ satisfies $[N]\equiv[M]$.
4. If some stage $n$ finds $T$, run for $n$ steps, halting on all of $S_n$ with a common answer $\sigma$, then $\sigma=T(\ulcorner M\urcorner)$.
5. For $M\in\Pi_Y$ (resp. $\Pi_N$) such a stage exists, with answer $1$ (resp. $0$).

Significance

The result. Theorem A.2 is the precise sense in which a semantic property of programs, decidable from the code on a promise, is decidable without the code: running the program on chosen inputs for chosen budgets, plus a bound on its length, suffices. It is the computability-theoretic counterpart of Conjecture 5.2, the complexity-theoretic statement whose failure (Theorem 5.3, under cryptographic assumptions) is one face of the impossibility of obfuscation. Together with Theorem A.4 it isolates the size bound as the ingredient that makes the generalization true.

Formalizing it. The theorem has a complete proof in the paper, about one page long. No machine-checked version is known: the Prove2Me catalogue has classical Rice's Theorem for index sets of Nat.Partrec.Code (FamousTheorems.rice_theorem, which this proof does not use) but nothing on promise problems, bounded-run oracles, or simulators. A formal proof produces reusable infrastructure: the oracle $\langle M\rangle$ as a total function on query codes, decidability of compatibility relative to it, and a dovetailing simulator assembled as a uniform oracle program.

Difficulty

Each mathematical step is elementary; the work lies in the effective content. The obvious idea, "query $\langle M\rangle$ until $[M]$ is known and then decide", fails: $[M]$ is an infinite object, and no finite set of queries pins it down. The paper's simulator instead uses the size bound to restrict attention to finitely many candidate codes, and needs $T$ to agree on every surviving candidate at a common budget. Turning this into one oracle program requires enumerating all codes of a given size, deciding compatibility from finitely many oracle answers, comparing bounded runs of $T$, and searching over $n$, all uniformly in $M$ and with no access to $\ulcorner M\urcorner$. Termination holds only on promise instances, since $T$ may diverge elsewhere, so the argument cannot assume a total decider.

Formalization scope

Machines are Mathlib's Nat.Partrec.Code; descriptions are Encodable.encode; $[M]$ is Code.eval; $\langle M\rangle(1^t,x)$ is Code.evaln t M x : Option ℕ, with none for $\bot$. The budget of evaln is fuel rather than a literal Turing-machine step count. It is monotone in $t$, converges to $[M]$, and is primitive recursive in $(t,M,x)$, and these are the only properties of step counts that the proof uses. Inputs are natural numbers, $|x|$ is Nat.size x, and $|M|$ is Nat.size (encode M). Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval (a single syntax tree with an oracle-query instruction, equivalent to relative partial recursiveness). The oracle $\langle M\rangle$ is the total function sending Nat.pair t x to 0 for $\bot$ and to y + 1 for an output $y$. The simulator's input $1^{|M|}$ is the number $|M|$, since unary versus binary is immaterial here. "$S^{\langle M\rangle}(1^{|M|})=1$" means that the run halts with output $1$. Promise problems carry their disjointness, as in the paper, although no statement uses it. The decider $T$ is a Code applied to descriptions and may diverge off the promise.

The trivializing readings are excluded. $S$ is chosen before $M$ (one program, not one per machine). It receives the size of $M$, never its description, and many machines share each size. It sees only the finitely many oracle answers a halting run queries. The oracle is the bounded-run function $\langle M\rangle$, not $[M]$ or the code.

Contributions welcome: proofs of the milestones; a primitive-recursive enumeration of the codes of a given size; a proof that oracle M is uniformly computable from M, which is useful beyond this mission.

Selected references

• B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159
• H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the AMS 74(2), 1953. https://doi.org/10.1090/S0002-9947-1953-0053041-6
• S. Even, A. L. Selman, Y. Yacobi, The complexity of promise problems with applications to public-key cryptography, Information and Control 61(2), 1984. https://doi.org/10.1016/S0019-9958(84)80056-X

Motivation

The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.

This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.

Background

• 1961. Higman characterizes finitely generated subgroups of finitely presented groups as the recursively presented groups.
• 1974. Boone and Higman prove the characterization $G \le H \le K$ with $H$ simple and $K$ finitely presented, and ask whether $H$ can be finitely presented.
• 1980. Thompson embeds every finitely generated group with decidable word problem into a finitely generated simple group with decidable word problem; a later proof is given by Darbinyan and Steenbock (2022).
• 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups, which embed an acting group in a simple group; Zaremsky (2024) gives a finite-presentation criterion requiring a finitely presented acting group with finitely generated point stabilizers and finitely many orbits on unordered pairs.
• 2023–2026. The conjecture is verified for hyperbolic groups and contracting self-similar groups (Belk, Bleak, Matucci, Zaremsky), Baumslag–Solitar and free-by-cyclic groups (Bux, Llosa Isenrich, Wu), and $\mathrm{Aut}(F_n)$ and mapping class groups of punctured surfaces (Belk, Fournier-Facio, Hyde, Zaremsky); see the survey of Belk, Bleak, Matucci and Zaremsky.
• 2026. The OpenAI preprint Finite algebraic envelopes and the Boone–Higman conjecture (dated September 23, 2026) states a proof of the conjecture in general. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A group $G$ is finitely generated if some finite tuple $g_1, \dots, g_n$ generates it. A word is a finite list of letters $g_i^{\pm1}$; $G$ has decidable word problem if for some finite generating tuple the set of words evaluating to $1$ is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than $1$ and itself. An embedding is an injective homomorphism.

In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from $G$.

Formalization targets

Goal: Theorem 1.1 (Boone–Higman conjecture)

For every finitely generated group $G$,

$$G \text{ has decidable word problem} \iff G \text{ embeds in a finitely presented simple group.}$$

The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.

Significance

The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.

Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.

Difficulty

Finite presentation does not pass to subgroups, so Boone and Higman's simple group $H$ and finitely presented group $K$ cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.

Formalization scope

• GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.
• Decidability is ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.
• IsSimpleGroup includes nontriviality, matching the paper's convention.

The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.

Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.

Selected references

• OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf
• W. W. Boone, G. Higman, An algebraic characterization of groups with soluble word problem, J. Austral. Math. Soc. 18 (1974). https://doi.org/10.1017/S1446788700019108
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• R. J. Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Word Problems II, North-Holland, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
• J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
• M. C. B. Zaremsky, Finite presentability of twisted Brin–Thompson groups, Proc. Roy. Soc. Edinburgh Sect. A (2024). https://doi.org/10.1017/prm.2024.131
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture, Duke Math. J. 175 (2026). https://doi.org/10.1215/00127094-2025-0055
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
• K.-U. Bux, C. Llosa Isenrich, X. Wu, On the Boone–Higman conjecture for groups acting on locally finite trees, 2025. https://arxiv.org/abs/2408.05673
• J. Belk, F. Fournier-Facio, J. Hyde, M. C. B. Zaremsky, Boone–Higman embeddings of Aut(F_n) and mapping class groups of punctured surfaces, 2026. https://arxiv.org/abs/2503.21882
• A. Darbinyan, M. Steenbock, Embeddings into left-orderable simple groups, J. London Math. Soc. 105 (2022). https://doi.org/10.1112/jlms.12552

Motivation

Automatic verification of programs that manipulate pointers needs procedure specifications: preconditions saying which part of the heap a procedure touches and postconditions saying what it leaves behind. Writing them by hand does not scale to millions of lines of code. Calcagno, Distefano, O'Hearn and Yang (J. ACM 58(6), 2011) infer them compositionally with bi-abduction: when symbolic execution reaches a call whose precondition is not implied by the current state, it asks for the missing memory $M$ that would make it hold. This abduction question in separation logic,

$$\Delta * M \models H,$$

is the engine behind the Abductor tool and, later, Facebook Infer.

The question has many solutions ($M = \mathsf{false}$ is always one), so its quality matters. The paper defines an order $\precsim$ on solutions that prefers less memory and then logical strength, shows that a best solution always exists as a semantic object, and then asks whether it can be written down and computed in the language that the analysis actually manipulates: symbolic heaps. For the fragment whose only spatial predicate is points-to, it answers yes. That answer, Theorem 3.25, is the goal of this mission.

Setting

Values are natural numbers; $0$ is nil and the nonzero naturals are the locations. A heap $h$ is a finite partial map from locations to values; a stack $s$ assigns a value to every variable; a state is a pair $(s,h)$. Write $h = h_0 \uplus h_1$ when $h_0,h_1$ have disjoint domains and $h$ is their union. A predicate is an arbitrary set of states. On predicates:

• $s,h \models F * G$ iff $h = h_0 \uplus h_1$ with $s,h_0 \models F$ and $s,h_1 \models G$;
• $s,h \models F \mathbin{-\!\!*} G$ iff for every $h'$ disjoint from $h$ with $s,h' \models F$, we have $s,h \uplus h' \models G$;
• $\mathsf{emp}$ holds in the empty heap, $\mathsf{true}$ everywhere, and $\neg$, $\vee$, $\wedge$, $\exists X$, $\forall X$ are the Boolean and quantifier operations; $F \models G$ is inclusion.

Symbolic heaps of the Points-to Instantiation. Expressions $E$ are variables or natural-number constants. A pure formula $\Pi$ is a conjunction of $E = E'$ and $E \neq E'$. A spatial formula $\Sigma$ is a $*$-conjunction of points-to facts $E \mapsto E'$, possibly with $*\,\mathsf{true}$; here $s,h \models E \mapsto E'$ iff $[\![E]\!]s \neq 0$ and $h$ is the one-cell heap $[\,[\![E]\!]s \mapsto [\![E']\!]s\,]$. A symbolic heap is $H = \exists \vec X.\, \Pi \wedge \Sigma$, and a disjunction $D = H_1 \vee \dots \vee H_n$. In the abduction question (5), $\Delta * D \models H$, the left-hand side $\Delta = \Pi \wedge L_1 \mapsto R_1 * \dots * L_n \mapsto R_n$ is quantifier-free.

Orders. $M \le M'$ iff $M' \models M * \mathsf{true}$ (spatially smaller), and

$$M \precsim M' \iff (M \le M' \wedge M' \not\le M) \vee (M \le M' \wedge M' \le M \wedge M \models M').$$

$\min(F)$ keeps the states of $F$ no proper subheap of which (with the same stack) is in $F$. $\mathrm{Elsewhere}(F) = \neg(F \mathbin{-\!\!*} \mathsf{false})$ says that some separate heap satisfies $F$, and the compatible preorder is $D \le_c D' \iff (D \wedge \mathrm{Elsewhere}(\Delta)) \le (D' \wedge \mathrm{Elsewhere}(\Delta))$. Subtraction is $F - G = F \wedge \neg((\neg\mathsf{emp}) * G)$.

Formalization targets

Goal: Theorem 3.25

There is a single algorithm $f$ such that for every quantifier-free $\Delta$ and symbolic heap $H$ of the Points-to Instantiation, the disjunction $D = f(\Delta, H)$ satisfies

$$\Delta * D \models H \quad\text{and}\quad D \precsim M \ \text{ for every predicate } M \text{ with } \Delta * M \models H.$$

Both halves are part of the goal: the best solution is expressible as a disjunction of symbolic heaps, and it is computable.

Milestones, in the order the paper's argument uses them

1. Lemma 3.16. If $D$ is a minimal solution w.r.t. $\le_c$, then $\min(D \vee \neg\mathrm{Elsewhere}(\Delta))$ is the minimal solution w.r.t. $\precsim$.
2. Figure 2 derives solutions (§3.4.2). If $\Delta * [D] \triangleright H$ is derivable, then $\Delta * D \models H$.
3. Lemma 3.18. For all $\Delta, H$ some $D$ with $\Delta * [D] \triangleright H$ is derivable, and the proof search terminates.
4. Lemma 3.19. If $\Delta * [D] \triangleright H$ is derivable and $\Delta * F \models H$, then $D \le_c F$.
5. Lemma 3.20. $\mathrm{Incompat}(\Delta)$ and $\neg\mathrm{Elsewhere}(\Delta)$ are semantically equivalent.
6. Lemma 3.23. Six algebraic properties of subtraction, including $\min(F_1 \vee \dots \vee F_n) = G_1 \vee \dots \vee G_n$ with $G_i = ((F_i - F_1)\cdots - F_n)$.
7. Quantifier removal for pure formulae (§3.4.4). $\exists X.\Pi$ is equivalent to a computable pure formula without $X$.
8. Subtraction with quantifiers (§3.4.4). $(\exists\vec X.\Delta) - (\exists\vec Y.\Delta')$ is a computable disjunction of symbolic heaps.

Significance

The result. Semantically the best solution is $\min(\Delta \mathbin{-\!\!*} H)$ (Theorem 3.13 of the paper), a formula that nests $-\!\!*$ and negation around $*$, which no automatic separation-logic prover handles and which says nothing directly about the shape of the missing memory. Theorem 3.25 shows that in the points-to fragment this object collapses to a finite disjunction of symbolic heaps, the format in which an analysis draws "pictures of memory", and that it can be computed. It gives an optimal abduction procedure against which the paper's heuristic procedure can be measured.

Formalizing it. The theorem is proved in the paper, but several steps are given as sketches ("the proof of each of these properties is straightforward", "a straightforward exercise"), Lemma 3.18 has only a proof sketch, and the quantifier-free subtraction display on p. 33 is incomplete as printed (it inspects only the points-to facts and not the pure part of the subtracted heap). A machine-checked development would supply the missing arguments, fix the subtraction step, and give a verified reference implementation of optimal abduction for points-to symbolic heaps. No part of it is known to have been formalized.

Difficulty

The obvious route is to compute $\min(\Delta \mathbin{-\!\!*} H)$ directly, but $-\!\!*$ quantifies over all heaps, and symbolic heaps have no syntax for it. The paper splits the problem into three phases (a $\le_c$-minimal solution from a proof system, the incompatible solutions, and $\min$), and each phase carries its own difficulty. The proof system's minimality (Lemma 3.19) must hold against arbitrary semantic predicates, not only symbolic heaps, and it fails as soon as $\Delta$ may denote more than one heap for a given stack (the paper notes that adding list segments breaks it). Computing $\min$ needs subtraction of symbolic heaps with quantifiers, which in turn needs quantifier elimination for Boolean combinations of equalities over an infinite domain, and the paper's quantifier-free subtraction step has to be repaired. Showing that the final disjunction is $\precsim$-least, not merely a solution, needs all three phases.

Formalization scope

All statements live in the namespace BiAbduction.Systematic. Values are ℕ with nil 0, locations are the nonzero naturals, variables are ℕ (program and logical variables form one sort), and heaps are maps ℕ → Option ℕ with 0 unallocated and finite domain. Finiteness of heaps is essential, since $\min$ relies on well-foundedness of the subheap order. Predicates are arbitrary Set (Stack × Heap). The syntax is built from ℕ, Bool, Sum, Prod and List by abbreviations, so "computed by an algorithm" is Mathlib's Computable₂ with the standard Primcodable encodings. The left-hand side $\Delta$ has no true conjunct, as in the paper's proofs; the right-hand side may have one. Figure 2 is an inductive relation in which psto may match any right-hand points-to fact. The soundness and $\le_c$-minimality statements assume the paper's bound-variable convention (no variable bound in $H$ occurs in $\Delta$); the goal does not need it.

The goal cannot be met by a degenerate reading. The competitors $M$ range over all predicates, not only over disjunctions, and computability refers to fixed standard encodings. The points-to semantics excludes nil addresses, and heaps are finite.

A complete development needs the separation-logic algebra of predicates (associativity and commutativity of $*$, the adjunction between $*$ and $-\!\!*$), properties of $\min$ under finite heaps, the soundness and minimality of the proof system, quantifier elimination for equality logic, and a computability argument for list-manipulating procedures. The semantic layer and the quantifier-elimination result are reusable beyond this mission. Contributions to any milestone, and to the supporting lemmas of §3.3 (Lemmas 3.10–3.11, Theorem 3.13), are welcome.

Theorem numbers and page references are those of the accepted manuscript of the J. ACM article (72 pages), not of the typeset journal version.

Selected references

• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, Journal of the ACM 58(6), Article 26, 2011. https://doi.org/10.1145/2049697.2049700
• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. https://doi.org/10.1145/1480881.1480917
• J. Berdine, C. Calcagno, P. W. O'Hearn, Symbolic Execution with Separation Logic, APLAS 2005. https://doi.org/10.1007/11575467_5
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002. https://doi.org/10.1109/LICS.2002.1029817
• D. Pym, P. W. O'Hearn, H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1), 2004. https://doi.org/10.1016/j.tcs.2003.11.020

Motivation

Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation $\alpha \to (\beta, c)^2$ to measure exactly this, and asked which countable ordinals $\alpha$ satisfy $\alpha \to (\alpha, 3)^2$ — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal $\alpha>1$ is a power of $\omega$, so the question becomes: for which countable $\beta$ is $\omega^\beta$ a partition ordinal? This is Erdős Problem 592.

The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.

Timeline (as recorded on erdosproblems.com/592):

• 1957 — Specker. $\omega^2 \to (\omega^2,3)^2$, and $\omega^n \not\to (\omega^n,3)^2$ for every finite $n \ge 3$.
• 1972 — Chang. $\omega^\omega \to (\omega^\omega,3)^2$ (the subject of Erdős Problem 590). Milner extended this to $\omega^\omega \to (\omega^\omega,m)^2$ for all finite $m$; Larson (1973) gave a short proof.
• 1974 — Galvin and Larson. If $\beta \ge 3$ and $\omega^\beta$ is a partition ordinal then $\beta$ is additively indecomposable, so $\beta=\omega^\gamma$. They conjectured that every such $\beta\ge3$ works.
• 2010 — Schipperus. Writing $\beta=\omega^\gamma$: the relation holds when $\gamma$ is a sum of one or two indecomposable ordinals, and fails when $\gamma$ is a sum of four or more. This refutes the Galvin–Larson conjecture in general.

The case where $\gamma$ is a sum of exactly three indecomposable ordinals appears to be the remaining open case.

Setting

An ordinal $\alpha$ is identified with a well-ordered set $X_\alpha$ of order type $\alpha$. A red/blue colouring of the complete graph $K_\alpha$ on $X_\alpha$ assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on $X_\alpha$.

For ordinals $\alpha,\beta$ and a cardinal $c$, the partition relation $\alpha \to (\beta,c)^2$ holds when every red/blue colouring of $K_\alpha$ has

• a set $S \subseteq X_\alpha$, all of whose pairs are red, whose order type (with the order inherited from $X_\alpha$) is exactly $\beta$, or
• a set $T \subseteq X_\alpha$, all of whose pairs are blue, with $|T| = c$.

The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an $\alpha$ with $\alpha \to (\alpha,3)^2$.

An ordinal is additively indecomposable if it is nonzero and $a+b<\beta$ for all $a,b<\beta$; the additively indecomposable ordinals are exactly the powers $\omega^\delta$. An ordinal $\gamma$ is the sum of $k$ indecomposable ordinals when

$$\gamma = \omega^{\delta_1}+\cdots+\omega^{\delta_k}, \qquad \delta_1 \ge \cdots \ge \delta_k,$$

i.e. its Cantor normal form has $k$ terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.

Formalization targets

Goal: the three-term case

$$\gamma \text{ countable},\ \gamma=\omega^{\delta_1}+\omega^{\delta_2}+\omega^{\delta_3}\ (\delta_1\ge\delta_2\ge\delta_3) \;\Longrightarrow\; \omega^{\omega^\gamma} \to \left(\omega^{\omega^\gamma}, 3\right)^2 .$$

This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable $\gamma$ with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable $\beta$, $\omega^\beta$ is a partition ordinal iff $\beta\le2$ or $\beta=\omega^\gamma$ with $\gamma$ a sum of at most three indecomposables.

Milestones (known results)

1. Specker: $\omega^2 \to (\omega^2,3)^2$.
2. Specker: $\omega^n \not\to (\omega^n,3)^2$ for $3 \le n < \omega$.
3. Chang: $\omega^\omega \to (\omega^\omega,3)^2$.
4. Galvin–Larson: $\beta \ge 3$ countable and $\omega^\beta \to (\omega^\beta,3)^2$ imply that $\beta$ is additively indecomposable.
5. Schipperus: $\gamma$ countable and a sum of one or two indecomposables imply $\omega^{\omega^\gamma} \to (\omega^{\omega^\gamma},3)^2$.
6. Schipperus: $\gamma$ countable and a sum of $k \ge 4$ indecomposables imply $\omega^{\omega^\gamma} \not\to (\omega^{\omega^\gamma},3)^2$.

Significance

The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form $\omega^\beta$ asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.

Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.

Difficulty

The property is not monotone in $\beta$: it holds for $\beta=2$, fails for every finite $\beta\ge3$, holds again for $\beta=\omega$, and, by Schipperus, both holds and fails for various larger $\beta=\omega^\gamma$ depending on the number of terms in the Cantor normal form of $\gamma$. So no induction on $\beta$ can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.

Formalization scope

• Ordinals and cardinals are Mathlib's Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.
• The graph lives on α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red $K_\beta$ is a red clique s with typeLT s = β; a blue $K_3$ is a blue clique of cardinality exactly 3.
• IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of $k$" would not be well defined, since for instance $\omega+\omega^2=\omega^2$.
• ω ^ ω ^ γ means $\omega^{(\omega^\gamma)}$.
• The Galvin–Larson milestone states additive indecomposability directly as $\forall a,b<\beta,\ a+b<\beta$ (for $\beta \ge 3$ this is equivalent to $\beta=\omega^\gamma$).

The goal is not trivially satisfiable: the hypotheses hold, for example, for $\gamma=3$ and $\gamma=\omega^2+\omega+1$, and the conclusion is a genuine partition relation on an infinite ordinal.

Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of $\omega^\beta$, and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.

Selected references

• T. F. Bloom, Erdős Problem #592, erdosproblems.com. https://www.erdosproblems.com/592 (this page lists the original references [Sp57], [Ch72], [GaLa74], [Sc10] cited below).
• E. Specker, Teilmengen von Mengen mit Relationen, Comment. Math. Helv., 1957.
• C. C. Chang, A partition theorem for the complete graph on $\omega^\omega$, J. Combinatorial Theory Ser. A, 1972.
• J. A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$, Ann. Math. Logic, 1973/74.
• F. Galvin and J. Larson, Pinning countable ordinals, Fund. Math., 1974/75.
• R. Schipperus, Countable partition ordinals, Ann. Pure Appl. Logic, 2010.
• Formal Conjectures (Google DeepMind), Erdős Problems 590–592. https://github.com/google-deepmind/formal-conjectures

Why interpretations

Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main algorithmic consequence is that first-order model checking is fixed-parameter tractable on graphs given with a contraction sequence of bounded width. A parameter of this kind is useful only if the classes it bounds are closed under the constructions that arise in practice. Many such constructions are first-order definable: the complement of a graph, its square (join vertices at distance at most two), the map graph of a planar map. Section 8 of the paper shows that twin-width is stable under every such construction: a first-order interpretation of a class of bounded twin-width has bounded twin-width. Bounded VC-dimension, by contrast, is not preserved (interval graphs have VC-dimension at most two but interpret every graph, p. 3:41).

The result has since become the basis of the "model-theoretic" view of twin-width: bounded twin-width classes are closed under first-order transductions (Theorem 8.1 of the paper), and later work identifies them, among ordered structures, with the monadically dependent classes (Twin-width IV, Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé and Toruńczyk).

Setting

Let $G$ be a finite simple graph on a vertex set $V$.

Two vertex sets $X,Y$ are homogeneous if all pairs in $X\times Y$ are edges or none is. For a partition $\mathcal P$ of $V$, the red graph $G_{\mathcal P}$ has the parts as vertices, two distinct parts being adjacent when they are not homogeneous. $\mathcal P$ is a $d$-partition if $G_{\mathcal P}$ has maximum degree at most $d$. The graph $G$ has twin-width at most $d$, $\operatorname{tww}(G)\le d$, if there is a sequence of $d$-partitions from the partition into singletons to a partition with at most one part, each obtained from the previous one by merging two parts (p. 3:32).

A prenex formula of depth $\ell$ with two free variables is

$$\varphi(x,y)=Q_1x_1\,Q_2x_2\cdots Q_\ell x_\ell\ \varphi^*,\qquad Q_i\in\{\forall,\exists\},$$

with $\varphi^*$ a Boolean combination of atoms $u=v$ and $E(u,v)$, $u,v\in\{x_1,\dots,x_\ell,x,y\}$. The interpretation $\varphi(G)$ is the graph on $V$ in which distinct $u,v$ are adjacent iff $G\models\varphi(u,v)\wedge\varphi(v,u)$. For a class $\mathcal G$, $\varphi(\mathcal G)$ is the class of all induced subgraphs of the graphs $\varphi(G)$, $G\in\mathcal G$.

The proof works with morphism-trees. The complete tree $MT_k(V)$ has as nodes all tuples $(v_1,\dots,v_i)$ of vertices with $i\le k$, the parent of a tuple being its prefix. Two sibling nodes are equivalent in $(G,\mathcal P)$ if an automorphism of the tree swaps them, preserving equalities and adjacencies among the entries of every tuple and the part of $\mathcal P$ of every entry. A reduction deletes one of two equivalent siblings with its subtree, repeatedly; a reduct admits no further reduction. Two vertices $u,u'$ are adjacent in $E_{\ell+2}(G,\mathcal P)$ when $(u)$ and $(u')$ are equivalent in some reduction of $MT_{\ell+2}(V)$, and $I_{\ell+2}(G,\mathcal P)$ is the partition into the connected components of $E_{\ell+2}(G,\mathcal P)$.

Formalization targets

Goal: Theorem 8.3 (graphs)

For every prenex formula $\varphi(x,y)$ and every $d$ there is $D$ such that

$$\operatorname{tww}(G)\le d\ \Longrightarrow\ \operatorname{tww}\bigl(\varphi(G)[S]\bigr)\le D\quad\text{for every graph } G \text{ and every } S\subseteq V(G).$$

The bound $D$ depends on $\varphi$ and $d$ only. No explicit function is asserted: the paper gives none (the proof goes through a tower-type bound on reducts).

Milestones

1. Lemma 5.2 in graph form (p. 3:18, applied on p. 3:43): $r$-refining $h$-partitions from the finest to the coarsest partition give $\operatorname{tww}(G)\le r(h+1)$.
2. Lemma 7.3 (p. 3:32): reducts of $MT_\ell(G)$ have size bounded by a function of $\ell$.
3. Lemmas 7.11–7.14 (pp. 3:35–3:38): restriction to connected tuples rooted at a part and the pruned shuffle commute with reductions; the pruned shuffle of all $MT_\ell(G,\mathcal P,X)$ is $MT_\ell(G,\mathcal P)$, and that of reducts is a reduction of it.
4. Lemma 8.4 (p. 3:41) and its extension to reductions (p. 3:42): equivalent nodes $(u,v),(u,v')$ of $MT_{\ell+2}$ satisfy the same prenex formulas of depth $\ell$.
5. $I_{\ell+2}$ refines $\mathcal P$ and is monotone under coarsening (p. 3:42).
6. Lemma 8.5 (p. 3:42): a part of a $d$-partition meets boundedly many components of $E_{\ell+2}(G,\mathcal P)$.
7. Lemma 8.6 (p. 3:43): parts of $I_{\ell+2}(G,\mathcal P)$ inside parts at distance at least $3^{\ell+2}$ in $G_{\mathcal P}$ are homogeneous in $\varphi(G)$.

Significance

Theorem 8.3 turns every first-order definable graph construction into a source of bounded-twin-width classes: squares and fixed powers of planar graphs, complements, map graphs (as transductions, via Theorem 8.1), $k$-planar graphs and bounded-degree string graphs. Combined with the model-checking algorithm it gives FPT first-order model checking on all these classes, provided a contraction sequence is available. The theorem is also the first step of the model-theoretic characterisations of bounded twin-width in the later papers of the series.

The result is proved in the paper; no machine-checked proof of it, or of any twin-width bound, exists to our knowledge, and Mathlib has no notion of twin-width or of first-order interpretations of graphs. The mission asks for a formal proof of the graph case. The morphism-tree milestones are also the combinatorial core of the paper's linear-time model-checking algorithm (Theorems 7.5, 7.15), whose running-time statements are not part of this mission.

Difficulty

The obvious approach refines the $d$-partitions $\mathcal P_i$ of $G$ by the "type" of each vertex with respect to $\varphi$. The number of such types is not bounded: a vertex's behaviour depends on the whole graph through the quantifiers. The paper replaces types by the components of $E_{\ell+2}(G,\mathcal P_i)$, defined through reductions of morphism-trees that respect $\mathcal P_i$. Two facts must then be shown, and neither is local in an obvious way. First, the number of components inside a part is bounded (Lemma 8.5); this needs the pruned shuffle, which assembles a reduction of the whole tree $MT_{\ell+2}(G,\mathcal P)$ from reductions of the local trees $MT_{\ell+2}(G,\mathcal P,X)$, and the fact that it commutes with reductions (Lemma 7.12), where an automorphism of one local tree must be extended to the shuffle without breaking adjacency between non-homogeneous parts. Second, far-apart components are homogeneous in $\varphi(G)$ (Lemma 8.6), which needs the evaluation argument of Lemma 8.4 inside a reduction of the partitioned tree.

Formalization scope

• Graphs are SimpleGraph V on a Fintype with decidable equality. Twin-width is the predicate TwinWidthLE G d in the paper's partition form (pp. 3:12, 3:32); trigraphs are not formalized, and twin-width is never an infimum, so no junk value of sInf can make a bound vacuous. Merge steps merge exactly two distinct parts, so a sequence cannot jump to one part.
• Formulas are Mathlib's FirstOrder.Language.graph.Formula (Fin 2), evaluated in G.structure; variable 0 is $x$, variable 1 is $y$. Prenex is Mathlib's IsPrenex; quantifier depth qdepth is defined in the mission ($\exists=\neg\forall\neg$ counts once).
• The interpretation requires $u\neq v$ for an edge (a simple graph has no loops). The goal is the graph case of Theorem 8.3, which the page states for augmented binary structures; Section 8 itself says it works with undirected graphs (p. 3:40).
• In the goal the bound $D$ is chosen after $\varphi$ and $d$ and before the graph: a bound chosen after the graph would make the statement trivial. The hereditary closure (induced subgraphs on every $S$) is part of the statement.
• Morphism-trees are sets of tuples (Set (List V)), the paper's identification of a node with its current path (p. 3:30), which is exact for reductions of complete trees. Equivalent siblings are distinct. Distances in $G_{\mathcal P}$ are in $\mathbb N\cup\{\infty\}$, so disconnected parts are far apart. The sequence graph uses 0-based indices, hence the exponent $3^{\ell-(k+1)}$. The pruned shuffle is defined by its characterisation (each component of the sequence graph of a tuple lies in the tree of its local root). Lemmas of §7.3 carry its standing assumption $\ell>0$.
• Lemma 5.2 is posed for graphs with the bound $r(h+1)$ (the matrix lemma's $rt$ with $t=h+1$).
• Not in the mission: Theorem 8.1 (transductions), Lemma 8.2 and Lemma 5.1 (augmented binary structures), and all running-time statements (Theorems 1.1, 7.1, 7.5, 7.15, Corollaries 7.16–7.17).

Reusable beyond this mission: the partition form of twin-width, quantifier depth of first-order formulas, and the morphism-tree machinery (reductions, pruned shuffles), which formalizes the algorithmic core of first-order model checking on bounded twin-width. Contributions welcome: proofs of the §7 lemmas, of Lemma 8.4 by induction on the quantifier prefix, and the closure of twin-width under induced subgraphs.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655 (arXiv:2004.14789, https://arxiv.org/abs/2004.14789)
• É. Bonnet, U. Giocanti, P. Ossona de Mendez, P. Simon, S. Thomassé, S. Toruńczyk, Twin-width IV: Ordered Graphs and Matrices, J. ACM, 2024. https://arxiv.org/abs/2102.03117