1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

Motivation

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.

Say $\alpha$ is $k$-collapsible if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, collapsible if it is $1$-collapsible, and eventually collapsible if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and degree $3$ is open. That one-step cubic case is this mission's goal.

Setting

Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a depressed cubic

$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$

with discriminant $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is totally real (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as

$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$

and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant

$$\tau = e^2/d^3$$

determines the problem up to scaling: the search space is one rational parameter, not two.

Formalization targets

Goal — every cubic algebraic number is collapsible

$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$

This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.

Supporting targets

The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:

1. the product criterion — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. affine invariance, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two sufficient conditions: square discriminant, and the power-family condition subsuming it;
4. three obstructions: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.

The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.

Significance

A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.

The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.

Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.

Difficulty

The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.

Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces

$$\deg f \ \ge\ \pi/\psi.$$

As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.

Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.

In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.

Formalization scope

Representation. IsSplit f says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.

Ruling out a trivialisation. Collapsible places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.

Conventions in the archimedean milestones. In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.

In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.

Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.

Selected references

• Griffin Macris, List of open problems, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
• Miles, Collapsible algebraic numbers, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.

Motivation

Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$-sphere.

This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.

Setting

Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$. Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$. The condition that $L$ is a simplicial $4$-sphere means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$.

For each face $\sigma\in L$, assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$. The associated moment-angle complex is

$$\mathcal Z_L =\bigcup_{\sigma\in L} \prod_{i=1}^{m}Y_i(\sigma), \qquad Y_i(\sigma)= \begin{cases} D^2,&i\in\sigma,\\ S^1,&i\notin\sigma. \end{cases}$$

The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$, the mission uses total integral singular homology

$$H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)$$

as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$.

Formalization targets

Arbitrary torsion in one moment-angle manifold

For every finitely generated abelian group $G$, prove that there are an integer $m$ and a simplicial complex $L$ on Fin m such that $|L|\cong S^4$ and there are injective homomorphisms

$$G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z), \qquad G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).$$

The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.

Significance

The theorem gives a universality statement for moment-angle manifolds over simplicial $4$-spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.

Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.

Difficulty

The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.

There is also a substantial representation boundary between combinatorics and topology. The face data of $L$, the union of disk-circle products, the homeomorphism $|L|\cong S^4$, and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.

Formalization scope

Lean represents $L$ using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$-sphere.

The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in $\mathbb Z$, and total homology is a direct sum over all natural degrees.

The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.

Selected references

• Yang Han and Keke Li, Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion, International Mathematics Research Notices 2026(4), 1--7, 2026. DOI
• A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces, Advances in Mathematics 225(3), 2010, 1634--1668. DOI

Motivation

Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.

This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.

Suggested attack route

Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.

Formalization scope

The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Durt et al., review of MUBs

Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Which laws imply which others, over all magmas or over finite magmas only, is the question the Equational Theories Project studies at scale. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The project's December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $\alpha$ with a total binary operation $\diamond:\alpha\times\alpha\to\alpha$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

$$\forall x,y\in\alpha,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$

The condition E255 means

$$\forall x\in\alpha,\quad x=((x\diamond x)\diamond x)\diamond x.$$

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$, the left translation (left multiplication) map is $L_y(x)=y\diamond x$. A fixer of $x$ is an element $y$ with $y\diamond x=x$; it acts on $x$ from the left. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element. The left orbit of $x$ is the forward orbit $x,L_x(x),L_x^2(x),\ldots$ of $x$ under its own left translation.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $\alpha$ satisfying E677, the first supporting statement is

$$\forall y\in\alpha,\quad L_y\text{ is bijective}.$$

The second supporting statement determines any fixer:

$$\forall x,y\in\alpha,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$

The third supporting statement is the backward recurrence

$$\forall x,y\in\alpha,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$

These three statements are blueprint Lemma 13.1(i)–(iii) and are Proved on this platform. The following fixer-existence assertion is the same obligation as E255 under E677 and finiteness (blueprint Lemma 13.2); it is a reduction node, not a milestone:

$$\forall x\in\alpha,\quad\exists y\in\alpha,\quad y\diamond x=x.$$

The mission goal is

$$\forall\text{ finite magmas }\alpha,\quad \operatorname{E677}(\alpha)\ \Longrightarrow\ \operatorname{E255}(\alpha).$$

For finite E677 magmas, E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$; from any fixer $y$ of $x$, Lemma 13.1(ii) gives $y=(x\diamond x)\diamond x$ and hence E255 at $x$. Each direction is one line, so fixer existence is not a strictly weaker milestone.

Three open sub-goals come from the case split in the accepted reduction sketches for the fixer-existence node. Sub-goal 1 is orbit-local: for a fixed $x$, if two elements of the left orbit of $x$ have equal right products by $x$, then they are equal or $x$ has a fixer. Sub-goal 2 concerns the case of exactly one element $A$ outside the left orbit of $x$, with $x$ having no fixer: a right-translation collision $c\diamond x=A\diamond x$ between an orbit point $c$ and $A$ must propagate to the orbit successor $x\diamond c$. Sub-goal 3 assumes $x\diamond x\ne x$ and at least two elements outside the left orbit: if right translation by $x$ sends an orbit point outside the orbit, then $x$ has a fixer. Sub-goal 3 is not a smaller case of the goal. If it holds for every finite E677 magma, the mission goal follows by a product construction (item 1 of Known reductions and results below), and the mission goal gives Sub-goal 3 because E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$. So a proof of Sub-goal 3 alone proves the goal, and a route through Sub-goals 1 and 2 still needs Sub-goal 3. The D4 milestones specialize Sub-goal 1 to a left orbit of exact period four; D4.0, D4.1, D4.2 and D4.4a–e are Proved, and the series is open at D4.3 and its five branch closeouts D4.3a–e. One conditional result (E677 together with conjugacy-closed left translations implies E255; Padilla, 2026) is Proved on this platform. The counterexample milestone is the disproof target. None of the displayed statements restricts the cardinality to a tested range.

In the authors' repository, Sub-goal 1 is called Piece 1, the unique-outsider case containing Sub-goal 2 is called Gap 1, and the case of Sub-goal 3 is called Gap ≥ 2; those names appear in some theorem sources and file names.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left translation property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left translation conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left translation map alone does not state that a fixer exists.

Because the implication fails for infinite magmas, E255 is not an equational consequence of E677, so any proof must use finiteness in an essential way. The blueprint's linear and linear-extension constructions cannot produce a finite counterexample (blueprint Lemmas 13.3 and 13.4); community members have formalized on this platform the scalar-coefficient case of the linear lemma, the Type I and Type II affine families, and the linear-extension lemma (see the discussion thread).

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

The definition bundle FiniteMagmaE677 provides E677, E255, HasFixerAt (existence of a fixer of $x$), InLeftOrbit (membership in the left orbit of $x$) and OrbitRightCollisionOrFixer. Three further bundles, FiniteMagmaE677_seventh_element_growth, FiniteMagmaE677_d4_first_return and FiniteMagmaE677_sswap_renewal, hold the period-four packet types used by the D4 milestones.

Status (2026-10-17 UTC). Proved on this platform: Lemma 13.1(i)–(iii), the Sub-goal 1 and Sub-goal 2 support lemmas, D4.0, D4.1, D4.2, D4.4a–e, the conditional conjugacy-closure theorem, and three further conditional theorems by omegaestable (existential row transport, parametrized row transport, left-parameter transport; see the discussion thread). Open: Sub-goals 1–3, D4.3 with D4.3a–e, and the counterexample target. Community members have also formalized the blueprint's 496-element non-right-cancellative E677 magma (see the discussion thread).

Welcome contributions: a proof of any open sub-goal or D4.3 branch (a proof of Sub-goal 3 proves the goal; see item 1 below); a proof sketch that reduces an open leaf to new lemmas; a concrete operation table on Fin n proving finite_counterexample, which would make the main theorem false.

Known reductions and results from the captain's repository

These results are in the captain's private repository and are not on this platform. Readers cannot open that repository, so each statement is given in full. For a Lean result, the axioms that Lean reports are listed.

1. Sub-goal 3 alone gives the mission goal. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). Let $K$ be the E677 magma on $\{0,\dots,6\}$ whose rows $a\diamond 0,\dots,a\diamond 6$ for $a=0,\dots,6$ are 6304251, 5620143, 2063514, 1256430, 0431625, 3145062, 4512306 (file db/7/1 of the public collection memoryleak47/eq677). The left orbit of $0$ in $K$ is $0,6,1,3,4,2$, the only element outside it is $5$, and the orbit point $L_0^2(0)=1$ has $1\diamond 0=5$. Let $\alpha$ be a finite E677 magma and $x\in\alpha$ with $x\diamond x\ne x$. Then $\alpha\times K$ with the componentwise operation satisfies E677 (product_e677 on this platform), and the second coordinates of the left orbit of $X=(x,0)$ are the left orbit of $0$ in $K$. So $X\diamond X\ne X$; $(x,5)$ and $(x\diamond x,5)$ are two distinct elements outside the left orbit of $X$; and $L_X^2(X)\diamond X$ has second coordinate $5$, so it is outside the orbit. These are the hypotheses of Sub-goal 3 at $X$, and a fixer $(y_1,y_2)$ of $X$ gives the fixer $y_1$ of $x$. If $x\diamond x=x$, then $x$ is a fixer of $x$. So Sub-goal 3, for every finite E677 magma, gives a fixer of every element of every finite E677 magma, and E255 follows by Lemma 13.1(ii). Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, lean/E677/Transport.lean, e677_fixer_exists_of_d7_leaf. The hypothesis of that theorem is the repository's D7TwoOutsiderRightDipPacket (lean/E677/Spine/D7NonFullCore.lean). Each part of it and the matching hypothesis of Sub-goal 3 give each other in one step: $\neg\exists i,\ a=L_x^i(x)$ against $\forall n,\ a\ne L_x^n(x)$ for an outsider, and an escaping orbit point $L_x^k(x)$ against its index $k$. The conclusion is the same formula $\exists y,\ y\diamond x=x$.

2. Normal form of a counterexample. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). Write $D(z)=((z\diamond z)\diamond z)\diamond z$. A congruence is a reflexive, symmetric and transitive relation $\theta$ such that $a\,\theta\,b$ and $c\,\theta\,d$ imply $(a\diamond c)\,\theta\,(b\diamond d)$. If some finite E677 magma fails E255, then for some $n$ there are an E677 operation on $\{0,\dots,n-1\}$ and a point $z$ with $D(z)\ne z$ such that every element is a $\diamond$-term in $z$ alone, and every congruence that relates two distinct elements also relates $z$ and $D(z)$. The proof takes the least such $n$; otherwise a submagma or a quotient would be a smaller counterexample. Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, lean/E677/CriticalCore.lean, E677Crit.exists_pairCritical_counterexample. By E677Crit.not_pairCritical_prod_of_q_ne in the same file (no axioms), if two magmas each have at least two elements, no point of their product at which E255 fails has the congruence property. So a counterexample in this normal form is never such a product, and the construction of item 1 never produces one. Axiom record: docs/current/critical-core-audit-2026-08-03.md.

3. A refuted intermediate statement. NEGATIVE; computational (exhaustive check of one explicit table, run twice with independent encodings; not kernel-checked). Let $S(x)$ be the closure of the left orbit of $x$ under $z\mapsto z\diamond x$. The repository's gate CP asserted: in a finite E677 magma, if the hypotheses of Sub-goal 3 hold at $x$ and $z\mapsto z\diamond x$ is not injective on $S(x)$, then the left orbit of $x$ has minimal period $7$. Let $M$ be the E677 magma of order $77$ in file db/77/65 of the same collection. In $M\times K$ (order $539$; E677 checked on all $539^2$ pairs), the point $(0,0)$ satisfies these hypotheses, and its left orbit has minimal period $\operatorname{lcm}(7,6)=42$. The point $(0,0)$ has the fixer $(76,4)$, so this is not a counterexample to E255, and it refutes CP only in the form without a no-fixer hypothesis. With that hypothesis added, the construction of item 1 derives from CP a fixer of every element of every finite E677 magma, and hence the mission goal (PROVEN, Lean: lean/E677/Transport.lean, e677_fixer_exists_of_gate_cp; axioms propext, Classical.choice, Quot.sound). Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, docs/current/dead-ends/gap-ge-2.md, entry D7-6.

4. $\Phi(x)=(x\diamond x)\diamond x$ is not injective in general. EMPIRICAL. In the 2026-09-27 snapshot of the community database (4091 tables), every table satisfies E255, and $\Phi$ is not injective in 1107 of them; the smallest such order is $7$. In one table of order 7, row 6 is the identity row, so $6$ is a fixer of every $x$ and Lemma 13.1(ii) gives $\Phi(x)=6$ for every $x$. So global injectivity of $\Phi$ is not a usable intermediate target. Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, docs/professor-phi-injectivity.md, correction of 2026-10-14.

5. Solver ledger for one period-four configuration. EMPIRICAL, incomplete. One CNF encoding of a period-four collision configuration of Sub-goal 1 on 11 elements, with added derived constraints, is split into 37 cubes. Twenty cubes are UNSAT, each with an LRAT proof accepted by the native drat-trim LRAT checker (unverified C code, not a kernel-checked proof). The other 17 have no recorded result; each was UNKNOWN under an earlier 300-second limit. No conclusion about Sub-goal 1 follows. Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, docs/current/e677-closure-plan-2026-08-04.md, section "Live strict PiQD campaign for the 37-cube n = 11 diagnostic".

6. Period-four refinements. PROVEN in the private repository; not ported to this platform (Lean; axioms propext, Classical.choice, Quot.sound). A repository theorem refines the five branches of the D4.2 first-return packet and keeps every case. Write $q=c_2\diamond x$. In the R-through-one branch (the repository's name), each outcome is a fixer of $x$, a strict decrease of a finite contact budget, a new $L_x$-cycle disjoint from the elements already accounted for (with its exact size), or a closed trace of $L_q^{-1}$ that is reduced to two phase-contact families. In the two unswapped S branches, each outcome is a fixer of $x$, a decrease by one of the number of unmarked phases on the $L_x$-cycle of $q$, or a new disjoint $L_x$-cycle with its exact size. These results do not close D4.3 or any of D4.3a–e, because the outcomes are not yet combined into one state with a strictly decreasing well-founded measure. Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, lean/E677/Spine/Piece1D4RefinedFirstReturn.lean, e677_d4_q_refinedFirstReturnPacket_of_firstReturnPacket; closure plan docs/current/e677-closure-plan-2026-08-04.md, sections "D4 R/S finite renewal integration" and "Production-interface correction".

7. Whole-orbit form of the q-subdiagonal identity. PROVEN in the private repository; not ported to this platform (Lean; axioms propext, Classical.choice, Quot.sound). In a finite E677 magma, fix $x$ and write $c_k=L_x^k(x)$ and $q_k=c_k\diamond((c_{k+1}\diamond c_k)\diamond c_{k+1})$. If $q_i=q_j$ implies $c_i=c_j$ for all $i,j$, then right translation by $x$ is injective on the left orbit of $x$, so Sub-goal 1 holds at $x$ through its first alternative. Conversely, if right translation by $x$ is injective on the left orbit of $x$, then $q_i=q_j$ implies $c_i=c_j$ for all $i,j$. Sub-goal 1 support (b) and (c) are the pointwise statements. So a no-repeat property of the $q$-subdiagonal is not a weaker target than injectivity of right translation on the orbit. Source: Adam McKenna, The Missing Pair (private repository), revision 4100763b, lean/E677/CoreBase.lean, e677_orbitQ_subdiag_injective_iff_Rx_injective_on_orbit.

Selected references

• Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
• The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.4, chapter, accessed September 7, 2026 and October 13, 2026.
• J. I. Padilla (GitHub: omegaestable), Prove E677 implies E255 under left translation conjugacy closure, Equational Theories Project pull request #1518, 2026 (closed without merge by its author on 2026-10-13; the theorem is Proved on this platform), pull request.

Motivation

Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is unsolved.

What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.

• Cyclic and, more generally, finite abelian groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
• Symmetric and alternating groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
• Every finite solvable group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219), obtained by solving embedding problems.
• Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — every finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
• Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.

Setting

Fix a field $K$ and a group $G$. A Galois realization of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism

$$G \;\cong\; \mathrm{Gal}(L/K),$$

where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is realizable over $K$, written IsRealizable K G, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.

Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.

Formalization targets

Goal — the inverse Galois problem

$$\text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G.$$

The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.

Milestones — the known partial results

$$G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K,$$ $$G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0),$$ $$G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}.$$

The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.

Significance

The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group $M_{23}$ show.

Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.

Difficulty

The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover over $\mathbb{Q}$ rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.

A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.

Formalization scope

The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:

• IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.
• The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
• The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
• $\mathrm{Sym}(S)$ is Equiv.Perm S for a finite type $S$, and $A_n$ is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.
• Solvability is Group.IsSolvable.

The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.

Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.

Selected references

• Inverse Galois problem, Wikipedia. https://en.wikipedia.org/wiki/Inverse_Galois_problem
• I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219.
• C. U. Jensen, A. Ledet, N. Yui, Generic Polynomials: Constructive Aspects of the Inverse Galois Problem, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
• G. Malle, B. H. Matzat, Inverse Galois Theory, Springer Monographs in Mathematics, 1999.
• R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, 17T7 is a Galois group over the rationals, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857

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

Deciding whether a system of real polynomial equations, inequations and inequalities has a solution is the basic feasibility question behind nonconvex quadratic programming, polynomial optimization, robustness analysis in control, and combinatorial relaxations. Over the complex numbers, Hilbert's Nullstellensatz turns infeasibility into an algebraic identity whose bounded-degree instances are found by linear algebra. Over the reals this fails: $x^2+1=0$ has no real solution, yet $1$ is not in the ideal generated by $x^2+1$.

The real substitute is the Positivstellensatz of Stengle (Stengle 1974; see Bochnak–Coste–Roy, Real Algebraic Geometry, Theorem 4.4.2): a real polynomial system is infeasible exactly when an identity $f+g^2+h=0$ holds, with $f$ built from sums of squares and the inequality constraints, $g$ a product of the inequation polynomials and $h$ in the ideal of the equations. Parrilo (2003), building on his thesis (2000), observed that once the degrees are bounded, the search for such an identity is a semidefinite program (SDP), because a polynomial is a sum of squares exactly when it has a positive semidefinite Gram matrix. This yields a hierarchy of SDPs that is sound at every level and complete in the limit, and it is the origin of the sum-of-squares (SOS) method used throughout polynomial optimization.

Timeline:

• 1974: Stengle proves the Positivstellensatz for semialgebraic sets over real closed fields.
• 1995: Choi, Lam and Reznick analyze the Gram matrix method for sums of squares.
• 2000–2003: Parrilo (thesis; Math. Program. Ser. B 96) formulates bounded-degree Positivstellensatz refutations as SDPs (Theorem 5.1); Lasserre (2001) develops the dual moment approach independently.

Setting

Write $\mathbb R[x_1,\dots,x_n]$ for real polynomials in $n$ variables. Fix three finite, possibly empty, families: $f_1,\dots,f_s$ (inequalities), $g_1,\dots,g_t$ (inequations), $h_1,\dots,h_u$ (equations). They define the basic semialgebraic set

$$K=\{x\in\mathbb R^n \mid f_j(x)\ge 0,\ g_k(x)\ne 0,\ h_\ell(x)=0\ \text{for all } j,k,\ell\}.\qquad(4.4)$$

A cone of $\mathbb R[x_1,\dots,x_n]$ is a subset closed under addition and multiplication that contains every square $a^2$; $P(S)$ is the smallest cone containing $S$, and $P(\emptyset)$ is the set of sums of squares. $M$ is the multiplicative monoid generated by the $g_k$ (with the empty product $1$), and $I$ is the ideal generated by the $h_\ell$.

For a degree bound $D$, let $z$ be the vector of all monomials $x^\alpha$ of total degree at most $D$; it has $\binom{n+D}{D}$ entries. For a real matrix $Q$ indexed by these monomials, the Gram polynomial is $z^TQz=\sum_{\alpha,\beta}Q_{\alpha\beta}x^\alpha x^\beta$.

The degree-$d$ Positivstellensatz SDP $\mathrm{SDP}_d$: with $G=\sum_k\deg g_k$ and $N(d)=d(2G+1)$, find positive semidefinite matrices $Q_T$ over the monomials of degree at most $N(d)$, one for each $T\subseteq\{1,\dots,s\}$, and polynomials $q_\ell$ of degree at most $2N(d)$, such that

$$\sum_{T}(z^TQ_Tz)\prod_{j\in T}f_j+\Big(\prod_{k=1}^t g_k^{2d}\Big)^2+\sum_{\ell=1}^u q_\ell h_\ell=0 .$$

Its unknowns are finitely many real numbers, the constraint is linear in them, and the matrices are constrained to be positive semidefinite.

Formalization targets

Goal: Theorem 5.1

$$\big(\forall d,\ \mathrm{SDP}_d\ \text{feasible}\Rightarrow K=\emptyset\big)\quad\text{and}\quad\big(K=\emptyset\Rightarrow\exists d_0\ \forall d\ge d_0,\ \mathrm{SDP}_d\ \text{feasible}\big).$$

The first half says every feasible point is a refutation; the second says the hierarchy is complete once the degree bound is large enough. No bound on $d_0$ is asserted, matching the paper.

Milestones

• Theorem 4.6, $2\Rightarrow1$: an identity $f+g^2+h=0$ with $f\in P$, $g\in M$, $h\in I$ forces $K=\emptyset$.
• A positive semidefinite Gram matrix gives a sum of squares (§3.2).
• Theorem 4.6, $1\Rightarrow2$ (Stengle's Positivstellensatz): $K=\emptyset$ forces such an identity.
• $P(\emptyset)$ is the set of sums of squares and the smallest cone; the finite-generator form $P(S)=\{p+\sum_i q_ib_i\}$; the squarefree form $\sum_T p_T\prod_{j\in T}f_j$ of the cone used in the proof of Theorem 5.1.
• A sum of squares of degree at most $2d$ has a positive semidefinite Gram matrix over the monomials of degree at most $d$; Theorem 3.3 combining both directions with the size $\binom{n+d}{d}$; the count $\binom{n+d}{d}$ of the monomial vector.

Significance

Theorem 5.1 is the statement that makes Positivstellensatz certificates computable: it converts an existence theorem of real algebraic geometry into a sequence of convex feasibility problems, each solvable by interior-point methods, and any solution is an exact proof of infeasibility. Lower bounds in polynomial optimization (Example 5.4), the copositivity tests of §7.5, SOS relaxations for MAX-CUT and stable sets, and Lyapunov-function searches in control are all instances of this scheme.

The paper proves only the soundness direction of the Positivstellensatz and cites the converse. A complete formal development therefore contains the first machine-checked statement chain from Stengle's theorem to the SDP hierarchy. To the best of current searches, neither Mathlib nor Prove2Me contains the real Positivstellensatz, the Gram matrix characterization of sums of squares, or the monomial count; Mathlib has sums of squares in rings (IsSumSq), positive semidefinite matrices, and the complex Nullstellensatz.

Difficulty

The soundness half is elementary. Completeness rests on Stengle's Positivstellensatz, whose standard proofs pass through real closed fields, orderings of rings and the Tarski–Seidenberg transfer principle, none of which is available in Mathlib in usable form. A tempting shortcut, proving completeness by reasoning only about $\mathbb R$-points, does not work: the certificate must be an algebraic identity, and points cannot produce it.

A second, smaller difficulty is degree bookkeeping. Each level of the hierarchy has a fixed shape (the exponent of the $g_k$ and the degree of every multiplier are tied to $d$), while a certificate supplied by the Positivstellensatz has arbitrary degrees and exponents. A Gram representation also needs a degree bound on every square in a sum of squares, not only on the sum.

Formalization scope

• Polynomials are MvPolynomial (Fin n) ℝ; $n,s,t,u$ are arbitrary natural numbers, including $0$; the families are indexed by Fin s, Fin t, Fin u. The set (4.4) lives in $\mathbb R^n$ = Fin n → ℝ.
• $P(S)$ is the smallest set closed under $+$, $\cdot$ and containing all squares (Definition 4.5), an inductive predicate. Mathlib's RingPreordering is not used: it excludes $-1$, which an infeasible system's cone typically contains.
• Sums of squares are IsSumSq; positive semidefiniteness is Matrix.PosSemidef (symmetric, which is the paper's $Q\in\mathcal S^n$); $M$ is Submonoid.closure, $I$ is Ideal.span.
• The meta-claim "the search … can be done using semidefinite programming" is the definition of $\mathrm{SDP}_d$: finitely many PSD Gram matrices indexed by a finite type of monomials, and ideal multipliers of bounded total degree. The degree choices ($m=d$ in $g=\prod g_k^{2m}$; multiplier degree $d_2=2d(2G+1)$) fill the freedom the proof leaves and satisfy its printed bounds $d_2\ge d$, $d_2\ge\deg g$. "Large enough" is $\exists d_0\,\forall d\ge d_0$.
• A formalization without the degree bounds or with an infinite index type would make $\mathrm{SDP}_d$ equivalent to Theorem 4.6 item 2 and is ruled out; so is a goal stated for a fixed $n$, for empty families only, or with soundness only at large $d$.
• Needed infrastructure: Stengle's Positivstellensatz over $\mathbb R$ (real closed field theory or a direct proof), the Gram matrix correspondence, and degree lemmas for sums of squares. The Positivstellensatz and the Gram correspondence are reusable far beyond this mission; contributions toward either are welcome.

Selected references

• P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Math. Program. Ser. B 96 (2003) 293–320. https://doi.org/10.1007/s10107-003-0387-5
• G. Stengle, A Nullstellensatz and a Positivstellensatz in semialgebraic geometry, Math. Ann. 207 (1974) 87–97. https://doi.org/10.1007/BF01362149
• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Theorem 4.4.2. https://doi.org/10.1007/978-3-662-03718-8
• M. D. Choi, T. Y. Lam, B. Reznick, Sums of squares of real polynomials, Proc. Sympos. Pure Math. 58 (1995) 103–126. https://doi.org/10.1090/pspum/058.2/1327293
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11 (2001) 796–817. https://doi.org/10.1137/S1052623400366802

Why noisy secrets need sketches

Biometric readings, physical unclonable functions and typed passphrases share two defects as cryptographic keys: they are not uniformly distributed, and they are never reproduced exactly. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; preprint arXiv:cs/0602007v4) introduced the secure sketch to handle the second defect without destroying what entropy the secret has. A secure sketch publishes a string $s$ from which any reading close to the original recovers the original exactly, while the original keeps a guaranteed amount of min-entropy given $s$. Many sources of noise are not substitutions but insertions and deletions: keystroke sequences, sequenced DNA, and any reading whose alignment drifts. For these the relevant distance is the edit distance, and §7 of the paper gives a secure sketch for it.

This mission formalizes that construction: Theorem 7.5 (p. 27), together with the results it is assembled from, PinSketch for set difference (Theorem 6.3, p. 23, with the BCH decoding argument of Appendix E) and the shingling embedding (Lemma 7.3, p. 25), glued by Lemma 4.7 (p. 15).

Setting

All logarithms are base 2. A random variable is identified with its distribution. The min-entropy of $W$ is $\mathbf H_\infty(W) = -\log \max_w \Pr[W = w]$, and the average min-entropy of $W$ given $I$ is $\tilde{\mathbf H}_\infty(W \mid I) = -\log \sum_i \max_w \Pr[W = w \wedge I = i]$.

Let $\mathcal M$ be a set with an integer-valued distance $\mathrm{dis}$. An average-case $(\mathcal M, m, \tilde m, t)$-secure sketch is a pair of randomized procedures $(\mathsf{SS}, \mathsf{Rec})$ such that $\mathsf{Rec}(w', \mathsf{SS}(w)) = w$ whenever $\mathrm{dis}(w, w') \le t$, and $\tilde{\mathbf H}_\infty(W \mid \mathsf{SS}(W), I) \ge \tilde m$ for every pair $(W, I)$ with $\tilde{\mathbf H}_\infty(W \mid I) \ge m$. The difference $m - \tilde m$ is the entropy loss.

Three spaces occur.

1. $\mathrm{Edit}_{\mathcal F}(n)$: strings of length $n$ over a finite alphabet $\mathcal F$ of $F$ letters, with distance the smallest number of character insertions and deletions turning one string into the other.
2. $\mathrm{SDif}(\mathcal U)$: all subsets of a finite universe $\mathcal U$, with distance $|w \triangle w'|$.
3. For PinSketch, $\mathcal U = GF(2^\mu)^*$, of size $n = 2^\mu - 1$. A subset $w$ has syndrome entries $s_i(w) = \sum_{x \in w} x^i$, computed in the field. PinSketch publishes $(s_1, s_3, \dots, s_{2t-1})$.

A $c$-shingle of a string is a length-$c$ consecutive substring, and the $c$-shingling $\mathrm{SH}_c(w) \subseteq \mathcal F^c$ is the set of all of them. A map $f : \mathcal M_1 \to \mathcal M_2$ is a $(t_1, t_2, \lambda)$-biometric embedding with recovery information $g$ if it maps distance $\le t_1$ to distance $\le t_2$, $g$ takes at most $2^\lambda$ values, and $w$ is determined by $(f(w), g(w))$.

Formalization targets

Goal: Theorem 7.5

For every finite alphabet $\mathcal F$ with $F$ letters, all $n, c, t \in \mathbb N$ with $1 \le c \le n$ and every real $m$, there is an average-case secure sketch

$$\Big(\mathrm{Edit}_{\mathcal F}(n),\ m,\ m - \big\lceil \tfrac nc \big\rceil \log_2(n - c + 1) - (2c - 1)\,t\,\lceil \log(F^c + 1) \rceil,\ t\Big).$$

Milestones

1. Set difference. Theorem 6.3: PinSketch is an average-case $(\mathrm{SDif}(\mathcal U), m, m - t\log(n+1), t)$ secure sketch. On the way:
   • the Appendix E identity $s_{2i} = s_i^2$;
   • the key equation $S(z)\sigma(z) \equiv \omega(z) \bmod z^\delta$;
   • the uniqueness of $\omega/\sigma$ among low-degree solutions;
   • Lemma 6.2: a word of weight $\le (\delta - 1)/2$ is determined by its first $\delta - 1$ syndromes;
   • step 4 of Construction 6: decoding returns $w \triangle w'$.
2. Edit distance into set difference. Lemma 7.3: $\mathrm{SH}_c$ is an average-case $(t_1, (2c-1)t_1, m_1, m_1 - \lceil n/c \rceil \log_2(n - c + 1))$ biometric embedding. Its strengthening: $\mathrm{SH}_c$ has recovery information $g_c$ with $\lambda = \lceil n/c \rceil \log_2(n - c + 1)$.
3. Composition. Lemma 4.7: an embedding with recovery information turns an average-case sketch on $\mathcal M_2$ for entropy $m_1 - \lambda$ into one on $\mathcal M_1$ for entropy $m_1$, with the same residual entropy.

Significance

Theorem 7.5 gives a secure sketch for the edit metric whose entropy loss is, for a good choice of $c$, about $2.38\,(t \log F)^{1/3}(n \log n)^{2/3}$ (p. 26). This is sublinear in $n$ for $t$ up to nearly linear, and for large $t$ it improves on the low-distortion embedding approach of §7.1. Combined with a strong extractor it yields fuzzy extractors for edit distance (Theorem 7.4). PinSketch is itself the standard set-difference sketch, and Lemma 4.7 is a general transfer principle between metrics.

All results here are proved in the paper. None has a machine-checked proof that we know of. A complete development would also formalize a fragment of BCH decoding over $GF(2^\mu)$, the syndrome-uniqueness theorem for binary BCH codes, and a combinatorial lemma on how insertions and deletions act on shingle sets. Each is reusable outside this mission.

Difficulty

There are two hard steps.

The first is Lemma 6.2. That a low-weight word is determined by $\delta - 1$ power sums is a statement about Vandermonde systems in characteristic 2, where the even power sums carry no new information. Newton's identities, the usual characteristic-zero route from power sums to elementary symmetric functions, fail there because they divide by integers that vanish in characteristic 2. The paper argues through the error-locator and error-evaluator polynomials instead.

The second is the distance clause of Lemma 7.3. An edit path between two strings of length $n$ passes through strings of other lengths, so a per-step bound on the shingle sets must hold for strings of every length, including lengths below $c$.

The entropy statements involve average min-entropy over arbitrary auxiliary variables, and each needs the chain-rule bound of Lemma 2.2(b) in average-case form.

Formalization scope

• Laws and kernels. Random variables are PMFs, and randomized procedures are kernels M → PMF S. The auxiliary variable of every average-case statement ranges over every ι : Type, not only finite types. Average min-entropy uses the joint form above. "Min-entropy $m$" means $\ge m$, and $m$ is real.
• The field. The paper's $GF(2^m)$ is any finite field K of characteristic 2, and its degree is renamed $\mu$ because $m$ denotes min-entropy. Appendix E's large field $\mathcal F$ is this K, distinct from §7's alphabet $\mathcal F$. Only binary words are formalized, as subsets (Finset Kˣ); the $q$-ary generality of Lemma E.1 is not.
• The key equation. $\omega(z)$ is written without division, congruence mod $z^\delta$ is divisibility by $X^\delta$, and the ratio identity is cross-multiplied.
• Edit distance. It reuses the published weighted edit distance MasekPaterson.Shared.editDist with cost 1 per insertion or deletion and 2 per replacement, which equals the insertion/deletion count.
• Shingling and $g_c$. Shingling is defined for strings of all lengths. $g_c$ is the concrete function of the proof, with 0-based indices.
• Explicit hypotheses.
  • The Appendix E uniqueness statement takes the BCH designed distance to satisfy $1 \le \delta$; at $\delta=0$ its congruence is vacuous and the conclusion can fail.
  • $1 \le c \le n$, which the paper leaves implicit, is assumed in Lemma 7.3 and Theorem 7.5.
  • $\epsilon$ is dropped from Theorem 7.5, where it does not occur in the conclusion.
  • $\lceil \log(F^c + 1) \rceil$ is Nat.clog 2 (F ^ c + 1).
• Misprints, read as corrected.
  • In Definition 7, $f(w_2)$ is read as $f(w_1')$.
  • In Lemma 4.7, $\mathsf{Rec}(w', s)$ is read as $\mathsf{Rec}(f(w'), s)$.
  • In Appendix E, $w'(z)$ is read as $\omega'(z)$.
• Efficiency. Every claim of efficiency or running time (Lemma 6.2, Theorem 6.3, Theorem 7.5) is dropped: Mathlib has no complexity substrate, and no vacuous substitute is used.
• Excluded trivializations. The distance is the insertion/deletion distance, not the Hamming distance on length-$n$ strings (a different and easier problem). It is not a degenerate cost that is identically 0: insertion and deletion each cost 1.
• Not posed here. Lemma 2.2(b) and Lemma 3.1 are posed in the companion mission on Hamming fuzzy extractors. Proofs that need them may restate them.

Contributions are welcome on any milestone. The BCH part (Appendix E, Lemma 6.2) and the shingling part (Lemma 7.3) are independent.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. https://doi.org/10.1137/060651380 ; arXiv:cs/0602007v4, https://arxiv.org/abs/cs/0602007
• J. H. van Lint, Introduction to Coding Theory, 2nd ed., Springer, 1992 (BCH codes and their decoding; the reference [vL92] of Appendix E).
• A. Z. Broder, On the resemblance and containment of documents, Compression and Complexity of Sequences, IEEE, 1997 (shingling). https://doi.org/10.1109/SEQUEN.1997.666900
• W. J. Masek, M. S. Paterson, A faster algorithm computing string edit distances, J. Comput. System Sci. 20(1):18–31, 1980 (the weighted edit distance reused here). https://doi.org/10.1016/0022-0000(80)90002-1