Mathematical Logic

Motivation

A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.

Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.

Timeline

• 1992. Cai, Fürer and Immerman construct graph pairs that hide a global parity obstruction from bounded-variable counting logic (doi:10.1007/BF01305232).
• 1998. Gire and Hoang introduce a fixpoint logic with a symmetry-based choice construct (doi:10.1006/inco.1998.2712).
• 1999, 2002. Blass, Gurevich and Shelah introduce choiceless polynomial time and its counting extension, and study CFI and linear-algebra instances (doi:10.1016/S0168-0072(99)00005-6, doi:10.2178/jsl/1190150152).
• 2003. Dawar and Richerby define a fixed-point logic with symmetric choice, with parameters and nesting (doi:10.1007/978-3-540-45220-1_16).
• 2008. Dawar, Richerby and Rossman show that preordered CFI queries are CPT-definable, and that bounded-rank CPT fails on them (doi:10.1016/j.apal.2007.11.011).
• 2014–2021. Abu Zaid, Grädel, Grohe and Pakusa, and Lichter and Schweitzer, obtain CPT canonization for structures with small abelian, dihedral or cyclic colour classes (doi:10.1007/978-3-662-44522-8_5, doi:10.4230/LIPIcs.CSL.2021.31).
• 2010–2023. Rossman and Pago prove functional lower bounds for CPT (doi:10.1007/978-3-642-15025-8_28, doi:10.4230/LIPIcs.CSL.2021.33, doi:10.4230/LIPIcs.MFCS.2023.73).
• 2022–2023. Lichter and Schweitzer define CPT + WSC, show that definable isomorphism testing yields canonization, and ask whether WSC strictly adds expressive power (arXiv:2205.14003).

The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.

Setting

Let $A$ be a finite set of atoms and $\mathrm{HF}(A)$ the hereditarily finite sets over $A$. CPT terms are built from variables, $\emptyset$, $\mathrm{Atoms}$, $\mathrm{Pair}(a,b)=\{a,b\}$, $\mathrm{Union}$, $\mathrm{Unique}$ (the member of a singleton, else $\emptyset$), $\mathrm{Card}$ (the von Neumann ordinal $|a|$), comprehensions $\{s(\bar a,u):u\in t(\bar a),\ \theta(\bar a,u)\}$ and iteration from $\emptyset$; formulas use input relations, equality and Boolean connectives. A sentence $(\Phi,p)$ pairs a closed formula with a polynomial $p$ that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with $n$ atoms; exceeding the bounds yields a default or a failure value $\dagger$.

A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set $D$; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of $D$ to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is $\dagger$.

The true-model class of a sentence is the set of finite structures on which it returns true; false and $\dagger$ are both outside it.

Formalization targets

Goal: Theorem 1.1

For the fixed vocabulary $\tau$ of eight binary relations there is a CPT + WSC sentence $(\Phi,p)$ with exactly one WSC occurrence such that

$$\text{(i)}\ (\Phi,p)\ \text{returns true or false on every finite }\tau\text{-structure;}\qquad \text{(ii)}\ \mathrm{TrueModels}(\Phi,p)\neq\mathrm{TrueModels}(\Psi,q)\ \text{for every CPT sentence }(\Psi,q).$$

The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.

Significance

Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.

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

Difficulty

Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.

Formalization scope

• Syntax is a mutual inductive Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.
• Evaluation returns Option (none is $\dagger$). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.
• WSC validity (GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.
• FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.

A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.

Selected references

• OpenAI, Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026/paper.pdf
• 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
• M. Lichter, P. Schweitzer, Choiceless polynomial time with witnessed symmetric choice, 2023 (arXiv v3). https://arxiv.org/abs/2205.14003
• 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
• 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
• 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
• F. Gire, H. K. Hoang, An extension of fixpoint logic with a symmetry-based choice construct, Inform. and Comput., 1998. https://doi.org/10.1006/inco.1998.2712
• A. Dawar, D. Richerby, A fixed-point logic with symmetric choice, CSL, 2003. https://doi.org/10.1007/978-3-540-45220-1_16

Motivation

Turing reducibility compares sets of natural numbers by their information content: $A\le_TB$ if an oracle Turing machine with oracle $B$ computes the characteristic function of $A$. Identifying mutually reducible sets gives the Turing degrees $\mathcal D_T$, partially ordered by $\le_T$. A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.

Timeline

• 1939. Turing introduces oracle machines and relative computability (doi:10.1112/plms/s2-45.1.161).
• 1977. Jockusch and Solovay prove that every jump-preserving automorphism fixes all degrees above $\mathbf0^{(4)}$ (doi:10.1007/BF03007659).
• 1980. Nerode and Shore prove that every automorphism fixes some cone of degrees, whose base may depend on the automorphism (doi:10.1016/0003-4843(80)90004-2).
• 1999. Shore and Slaman prove that the Turing jump is definable from the order, so every automorphism preserves it (Math. Res. Lett., 1999).
• 2005. Slaman and Woodin's manuscript Definability in Degree Structures shows that every automorphism fixes all degrees above $\mathbf0''$, that the automorphism group is countable, that every automorphism has an arithmetic representation on sets of integers, and that rigidity is equivalent to their biinterpretability conjecture; see also Slaman's survey (doi:10.1142/9789812794055_0002).
• 2007. Shore gives direct degree-theoretic definitions of the jump (J. Math. Log., 2007).
• 2018. Kjos-Hanssen shows that automorphisms induced by permutations of the integers are trivial (doi:10.1017/bsl.2018.15).

After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.

Setting

An oracle is a function $A:\mathbb N\to\{0,1\}$ (a set of natural numbers). $A\le_TB$ means that the characteristic function of $A$ is partial recursive relative to $B$. This is a preorder; its quotient by $A\equiv_TB\iff(A\le_TB\wedge B\le_TA)$ is the set $\mathcal D_T$ of Turing degrees, partially ordered by $\le_T$. An automorphism of $(\mathcal D_T,\le_T)$ is a bijection $\pi:\mathcal D_T\to\mathcal D_T$ with

$$\mathbf a\le_T\mathbf b\iff\pi(\mathbf a)\le_T\pi(\mathbf b).$$

No definability, Borel or continuity hypothesis is imposed on $\pi$.

Formalization targets

Goal: Theorem 1.1

$$\forall\pi\in\operatorname{Aut}(\mathcal D_T,\le_T)\ \ \forall\mathbf a\in\mathcal D_T:\qquad \pi(\mathbf a)=\mathbf a.$$

The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.

Significance

Rigidity says that the order $\le_T$ alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.

Difficulty

Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as $\mathbf0''$, where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.

Formalization scope

• Oracles are ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values $0$ and $1$).
• Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting $\le_T$.
• The statement quantifies over all order isomorphisms, with no measurability or definability assumption, as in the paper.

A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on $2^{\mathbb N}$ and $\mathbb R$, and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.

Selected references

• OpenAI, Rigidity of the Turing degrees, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf
• T. A. Slaman, W. H. Woodin, Definability in Degree Structures, unpublished manuscript, 2005. https://math.berkeley.edu/~slaman/talks/sw.pdf
• T. A. Slaman, Global properties of the Turing degrees and the Turing jump, in Computational Prospects of Infinity, Part I, 2008. https://doi.org/10.1142/9789812794055_0002
• C. G. Jockusch, Jr., R. M. Solovay, Fixed points of jump preserving automorphisms of degrees, Israel J. Math., 1977. https://doi.org/10.1007/BF03007659
• A. Nerode, R. A. Shore, Reducibility orderings: theories, definability and automorphisms, Ann. Math. Logic, 1980. https://doi.org/10.1016/0003-4843(80)90004-2
• R. A. Shore, T. A. Slaman, Defining the Turing jump, Math. Res. Lett., 1999.
• R. A. Shore, Direct and local definitions of the Turing jump, J. Math. Log., 2007.
• B. Kjos-Hanssen, Permutations of the integers induce only the trivial automorphism of the Turing degrees, Bull. Symb. Log., 2018. https://doi.org/10.1017/bsl.2018.15
• A. M. Turing, Systems of logic based on ordinals, Proc. London Math. Soc., 1939. https://doi.org/10.1112/plms/s2-45.1.161

Motivation

Random 3-SAT, a conjunction of random three-literal clauses on $n$ variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near $4.267$. Once a limiting threshold $\alpha_3$ is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given $r$, outputs a rational within $2^{-r}$ of $\alpha_3$? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.

Timeline

• 1949. Specker constructs a bounded monotone computable sequence of rationals with a noncomputable limit.
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition about a size-dependent location (doi:10.1090/S0894-0347-99-00305-7).
• 2003, 2006. Hajiaghayi and Sorkin, and Kaporis, Kirousis and Lalas, prove the lower bound $3.52$ (arXiv:math/0310193).
• 2002–2006. Mézard, Parisi and Zecchina develop the cavity/survey-propagation picture; Mertens, Mézard and Zecchina predict $\alpha_3\approx4.267$.
• 2009. Díaz, Kirousis, Mitsche and Pérez-Giménez prove the upper bound $4.4898$.
• 2013. Bayati, Gamarnik and Tetali prove limits for normalized optimization values via sparse interpolation (doi:10.1214/12-AOP816).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture with the predicted value for all large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and the existence of limiting thresholds for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for the satisfiability conjecture belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of $\alpha_3$, beyond existence.

Setting

For $n\ge3$, a proper random 3-clause chooses three distinct variables uniformly from $x_1,\dots,x_n$ and gives each an independent fair sign. Let $\Phi(n,m)$ be the conjunction of $m\ge0$ independent such clauses (sampled with replacement from the $8\binom n3$ possibilities; the empty formula is satisfiable) and

$$p(n,m)=\mathbb P\{\Phi(n,m)\ \text{is satisfiable}\}.$$

A real $\alpha$ is computable if a single algorithm, on input $r$, halts with a rational $q_r$ satisfying $|q_r-\alpha|\le2^{-r}$.

Formalization targets

Goal: Theorem 1.1

There is $\alpha_3\in(0,\infty)$ such that for every fixed real $a\ge0$

$$\lim_{n\to\infty}p(n,\lfloor an\rfloor)=\begin{cases}1,&a<\alpha_3,\\0,&a>\alpha_3,\end{cases}$$

and one finite deterministic Turing machine, on input $1^r$, halts with a rational $q_r$ with $|q_r-\alpha_3|\le2^{-r}$, using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.

Significance

The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of $\alpha_3$ (Theorem 4.4) for the same proper-clause model.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite $n$ certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above $\alpha_3$ some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.

Formalization scope

• ProperClause n k is Fin n → Option Bool with exactly $k$ defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to $p(n,m)$.
• MainStatement asserts $\exists\,\alpha>0$ with the two strict-side limits at $m=\lfloor an\rfloor$, a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and $|q_r-\alpha|\le2^{-r}$ for all $r$.
• The input is a natural number rather than a unary string, which is equivalent for computability; the $r=0$ case is a harmless extra requirement.
• Nothing is asserted at $a=\alpha_3$.

Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.

Selected references

• OpenAI, Computing the Random 3-SAT Threshold, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• M. Hajiaghayi, G. B. Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52, preprint, 2003. https://arxiv.org/abs/math/0310193
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. of Math., 2013. https://doi.org/10.4007/annals.2013.177.1.8
• E. Specker, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symbolic Logic, 1949.

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, 441–450. https://doi.org/10.1287/moor.12.3.441
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.