Completed

Algebraic Geometry Representation Theory·Captain: wurtle

Quadratic stabilization of the canonical Foulkes--Howe mapResearch Paper

Motivation: plethysm, Foulkes' conjecture and the canonical map

Plethysm — decomposing $\operatorname{Sym}^a(\operatorname{Sym}^b V)$ into irreducible $\mathrm{GL}(V)$ -representations — is one of the oldest open problems in the representation theory of the general linear group, and it is central to geometric complexity theory, where the coordinate rings of Chow varieties of products of linear forms control lower-bound arguments. Foulkes' conjecture (1950) predicts that for $a\le b$ there is a $\mathrm{GL}(V)$ -equivariant injection $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$ . A natural candidate is supplied by a specific map, the canonical Foulkes–Howe map $\mu_{a,b,V}:\operatorname{Sym}^b(\operatorname{Sym}^aV)\to\operatorname{Sym}^a(\operatorname{Sym}^bV)$ ; its surjectivity yields such an embedding by complete reducibility. Its image is the degree- $b$ part of the coordinate ring of the Chow variety of decomposable $a$ -forms, so surjectivity for large $b$ is a statement about that variety's normalization. The question is from which degree $b$ on the map is surjective, uniformly in $\dim V$ .

Timeline

1950 — Foulkes formulates the plethysm comparison (Foulkes, J. London Math. Soc. 1950).
1993 — Brion proves eventual surjectivity of the canonical map for fixed $a$ and $V$ (Brion, Manuscripta Math. 1993); in 1997 he gives an effective bound depending on both $a$ and $\dim V$ (Séminaires et Congrès 2, SMF, 1997, Theorem 3.3).
2008 — McKay proves a propagation theorem for Foulkes-type injectivity (J. Algebra 2008); Ikenmeyer gives a weight-shift proof (arXiv:1509.04957, 2015).
2015 — Landsberg's introduction to geometric complexity theory asks for a polynomial stabilization bound (Problem 7.19) (Ann. Univ. Ferrara 2015).
2017 — Cheung, Ikenmeyer and Mkrtchyan show that the canonical map has nonzero kernel at $(a,b)=(5,5)$ and $(6,6)$ in suitable dimensions (J. Symbolic Comput. 2017).
2022 — Raicu, Sam and Weyman bound the regularity of the Segre ring and modules of covariants on the Chow variety (Vietnam J. Math. 2022), without computing the top degree controlling stabilization.
2026 — An OpenAI preprint, Quadratic stabilization of the canonical Foulkes–Howe map (OpenAI Math Release, September 25, 2026), claims surjectivity for all $a\ge2$ , $b\ge a(a-1)$ and every finite-dimensional $V$ . The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Let $V$ be a finite-dimensional complex vector space and $\operatorname{Sym}V$ its symmetric algebra. $\operatorname{Sym}^nV\subseteq\operatorname{Sym}V$ is the span of products $v_1\cdots v_n$ of $n$ vectors. For $v_{j,i}\in V$ ( $1\le j\le b$ , $1\le i\le a$ ), the canonical Foulkes–Howe map is the linear map determined by

\mu_{a,b,V}\Bigl(\prod_{j=1}^{b}\bigl(v_{j,1}\cdots v_{j,a}\bigr)\Bigr) =\frac{1}{(a!)^{b}}\sum_{\sigma_1,\dots,\sigma_b\in S_a}\ \prod_{i=1}^{a}\Bigl(\prod_{j=1}^{b}v_{j,\sigma_j(i)}\Bigr),

where the outer products on the left and right are taken in $\operatorname{Sym}(\operatorname{Sym}^aV)$ and $\operatorname{Sym}(\operatorname{Sym}^bV)$ respectively. Equivalently: identify $\operatorname{Sym}^aW$ with symmetric tensors via averaging, multiply $b$ such tensors in $(\operatorname{Sym}V)^{\otimes a}$ , and project back. That this formula is well defined on $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is part of the content.

Formalization targets

Goal: quadratic stabilization (Theorem 1)

For every finite-dimensional complex $V$ and integers $a\ge2$ , $b\ge a(a-1)$ , there is a unique linear map

\mu:\operatorname{Sym}^b(\operatorname{Sym}^aV)\longrightarrow\operatorname{Sym}^a(\operatorname{Sym}^bV)

satisfying the displayed formula on monomials, and $\mu$ is surjective.

The bound $a(a-1)$ is not claimed to be sharp; the content is a stabilization degree polynomial in $a$ and independent of $\dim V$ . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Surjectivity gives, by complete reducibility, a $\mathrm{GL}(V)$ -equivariant embedding $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$ for $b\ge a(a-1)$ (Corollary 4 of the source), e.g. the sixth-power comparison for $b\ge30$ . It answers positively the request for a polynomial bound in Landsberg's Problem 7.19, and it says that the coordinate ring of the Chow variety of decomposable $a$ -forms agrees with its normalization in every degree $b\ge a(a-1)$ . Since the canonical map is known to fail to be injective at $(5,5)$ and $(6,6)$ , an explicit range of surjectivity is the right kind of statement for this specific map.

Formalizing it. The statement is purely algebraic and uniform in $V$ , $a$ , $b$ . A formal proof would need multilinear algebra over symmetric algebras (symmetric powers of symmetric powers), which is reusable for plethysm and invariant-theory projects.

Difficulty

Surjectivity is equivalent to the vanishing of every symmetric $a$ -linear form on $\operatorname{Sym}^bV$ whose diagonal vanishes on products of $b$ vectors. The naive induction on $a$ fails because the factors in different slots share a common product and cannot be varied independently; the dimension of $V$ also grows the space of such forms without bound, so arguments using a fixed basis or dimension count do not give a uniform bound. Brion's effective bound depends on $\dim V$ , and regularity bounds for the normalization do not locate the top degree of the quotient that controls stabilization.

Formalization scope

$\operatorname{Sym}^nV$ is represented as the submodule SymPow n V of Mathlib's SymmetricAlgebra ℂ V spanned by products of $n$ vectors, and $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is SymPow b (SymPow a V).
IsFoulkesMap a b V μ states the monomial formula above, with the normalizing factor $(a!)^{-b}$ and the sum over $b$ -tuples of permutations of Fin a.
The goal asserts existence, surjectivity and uniqueness of a linear map with this formula; uniqueness rules out choosing an arbitrary surjection, so the theorem is about the canonical map and not merely about dimensions.
$V$ ranges over all finite-dimensional complex vector spaces in an arbitrary universe; $a\ge2$ and $b\ge a(a-1)$ are natural numbers.
Needed infrastructure: symmetric powers inside the symmetric algebra, polarization/annihilator criteria, and directional-derivative operators on polynomial functions.

Selected references

H. O. Foulkes, Concomitants of the quintic and sextic up to degree four in the coefficients of the ground form, J. London Math. Soc. 25 (1950), 205–209. https://doi.org/10.1112/jlms/s1-25.3.205
M. Brion, Stable properties of plethysm: on two conjectures of Foulkes, Manuscripta Math. 80 (1993), 347–371. https://doi.org/10.1007/BF03026558
M. Brion, Sur certains modules gradués associés aux produits symétriques, Séminaires et Congrès 2, SMF, 1997, 157–183. https://smf.emath.fr/publications/sur-certains-modules-gradues-associes-aux-produits-symetriques
T. McKay, On plethysm conjectures of Stanley and Foulkes, J. Algebra 319 (2008), 2050–2071. https://doi.org/10.1016/j.jalgebra.2007.12.003
C. Ikenmeyer, On McKay's propagation theorem for the Foulkes conjecture, arXiv:1509.04957, 2015. https://arxiv.org/abs/1509.04957v1
J. M. Landsberg, Geometric complexity theory: an introduction for geometers, Ann. Univ. Ferrara 61 (2015), 65–117. https://doi.org/10.1007/s11565-014-0202-7
M.-W. Cheung, C. Ikenmeyer and S. Mkrtchyan, Symmetrizing tableaux and the 5th case of the Foulkes conjecture, J. Symbolic Comput. 80 (2017), 833–843. https://doi.org/10.1016/j.jsc.2016.09.002
C. Raicu, S. V. Sam and J. Weyman, On some modules supported in the Chow variety, Vietnam J. Math. 50 (2022), 501–521. https://doi.org/10.1007/s10013-021-00527-2
OpenAI, Quadratic stabilization of the canonical Foulkes–Howe map, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf

43 thms2 active usersReviewed

Completed

Algebraic Topology Group Theory·Captain: wurtle

A Torsion-Free Group Algebra with Zero DivisorsResearch Paper

Motivation: Kaplansky's zero-divisor conjecture

For a field $K$ and a group $G$ , the group algebra $K[G]$ consists of finite formal sums $\sum_g a_g g$ with $a_g\in K$ , multiplied by extending the group law bilinearly. If $g\in G$ has finite order $m>1$ , then $(1-g)(1+g+\dots+g^{m-1})=0$ , so $K[G]$ has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if $G$ is torsion-free, $K[G]$ has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).

Timeline

1940 — Higman's thesis raises the question and proves the domain property for groups in which every nontrivial subgroup maps onto $\mathbb Z$ (Higman, Proc. LMS 1940); the thesis formulation is reproduced by Sandling (1981).
1956/1957 — Kaplansky poses the problem (Problem 6 in Problems in the theory of rings, National Research Council, 1957).
1987 — Rips and Segev construct torsion-free groups without the unique-product property, removing the standard route to the conjecture (J. Algebra 1987); Steenbock gives a graphical small-cancellation treatment (J. Algebra 2015).
1988 — Kropholler, Linnell and Moody prove the conjecture for torsion-free elementary amenable groups (Proc. AMS 1988).
2021 — Gardam disproves the related unit conjecture over $\mathbb F_2$ (Ann. of Math. 2021), and later over $\mathbb C$ (arXiv:2312.05240, 2024). A nontrivial unit is not a zero divisor, so the zero-divisor conjecture remained open.
2026 — Fisher and Sánchez-Peralta prove the domain conclusion for torsion-free 3-manifold groups and division-ring embeddings for virtually compact special groups (J. Comb. Algebra 2026).
2026 — An OpenAI preprint, A Torsion-Free Group Algebra with Zero Divisors (OpenAI Math Release, September 23, 2026), claims a finitely presented torsion-free group $G$ with a finite 2-dimensional classifying space such that $\mathbb F_2[G]$ has nonzero zero divisors. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A group $G$ is torsion-free if $g^n=1$ with $n\ge1$ implies $g=1$ . It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or $K(G,1)$ ) for $G$ is a path-connected space $X$ with $\pi_1(X)\cong G$ whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions $\le 2$ . A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.

The coefficient field is $\mathbb F_2=\mathbb Z/2$ , and $\mathbb F_2[G]$ is Mathlib's MonoidAlgebra (ZMod 2) G.

Formalization targets

Goal: a counterexample to the zero-divisor conjecture (Theorem 1.1)

There exist a group $G$ and $\alpha,\beta\in\mathbb F_2[G]$ such that

G\ \text{finitely presented},\quad G\ \text{torsion-free},\quad G\ \text{has a finite 2-dimensional } K(G,1),\quad \alpha\neq0,\ \beta\neq0,\ \alpha\beta=0.

This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over $\mathbb F_2$ , a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force $K[G]$ to be a domain. It implies that $G$ fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.

Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional $K(G,1)$ ) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's $\widetilde A_2$ lattice (Mian–Siddique 2026).

Difficulty

Writing down $\alpha,\beta$ whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.

Formalization scope

TorsionFree G is the plain group-theoretic notion ( $g^n=1$ , $n>0$ implies $g=1$ ); finite presentability is Group.IsFinitelyPresented.
HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space $X$ with a finite CW structure on all of $X$ , no cells above dimension $2$ , at least one $2$ -cell, a group isomorphism $G\simeq\pi_1(X,x)$ , and a surjective covering map from a contractible space onto $X$ (so $X$ is aspherical). Requiring a $2$ -cell excludes only the case of free groups, whose group algebras are domains.
The witnessing group lives in Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.
A trivializing reading is excluded because all three group properties and both nonvanishing conditions are required simultaneously.
Infrastructure needed: CW complexes and covering spaces (partially in Mathlib), the fundamental group of a 2-complex built by attaching cones, Hurewicz/Whitehead-type asphericity arguments, and random graph constructions.

Selected references

G. Higman, The units of group-rings, Proc. London Math. Soc. (2) 46 (1940). https://doi.org/10.1112/plms/s2-46.1.231
I. Kaplansky, Problems in the theory of rings, Report of a Conference on Linear Algebras (1956), National Research Council, 1957.
E. Rips and Y. Segev, Torsion-free group without unique product property, J. Algebra (1987). https://doi.org/10.1016/0021-8693(87)90125-6
P. H. Kropholler, P. A. Linnell and J. A. Moody, Applications of a new K-theoretic theorem to soluble group rings, Proc. Amer. Math. Soc. (1988). https://doi.org/10.2307/2046771
M. Steenbock, Rips–Segev torsion-free groups without the unique product property, J. Algebra (2015). https://doi.org/10.1016/j.jalgebra.2015.05.004
G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021). https://doi.org/10.4007/annals.2021.194.3.9
G. Gardam, Non-trivial units of complex group rings, preprint, 2024. https://arxiv.org/abs/2312.05240v2
S. P. Fisher and P. Sánchez-Peralta, Division rings for group algebras of virtually compact special groups and 3-manifold groups, J. Comb. Algebra (2026). https://doi.org/10.4171/JCA/89
I. Mian and S. Siddique, A machine-checked proof that Gardam's $\widetilde A_2$ lattice does not have unique products, preprint, 2026. https://arxiv.org/abs/2609.22380v1
OpenAI, A Torsion-Free Group Algebra with Zero Divisors, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026/paper.pdf

11 thms2 active usersReviewed

Completed

Algebraic Geometry·Captain: wurtle

An explicit failure of complex affine-space cancellationResearch Paper

Motivation

Zariski's cancellation problem asks whether affine space can be recognized from its cylinder: if a variety $X$ satisfies $X\times\mathbb A^1\cong\mathbb A^{n+1}$ , must $X\cong\mathbb A^n$ ? Algebraically, for a finitely generated commutative $\mathbb C$ -algebra $A$ and an independent variable $w$ ,

A[w]\cong\mathbb C^{[n+1]}\ \overset{?}{\Longrightarrow}\ A\cong\mathbb C^{[n]},

where $\mathbb C^{[r]}$ is a polynomial ring in $r$ variables and all isomorphisms are $\mathbb C$ -algebra isomorphisms. The problem is one of the central questions of affine algebraic geometry, closely tied to the recognition of affine space, coordinates of polynomial rings, and polynomial fibrations.

Background

1972. Abhyankar, Heinzer and Eakin prove cancellation for the affine line (doi:10.1016/0021-8693(72)90134-2).
1974. Dolgachev and Weisfeiler formulate the affine-fibration conjecture (doi:10.1070/IM1974v008n04ABEH002127).
1979–1980. Fujita, and Miyanishi and Sugie, prove cancellation for the complex affine plane (doi:10.3792/pjaa.55.106, doi:10.1215/kjm/1250522319).
1987. Asanuma constructs, in positive characteristic, threefolds whose cylinders are affine four-space (doi:10.1007/BF01389155).
1996. Makar-Limanov uses additive group actions to show that the Russell cubic is not $\mathbb C^3$ (doi:10.1007/BF02937314).
2014. Gupta proves failure of cancellation in every dimension $\ge3$ over every field of positive characteristic (doi:10.1007/s00222-013-0455-2, doi:10.1016/j.aim.2014.07.012).
2018–2021. El Kahoui–Ouali and Dutta–Lahiri prove that residual coordinates are one-stably coordinates (doi:10.1216/JCA-2018-10-3-317, doi:10.1016/j.jpaa.2021.106707).
2026. Gaifullin and Petrov still list the characteristic-zero problem in dimension $\ge3$ as unresolved (arXiv:2607.13593).

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

Setting

Let $p,s,u,F,J$ be independent variables over $\mathbb C$ and $P=\mathbb C[p,s,u,F,J]$ . Put

x=s^2+u^3+p^2F,\qquad H=x^2F-(1+2sx)J-p^2J^2-pu,\qquad A=P/(H).

So $A$ is the coordinate ring of the hypersurface $\{H=0\}\subset\mathbb A^5$ . For a $\mathbb C$ -algebra $A$ , $A[w]$ denotes the polynomial ring in one further variable, and $\mathbb C^{[r]}$ the polynomial ring in $r$ variables.

Formalization targets

Goal: Theorem 1.1

A\ \text{is a finitely generated integral domain of Krull dimension }4,\qquad A[w]\cong_{\mathbb C}\mathbb C^{[5]},\qquad A\not\cong_{\mathbb C}\mathbb C^{[4]}.

The Lean statement OAI.ComplexCancellation.main is open on the platform.

Significance

Theorem 1.1 gives a negative answer to Zariski's cancellation problem over $\mathbb C$ in dimension four, with an explicit counterexample of degree small enough to write in one line. The same polynomial yields two further consequences proved in the paper: $H$ is a coordinate of $P[w]$ but not of $P$ , so the Stable Coordinate Conjecture fails in ambient dimension five (Corollary 1.2); and the maps $p:\operatorname{Spec}A\to\mathbb A^1$ and $(p,H):\mathbb A^5\to\mathbb A^2$ are smooth $\mathbb A^3$ -fibrations that are not Zariski-locally trivial, disproving the Dolgachev–Weisfeiler conjecture over these bases (Corollary 7.1). Cancellation in dimension three over $\mathbb C$ is not addressed.

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

Difficulty

The cylinder isomorphism $A[w]\cong\mathbb C^{[5]}$ is comparatively explicit: a locally nilpotent derivation sends $H$ to $p^3$ , and exponentiating converts $H$ into $H+p^3w$ . The hard part is proving $A\not\cong\mathbb C^{[4]}$ . Standard invariants do not help: $A$ is smooth, factorial-type obstructions vanish, and topologically $\operatorname{Spec}A$ is contractible like $\mathbb C^4$ since its cylinder is $\mathbb C^5$ . The paper uses additive group actions (locally nilpotent derivations), passing to an associated graded algebra along $p=0$ , lifting actions through a line bundle over a smooth affine quadric, and a rigidity argument based on the Mason–Stothers polynomial abc inequality.

Formalization scope

P := MvPolynomial (Fin 5) ℂ with p, s, u, F, J := X 0, …, X 4; x and H are transcribed literally; A := P ⧸ Ideal.span {H}.
Dimension is ringKrullDim A = 4; integrality is IsDomain A; finite generation is Algebra.FiniteType ℂ A.
The cylinder statement is Nonempty (Polynomial A ≃ₐ[ℂ] MvPolynomial (Fin 5) ℂ); the non-polynomiality is ¬ Nonempty (A ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ). All isomorphisms are $\mathbb C$ -algebra isomorphisms.

A complete development needs: explicit polynomial automorphisms (for the cylinder), Krull dimension of hypersurface quotients, locally nilpotent derivations and their kernels, filtrations and associated graded rings, and the Mason–Stothers theorem for polynomials. Contributions formalizing Proposition 2.2, Proposition 3.4 (the graded identification), Propositions 4.1–4.3, Lemma 5.1 (order of a locally nilpotent derivation), Lemma 6.1 (Mason–Stothers) and Proposition 6.3 are welcome.

Selected references

OpenAI, An explicit failure of complex affine-space cancellation, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf
N. Gupta, On Zariski's cancellation problem in positive characteristic, Adv. Math., 2014. https://doi.org/10.1016/j.aim.2014.07.012
N. Gupta, On the cancellation problem for the affine space $\mathbb A^3$ in characteristic $p$ , Invent. Math., 2014. https://doi.org/10.1007/s00222-013-0455-2
S. S. Abhyankar, W. Heinzer, P. Eakin, On the uniqueness of the coefficient ring in a polynomial ring, J. Algebra, 1972. https://doi.org/10.1016/0021-8693(72)90134-2
T. Fujita, On Zariski problem, Proc. Japan Acad. Ser. A, 1979. https://doi.org/10.3792/pjaa.55.106
L. Makar-Limanov, On the hypersurface $x+x^2y+z^2+t^3=0$ in $\mathbb C^4$ or a $\mathbb C^3$ -like threefold which is not $\mathbb C^3$ , Israel J. Math., 1996. https://doi.org/10.1007/BF02937314
A. K. Dutta, A. Lahiri, On residual and stable coordinates, J. Pure Appl. Algebra, 2021. https://doi.org/10.1016/j.jpaa.2021.106707
M. El Kahoui, M. Ouali, A note on residual coordinates of polynomial rings, J. Commut. Algebra, 2018. https://doi.org/10.1216/JCA-2018-10-3-317
B. Yu. Weisfeiler, I. V. Dolgachev, Unipotent group schemes over integral rings, Math. USSR-Izv., 1974. https://doi.org/10.1070/IM1974v008n04ABEH002127
S. Gaifullin, M. Petrov, Non-cancellative varieties, maximal tori, and the Makar-Limanov invariant, preprint, 2026. https://arxiv.org/abs/2607.13593

41 thms2 active usersReviewed

Algebraic Geometry Convex Optimization Optimization·Captain: mikedeng1

Semidefinite Programming Relaxations for Semialgebraic Problems 1: A Polynomial System Has No Real Solution if and only if Its Degree-d Positivstellensatz SDP Is Feasible for All Large dResearch Paper

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

13 thms2 active usersReviewed

Information Theory Theoretical Computer Science·Captain: mikedeng1

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 3: Shingling plus PinSketch Gives an Average-Case Secure Sketch for Edit DistanceResearch Paper

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.

$\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.
$\mathrm{SDif}(\mathcal U)$ : all subsets of a finite universe $\mathcal U$ , with distance $|w \triangle w'|$ .
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

Set difference. Theorem 6.3: PinSketch is an average-case $(\mathrm{SDif}(\mathcal U), m, m - t\log(n+1), t)$ $(SDif (U), m, m - t lo g (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'$ .
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)$ .
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

13 thms2 active usersReviewed

Completed

Combinatorics Information Theory Theoretical Computer Science·Captain: mikedeng1

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 2: The Improved Juels–Sudan Sketch Is an Average-Case Secure Sketch for s-Element Sets with Entropy Loss t log nResearch Paper

Motivation

Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.

When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both $t\log n$ for $s$ -element subsets of an $n$ -element universe, independent of $s$ . The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.

Setting

Laws and average min-entropy. A random variable is identified with its law. For a pair $(A,B)$ ,

\tilde H_\infty(A\mid B) = -\log_2 \sum_b \max_a \Pr[A=a \wedge B=b],

which equals $-\log_2 \mathbb E_{b\leftarrow B}\big[\max_a\Pr[A=a\mid B=b]\big]$ , the average min-entropy of §2.4: the negative logarithm of the best probability of guessing $A$ after seeing $B$ .

Secure sketches. Let $\mathcal M$ be a set with an integer-valued distance $\mathrm{dis}$ . A pair of procedures $(\mathsf{SS},\mathsf{Rec})$ is an average-case $(\mathcal M,m,\tilde m,t)$ -secure sketch (Definitions 3 and 4) if

(correctness) $\mathrm{dis}(w,w')\le t$ implies $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ ;
(security) for all random variables $W$ over $\mathcal M$ and $I$ with $\tilde H_\infty(W\mid I)\ge m$ , one has $\tilde H_\infty(W\mid (\mathsf{SS}(W),I))\ge\tilde m$ .

The difference $m-\tilde m$ is the entropy loss.

The metric. For a finite universe $\mathcal U$ with $n=|\mathcal U|$ , $\mathrm{SDif}_s(\mathcal U)$ is the set of $s$ -element subsets of $\mathcal U$ with $\mathrm{dis}(w,w')=|w\triangle w'|$ .

Construction 5. Identify $\mathcal U$ with a finite field $\mathcal F$ of $n$ elements and let $t\le s$ .

$\mathsf{SS}(w)$ : form $p'(z)=\prod_{x\in w}(z-x)$ , monic of degree $s$ , and output its coefficients $a_{s-1},\dots,a_{s-t}$ of degree $s-1$ down to $s-t$ .
$\mathsf{Rec}(w',(a_{s-1},\dots,a_{s-t}))$ : form $p_{\mathrm{high}}(z)=z^s+\sum_{i=s-t}^{s-1}a_iz^i$ ; find a polynomial $p_{\mathrm{low}}$ of degree at most $s-t-1$ that agrees with $p_{\mathrm{high}}$ on at least $s-t/2$ points of $w'$ (Reed–Solomon decoding); output the roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$ .

The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.

Formalization targets

Goal: Theorem 6.1

For every finite field $\mathcal F$ with $n$ elements, all $t\le s$ and every real $m$ ,

(\mathsf{SS},\mathsf{Rec})\ \text{is an average-case}\ \big(\mathrm{SDif}_s(\mathcal F),\,m,\,m-t\log_2 n,\,t\big)\text{-secure sketch}.

The goal is uniform in $m$ : the entropy loss $t\log n$ does not depend on the input distribution.

Milestones (the correctness half)

The paper's argument on p. 21 splits into four steps, each a milestone:

$p'=p_{\mathrm{high}}+q$ with $\deg q\le s-t-1$ , and $p_{\mathrm{high}}=-q$ on $w$ ;
$|w\triangle w'|\le t$ implies $|w\cap w'|\ge s-t/2$ , so $-q$ is a valid $p_{\mathrm{low}}$ ;
any two valid $p_{\mathrm{low}}$ coincide;
$\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $|w\triangle w'|\le t$ .

A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first $t$ elementary symmetric polynomials of $w$ , up to sign.

The security half is the entropy bound: since $\mathsf{SS}$ takes at most $n^t$ values, $\tilde H_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde H_\infty(W\mid I)-t\log n$ (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).

Significance

The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are $t\log n$ , which the paper shows is essentially optimal when $n\gg s$ (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.

Difficulty

No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: $p_{\mathrm{high}}$ must agree with $p'$ in every coefficient of degree at least $s-t$ , so that the remainder has degree at most $s-t-1$ , and the uniqueness count ("two candidates agree on at least $s-t$ points") requires the threshold to be at least $s-t/2$ ; the paper's sentence says "more than", which does not support the argument as written. The roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$ must be shown to form exactly the set $w$ , with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, $n^t$ -valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.

Formalization scope

Conventions committed to in Lean:

Laws are PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary $I$ ranges over an arbitrary ι : Type (a superset of the paper's $\{0,1\}^*$ ), never restricted to finite types.
The universe is the field $\mathcal F$ itself, [Field 𝔽] [Fintype 𝔽], with $n$ = Fintype.card 𝔽; the paper's " $n$ is a prime power" is then automatic.
The paper leaves $t\le s$ implicit; every statement assumes it. No parity condition on $t$ is imposed: "at least $s-t/2$ " is written $2\cdot\#\ge 2s-t$ in $\mathbb N$ , which covers odd $t$ .
"Degree at most $s-t-1$ " is degree < s - t, so $p_{\mathrm{low}}=0$ when $t=s$ .
The sketch is a vector in $\mathcal F^t$ indexed from $0$ : entry $i$ is the coefficient of degree $s-1-i$ . The storage bound $t\log n$ holds by this type and is not restated.
$\mathsf{Rec}$ takes an arbitrary valid $p_{\mathrm{low}}$ (by choice) instead of running a decoding algorithm. The paper's "fail" output is encoded as returning $w'$ , which only occurs when correctness makes no claim.
Running time is out of scope. Theorem 6.1's clause that $\mathsf{SS}$ and $\mathsf{Rec}$ run in time polynomial in $s$ , $t$ and $\log n$ is dropped, and no surrogate predicate replaces it.

A formalization that checks only correctness, drops or trivializes the entropy clause, or lets $\mathsf{Rec}$ see $w$ itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with $\mathsf{Rec}$ given only $w'$ and the sketch.

Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.

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
A. Juels, M. Sudan, A Fuzzy Vault Scheme, Designs, Codes and Cryptography 38(2):237–257, 2006. https://doi.org/10.1007/s10623-005-6343-z
E. Agrell, A. Vardy, K. Zeger, Upper Bounds for Constant-Weight Codes, IEEE Trans. Inform. Theory 46(7):2373–2395, 2000. https://doi.org/10.1109/18.887851

8 thms2 active usersReviewed

Analysis·Captain: Lucas

Smale's Mean Value ConjectureOpen Problem

Motivation

The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.

Timeline

1981 — Smale poses the problem and proves the inequality below with constant $K = 4$ (Smale 1981). The example $P(z) = z^d - dz$ shows that the constant cannot be smaller than $\frac{d-1}{d}$ in degree $d$ , so no constant below $1$ works in all degrees.
1989 — Tischler proves the inequality with the optimal constant $K = \frac{d-1}{d}$ when all roots of $P$ are real, and when all roots of $P$ have the same absolute value (Tischler 1989).
2007 — Conte, Fujikawa and Lakic prove $K \le 4\frac{d-1}{d+1}$ (Conte–Fujikawa–Lakic 2007). Crane proves $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ (Crane 2007).
2009 — Dubinin and Sugawa prove the reverse (dual) inequality with constant $\frac{1}{d\,4^d}$ (Dubinin–Sugawa 2009); optimizing this lower bound is the dual mean value problem (Ng–Zhang 2016).

No absolute constant $K < 4$ is known that works in every degree.

Setting

Let $P$ be a polynomial with complex coefficients of degree $d \ge 2$ , and write $P'$ for its derivative. A critical point of $P$ is a complex number $c$ with $P'(c) = 0$ ; since $d \ge 2$ , $P'$ is a nonconstant polynomial of degree $d-1$ , so $P$ has at least one and at most $d-1$ distinct critical points. Fix a complex number $z$ that is not a critical point, $P'(z) \ne 0$ . For every critical point $c$ we then have $c \ne z$ , and the difference quotient

\frac{P(z) - P(c)}{z - c}

is well defined. The question is how small this quotient can be made, relative to $|P'(z)|$ , by choosing the critical point $c$ well.

Formalization targets

Goal: Smale's mean value conjecture ( $K = 1$ )

For every complex polynomial $P$ of degree $d \ge 2$ and every $z \in \mathbb C$ with $P'(z) \ne 0$ there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le |P'(z)|.

Stronger: the optimal constant

The same with $|P'(z)|$ replaced by $\frac{d-1}{d}\,|P'(z)|$ ; the example $z^d - dz$ shows this constant cannot be lowered.

Known results (milestones)

Smale's inequality with $K = 4$ .
The extremal example $P(z) = z^d - dz$ at $z = 0$ , where every critical point gives exactly $\frac{d-1}{d}|P'(0)|$ , and its consequence that no constant $K < 1$ works in all degrees.
Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$ .
Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ .
The Dubinin–Sugawa dual inequality $\left|\frac{P(z)-P(c)}{z-c}\right| \ge \frac{|P'(z)|}{d\,4^d}$ for some critical point $c$ .

Significance

The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.

Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's $K = 4$ bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.

Difficulty

The obvious strategies control the quotient through one critical point at a time: for instance, bounding $|P(z) - P(c)|$ by integrating $P'$ along the segment from $c$ to $z$ . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to $K$ close to $4$ . Reaching $K = 1$ requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case $z^d - dz$ , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.

Formalization scope

Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of $P$ are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants $\frac{d-1}{d}$ and $4\frac{d-1}{d+1}$ are computed in ℝ from the cast of natDegree.

Every statement assumes $P'(z) \ne 0$ . This is the standard normalization and is essential in Lean: division by zero returns $0$ , so without it the choice $c = z$ would make the inequality trivially true whenever $z$ is itself a critical point. With the hypothesis, every critical point $c$ differs from $z$ and the quotient is a genuine difference quotient.

Crane's bound is stated as the existence, for each degree $d \ge 8$ , of a constant strictly below $4 - \frac{2.263}{\sqrt d}$ that works for all polynomials of degree exactly $d$ ; this is equivalent to the best constant in degree $d$ being strictly below that value.

A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.

Selected references

S. Smale, The fundamental theorem of algebra and complexity theory, Bull. Amer. Math. Soc. (N.S.) 4 (1981), 1–36. https://doi.org/10.1090/S0273-0979-1981-14858-8
D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), 438–456. https://doi.org/10.1016/0885-064X(89)90019-8
A. Conte, E. Fujikawa, N. Lakic, Smale's mean value conjecture and the coefficients of univalent functions, Proc. Amer. Math. Soc. 135 (2007), 3295–3300. https://doi.org/10.1090/S0002-9939-07-08861-2
E. Crane, A bound for Smale's mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), 781–791. https://doi.org/10.1112/blms/bdm063
V. Dubinin, T. Sugawa, Dual mean value problem for complex polynomials, Proc. Japan Acad. Ser. A 85 (2009), 135–137. https://arxiv.org/abs/0906.4605
T.-W. Ng, Y. Zhang, Smale's mean value conjecture for finite Blaschke products, J. Anal. 24 (2016), 331–345. https://arxiv.org/abs/1609.00170
Wikipedia, Mean value problem. https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764

10 thms2 active usersReviewed

Algebraic Geometry Number Theory·Captain: vatsj

Milnor conjecture (Voevodsky 2003), formalizedResearch Paper

Motivation

For a field $F$ , two invariants built from very different data turn out to carry the same mod-2 information. One is Milnor K-theory $K^M_n(F)$ , defined by generators and relations from the multiplicative group $F^\times$ alone. The other is Galois cohomology $H^n(F,\mathbb{Z}/2)$ , the continuous cohomology of the absolute Galois group of $F$ . In 1970 Milnor considered a natural map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees, verified that it is an isomorphism for several classes of fields, and remarked that he knew of no field where it fails (Milnor 1970). The statement that it is always an isomorphism when $\operatorname{char} F \neq 2$ became known as the Milnor conjecture. Its companion conjecture on quadratic forms was later deduced from it (Orlov–Vishik–Voevodsky 2007). Together they identify the graded Witt ring of quadratic forms, Galois cohomology mod 2, and $K^M_*(F)/2$ .

Timeline. The attributions below follow the introduction of Voevodsky 2003.

1970: Milnor considers the map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees and gives classes of fields where it is an isomorphism (Milnor 1970).
Bass–Tate (published 1973): the Kummer classes satisfy the Steinberg relation, so the Kummer map extends to a ring homomorphism on $K^M_*(F)$ (Bass–Tate 1973).
Degrees 0 and 1: the map is an isomorphism, by Kummer theory and Hilbert's Theorem 90.
1981: Merkurjev proves degree 2 with $2$ as the coefficient prime.
1982: Merkurjev and Suslin extend degree 2 to every prime $\ell$ (Merkurjev–Suslin 1982).
Degree 3, $\ell = 2$ : proved by Merkurjev–Suslin and, independently, by Rost.
2003: Voevodsky proves all degrees, in every characteristic $\neq 2$ (Voevodsky 2003, Cor. 7.5), using the motivic Steenrod operations constructed in Voevodsky 2003b. This work was cited for his 2002 Fields Medal.
2011: the analogue for odd primes, the Bloch–Kato conjecture, is proved (Voevodsky 2011); a book-length account is Haesemeyer–Weibel 2019.

Setting

Let $F$ be a field with $2 \neq 0$ in $F$ .

Milnor K-theory. For $n \ge 0$ , $K^M_n(F)$ is the quotient of the $n$ -fold tensor power $(F^\times)^{\otimes n}$ , taken over $\mathbb{Z}$ with $F^\times$ written additively, by the subgroup generated by the pure tensors $a_1\otimes\cdots\otimes a_n$ in which some adjacent pair satisfies $a_i + a_{i+1} = 1$ . This is the degree- $n$ part of $T(F^\times)/I$ , where $I$ is the two-sided ideal generated by $a\otimes(1-a)$ . The class of $a_1\otimes\cdots\otimes a_n$ is the symbol $\{a_1,\dots,a_n\}$ . In particular $K^M_0(F) = \mathbb{Z}$ and $K^M_1(F) = F^\times$ . In Lean these are MilnorK F n and symbol a for a : Fin n → Fˣ.

Galois cohomology. Let $F^{\mathrm{sep}}$ be a separable closure and $G_F = \operatorname{Gal}(F^{\mathrm{sep}}/F)$ the absolute Galois group, a profinite group under the Krull topology. $H^n(F,\mathbb{Z}/2)$ is the continuous cohomology $H^n_{\mathrm{cts}}(G_F,\mathbb{Z}/2)$ with trivial action, computed from $G_F$ -invariant continuous homogeneous cochains. In Lean this is H F n, Mathlib's continuousCohomology n of the trivial representation.

The Galois symbol. For $a \in F^\times$ fix $\sqrt a \in F^{\mathrm{sep}}$ . The Kummer character $\chi_a : G_F \to \mathbb{Z}/2$ is $\chi_a(\sigma) = 0$ if $\sigma(\sqrt a) = \sqrt a$ and $1$ otherwise. It is a continuous homomorphism representing the Kummer class $\delta a \in H^1$ . The Galois symbol of $(a_1,\dots,a_n)$ is the class of the homogeneous cocycle

(x_0,\dots,x_n)\ \longmapsto\ \prod_{j=1}^{n}\bigl(\chi_{a_j}(x_j)-\chi_{a_j}(x_{j-1})\bigr),

the homogeneous form of $(\sigma_1,\dots,\sigma_n) \mapsto \chi_{a_1}(\sigma_1)\cdots\chi_{a_n}(\sigma_n)$ , i.e. the cup product $\delta a_1\cup\cdots\cup\delta a_n$ . In Lean this is galoisSymbol a.

Formalization targets

Goal: the Milnor conjecture (Voevodsky 2003, Corollary 7.5)

For every field $F$ with $\operatorname{char} F \neq 2$ and every $n \ge 0$ there is a homomorphism

\varphi : K^M_n(F) \to H^n(F,\mathbb{Z}/2),\qquad \varphi\{a_1,\dots,a_n\} = \delta a_1\cup\cdots\cup\delta a_n,

which is surjective and whose kernel is exactly $2\,K^M_n(F)$ .

Since symbols generate $K^M_n(F)$ , such a $\varphi$ is unique; it is the norm residue homomorphism. The statement is therefore equivalent to $K^M_n(F)/2 \cong H^n(F,\mathbb{Z}/2)$ via the norm residue map. Its existence, i.e. the fact that the Steinberg relations map to zero, is part of the claim.

Significance

The result itself. The theorem gives a presentation of mod-2 Galois cohomology by generators and relations: every class is a sum of cup products of degree-one classes, and every relation among such products comes from Steinberg relations and multiples of 2. With Orlov–Vishik–Voevodsky 2007 it yields Milnor's conjecture on quadratic forms, which classifies quadratic forms up to Witt equivalence by their Galois-cohomological invariants.

Formalizing it. The theorem is proved but not formalized. At the time of writing, Mathlib has neither Milnor K-theory nor cup products in group or continuous cohomology, and has Hilbert 90 only for finite Galois extensions. This mission's definitions provide a sorry-free Galois symbol in Mathlib's continuous cohomology, which already makes the degree 0 and degree 1 cases (Kummer theory) meaningful targets. A complete development would formalize the IHES proof, including motivic cohomology with $\mathbb{Z}/2$ coefficients and the motivic Steenrod algebra. No part of that is currently available in Lean. Related existing work: on this platform, a graded cup product (groupCohomology.exists_isGradedCupProduct) and a Kummer theory and Hilbert 90 for level-constant cocycles have been formalized on top of Mathlib's discrete groupCohomology. The cup product is for discrete groups, and the Kummer and Hilbert 90 results use finite-level hypotheses in place of continuity, so none of them transfers directly to continuousCohomology.

Difficulty

Degrees 0 and 1 follow from Kummer theory and Hilbert 90. Degree 2 is Merkurjev's theorem, whose proof goes through the K-theory of Severi–Brauer varieties. No argument internal to Galois cohomology or K-theory of fields is known in higher degrees. The known proof reformulates the statement as a vanishing theorem for motivic cohomology of fields, the "Hilbert 90" property for weight $n$ . It then argues by induction on $n$ through geometry over $F$ : splitting varieties of symbols (Pfister quadrics), their motives, and cohomology operations on motivic cohomology. Each of these is a substantial theory, none of it exists in Mathlib, and the induction passes through statements about arbitrary smooth varieties, not only fields.

Formalization scope

Scope. The target is the Milnor conjecture, i.e. the prime $2$ with coefficients $\mathbb{Z}/2 \cong \mu_2$ . The Bloch–Kato conjecture for odd primes is out of scope.

Conventions.

The field is F : Type, universe 0. Mathlib's continuousCohomology requires the coefficient module to live in the universe of the group. For $F$ in a higher universe this forces ULift (ZMod 2), for which the needed Module and ContinuousSMul instances are not available as global instances. Universe polymorphism is not part of this mission. It does not follow by plain transport, since a field in a higher universe need not be isomorphic to any field in Type; one route is a limit argument, using that both sides commute with directed unions of fields and that every field is the directed union of its countable subfields, each isomorphic to a field in Type.
The hypothesis $\operatorname{char} F \neq 2$ is [NeZero (2 : F)].
$H^n$ is Mathlib's continuousCohomology, built from homogeneous cochains, with $\mathbb{Z}/2$ as a trivial representation of $G_F$ with the Krull topology.
$K^M_n(F)$ is defined one degree at a time, not as a graded ring.
"Kernel $= 2K^M_n$ " means $\varphi(x)=0 \iff \exists y,\ x = 2y$ .

Ruling out trivializations. The Galois symbol is not a free parameter. It is a fixed, sorry-free definition, and the existence of $\varphi$ with the prescribed values on symbols is part of the goal. Neither can be chosen to make the statement vacuous.

Route. Reductions should follow Voevodsky 2003 together with Voevodsky 2003b. That route avoids resolution of singularities and works in every characteristic $\neq 2$ . The following rely on resolution of singularities (or on characteristic-0 reductions) and should not be used as inputs:

Mazza–Voevodsky–Weibel (MVW 2006), results 16.24, 16.25 and 20.1, and the cdh-topology and compactly-supported-motive material;
the original Suslin–Voevodsky paper relating Bloch–Kato to Beilinson–Lichtenbaum (Suslin–Voevodsky 2000); use Haesemeyer–Weibel 2019, Chapter 2, instead;
Haesemeyer–Weibel Part II, and their reduction to characteristic 0 (Lemma 1.3);
Voevodsky's 1995–96 preprints on the Milnor conjecture.

Infrastructure needed and reusable. A complete development needs:

the ring structure on $K^M_*(F)$ (cf. Carlier's KMilnorWitt for Milnor–Witt K-theory);
cup products in continuous cohomology;
Hilbert 90 for profinite Galois groups;
Galois cohomology as étale cohomology of $\operatorname{Spec} F$ ;
the Nisnevich topology;
presheaves with transfers, motivic complexes and motivic cohomology;
motivic Steenrod operations;
motives of Pfister quadrics.

Most of this is reusable well beyond the mission. The homogeneous-cochain construction in the definition files, which turns an invariant continuous cocycle $G^{n+1}\to M$ into a class in Mathlib's continuousCohomology, applies to any locally compact group with trivial coefficients. Contributions of any of these components, and of the degree 0 and 1 cases, are welcome.

Selected references

V. Voevodsky, Motivic cohomology with $\mathbb{Z}/2$ -coefficients, Publ. Math. IHÉS 98 (2003), 59–104. https://doi.org/10.1007/s10240-003-0010-6
V. Voevodsky, Reduced power operations in motivic cohomology, Publ. Math. IHÉS 98 (2003), 1–57. https://doi.org/10.1007/s10240-003-0009-z
J. Milnor, Algebraic K-theory and quadratic forms, Invent. Math. 9 (1970), 318–344. https://doi.org/10.1007/BF01425486
H. Bass, J. Tate, The Milnor ring of a global field, in Algebraic K-theory II, Lecture Notes in Math. 342, Springer, 1973. https://doi.org/10.1007/BFb0073733
A. S. Merkurjev, A. A. Suslin, K-cohomology of Severi–Brauer varieties and the norm residue homomorphism, Math. USSR Izv. 21 (1983). https://doi.org/10.1070/IM1983v021n02ABEH001793
D. Orlov, A. Vishik, V. Voevodsky, An exact sequence for $K^M_*/2$ with applications to quadratic forms, Ann. of Math. 165 (2007), 1–13. https://doi.org/10.4007/annals.2007.165.1
V. Voevodsky, On motivic cohomology with $\mathbb{Z}/l$ -coefficients, Ann. of Math. 174 (2011), 401–438. https://doi.org/10.4007/annals.2011.174.1.11
C. Haesemeyer, C. Weibel, The Norm Residue Theorem in Motivic Cohomology, Annals of Math. Studies 200, Princeton, 2019. https://doi.org/10.1515/9780691189635
C. Mazza, V. Voevodsky, C. Weibel, Lecture Notes on Motivic Cohomology, Clay Math. Monographs 2, AMS, 2006. https://www.claymath.org/wp-content/uploads/2022/03/Motivic-Cohomology.pdf
A. Suslin, V. Voevodsky, Bloch–Kato conjecture and motivic cohomology with finite coefficients, in The Arithmetic and Geometry of Algebraic Cycles, NATO Sci. Ser. C 548, Kluwer, 2000. https://doi.org/10.1007/978-94-011-4098-0_5

14 thms2 active usersReviewed

Number Theory·Captain: tomasz

Philippon: Multiplicity estimates in commutative algebraic groupsResearch Paper

Why multiplicity estimates matter

Formalization status, 10 October 2026: all eight milestones are complete. Both corrected addenda are Proved. The subgroup upper Hilbert estimate has an accepted proof with eight Proved inputs and no Open dependencies (submission 07198c4c-ea10-4c9a-89b8-b4a5319c40b5). Together with the accepted sharp contact-rank and ambient lower Hilbert bounds, this discharges every dependency of the corrected converse. The corrected 26-part full-paper goal remains Open, with exactly two frontier leaves: quadratic parameter-stalk germs and the local complex model for the closure action. The common-shift forward conclusion, quadratic first-input addition hypothesis in the converse, all constants and degree thresholds, and all 24 unaffected goal clauses are unchanged. The separately published Chardin theorem in arbitrary characteristic remains Open; it is no longer required by this mission proof.

An auxiliary polynomial in a transcendence proof is constructed to vanish to high order at many points. A multiplicity estimate limits how often that can happen without a geometric reason: a positive-dimensional algebraic subgroup can make the apparent vanishing conditions dependent. Such estimates are used to turn analytic approximations into algebraic-independence conclusions. The theory applies to products of commutative algebraic groups with both archimedean and nonarchimedean analytic directions.

The mission's objective is a faithful formalization of the complete 1986 paper, Patrice Philippon's Lemmes de zéros dans les groupes algébriques commutatifs, including every theorem, corollary, proposition, lemma, definition, and mathematical supporting claim. All results remain required whether or not a current application uses them. Necessary source corrections are explicit and their counterexamples remain part of the completion goal. The author's 1987 corrections are applied transparently, and the addendum's additional results are recorded separately (original, errata and addenda).

Groups, analytic directions, and geometric degree

Let K be the complex field or the completed algebraic closure of the field of ℓ-adic numbers for a prime ℓ, as in the source. Let G be a product of finitely many commutative algebraic groups G₁,…,Gᵣ over K, with each factor embedded as a quasi-projective variety in a projective space. Write n for the sum of their dimensions. A point of the product embedding has one block of homogeneous coordinates for each factor.

A nonzero multihomogeneous polynomial P has a degree Dᵢ in its i-th block of coordinates. Its zeros define a hypersurface of the ambient product of projective spaces. An analytic subgroup A is locally parametrized by an analytic homomorphism from a finite-dimensional additive K-space. The order of P along A at a group point g is the vanishing order of P after composing local projective coordinates with the translated parametrization. This definition must be independent of the choice of nonzero local coordinate representatives.

Let Σ be a finite set of group points containing the identity. Its n-fold sumset Σ(n) consists of all sums of n, not necessarily distinct, elements of Σ; Σ(0) is the singleton identity. For a connected algebraic subgroup H, the integer s is the analytic codimension of A∩H in A. The expression |(Σ+H)/H| counts distinct H-cosets meeting Σ. Codimension concerns the analytic tangent dimension; it does not assert that the point-set intersection is finite.

The source's Hilbert degree form ℋ(V;D₁,…,Dᵣ) is (dim V)! times the highest homogeneous part of the multigraded Hilbert–Samuel polynomial of the projective closure of V, evaluated at the degrees. It must be constructed from the coordinate ring, rather than supplied as an arbitrary numerical function. For one projective factor it is deg(V)D^(dim V). These definitions are fixed in §§2–3 of the original paper.

Formalization targets

The completion target is all results of the paper, with an aggregate goal that requires their individual formal statements. Theorem 2.1 is one milestone within that target. For each fixed family of embedded group factors, it chooses positive integers cᵢ, each depending only on its corresponding embedding. These constants precede the analytic subgroup, the finite sampling set, the polynomial degrees, the polynomial, and the contact parameter T. If P has order at least nT+1 along A at every point of Σ(n), there is a connected algebraic subgroup H with

\binom{T+s}{s}\, |(\Sigma+H)/H|\, \mathcal H(H;D_1,\ldots,D_r) \leq \mathcal H(G;c_1D_1,\ldots,c_rD_r).

The same H is contained in a translate of the zero locus of P on G and is incompletely defined by equations of multidegrees at most (c₁D₁,…,cᵣDᵣ): it is an irreducible component of the common zero locus in G of equations with those degree bounds. Both geometric conclusions are part of the target. A formalization retaining only the displayed numerical inequality would omit part of the original result.

The 1986 paper has 13 numbered results. Section 2 contains Theorem 2.1 and Corollaries 2.2–2.3, including the one-dimensional analytic result and the result for disjoint group factors. Section 3 contains Lemmas 3.1–3.2, Proposition 3.3 and Lemma 3.4. Section 4 contains Propositions 4.3–4.4, Lemmas 4.5–4.6 and Proposition 4.7. Section 5 contains Lemma 5.1. Every clause of these statements belongs to the mission.

Definitions 3.5, 4.1 and 4.2, the unnumbered setup, the internal Facts A–E, the counterexample after Proposition 3.3, and the mathematical claims in remarks also require coverage. Source numbers and page references identify the correspondence between the prose and Lean declarations. The two 1987 addendum targets are explicitly corrected variants. The forward statement assumes ambient connectedness and allows one common shift $v\in G$ , so $g+v+H\subseteq\{P=0\}\cap G$ for every sampled $g$ , with the same connected subgroup $H$ satisfying incomplete definition and the full coset-count inequality. Its embedding-dependent constants are chosen before the sample and polynomial. This is not an exact transcription of the printed strengthening. The converse assumes ambient connectedness and explicit local addition formulas of degree at most two in the first input for every embedded factor. Its subgroup may remain disconnected; the degree threshold, constant $1/(4^n n!)$ , and polynomial nonzero somewhere on $G$ are unchanged. All original sampling and contact assumptions remain. No desired estimate is encoded as a geometric assumption.

Eight milestones and the completion goal

The completion goal is PhilipponMultiplicity.paper_results_corrected_erratum, a conjunction of 26 concrete propositions. This is a collection goal requiring the source statements and the additional mathematical claims in the coverage record. It is separate from the paper's original Theorem 2.1, which remains individually named and reusable.

The mission has eight milestones; seven are currently Proved:

Source	Milestone	Status
Theorem 2.1	General multiplicity estimate, with every geometric and numerical conclusion.	Proved
Corollary 2.2	One-dimensional analytic-subgroup consequence.	Proved
Corollary 2.3	Consequence for disjoint group factors and sampling grids.	Proved
Proposition 3.3	Multigraded intersection bounds, including the multiplicity-sensitive bound.	Proved
Proposition 4.7	Binomial lower bound for contact multiplicity.	Proved
Lemma 5.1	Stabilizer construction and the geometric counting estimate.	Proved
1987 addendum, p. 398	Corrected common-shift vanishing in a connected ambient group.	Proved
1987 addendum, p. 398	Connected converse with first-input addition degree at most two.	Open

The full statement package has 27 compiled theorem statements: all thirteen numbered results, both addenda, eleven supporting or correction targets, and the aggregate goal. The fourteen original admission-free definition bundles and one erratum supplement supply their actual geometric and algebraic objects. All 41 original statement and definition items have independent blind readbacks. The eight milestones above retain their existing identities.

The supporting clauses include Hilbert-polynomial existence, primary components and Facts A–E; the geometric interpretation of mixed degree; the actual counterexample after Proposition 3.3; translation operators and their comparison with intrinsic ideals; contact invariance; translation-invariance and embedding remarks; the component/stabilizer construction; counting estimates; and the exact Masser–Wüstholz Theorem I consequence claimed on p.361. Proof-internal recursive ideals and tangent/exponential arguments belong to their corresponding theorem proofs.

Source corrections are visible for review. Lemma 3.1 and Corollary 2.2 require positive equation degrees; explicit zero-degree counterexamples are required goal clauses. Both addenda require positive ambient dimension; the goal also requires their dimension-zero counterexamples. The three-generator ideal printed on p.370 is nonradical, contrary to the printed word “prime”; its valid degree-four versus length-six counterexample is preserved, together with an explicit nilpotent witness. Connectedness is stated in the translation-invariance and Lange reembedding remarks. These are mathematical corrections documented during the source comparison, beyond the author's 1987 errata. They are not silent changes to the source.

Existing completed proofs and all 24 unaffected goal clauses are retained. The corrected forward addendum is Proved. The repaired converse and the replacement collection goal remain Open; two general geometry lemmas also remain on the frontier. The existing proved local-algebra references remain reusable ingredients.

What a completed formalization enables

The output is a reusable development of the paper's multigraded commutative algebra, translation and differential operators, geometric multiplicity theory, and zero estimates. All source results are required for completion. A downstream Weierstrass application can consume a specialization of Theorem 2.1; its needs do not determine the scope or completion of this mission (example application).

These are established mathematical results whose proofs are being formalized. The complete original Theorem 2.1 has an accepted proof. The selected Weierstrass application uses individually named Philippon results, with its application-specific model and subgroup bridges proved in the Senthil mission. The remaining general results stay required even though that application is complete.

The foundational difficulty

Vanishing conditions need not be independent: many can occur on the same component or on translates with a nontrivial stabilizer. Counting coefficients of P therefore does not bound their total multiplicity. The development needs geometric degree for actual components, multiplicities measured by lengths of localized quotient rings, and uniform control of translations in fixed projective embeddings.

Proposition 3.3 supplies multigraded intersection bounds, Proposition 4.7 controls contact multiplicity, and Lemma 5.1 connects the stabilizer to the geometric counting estimate. These three results and Theorem 2.1 now have checked proofs. The remaining corollaries, general geometric and analytic claims, examples and addenda are independent deliverables. Application-specific contact results do not discharge the remaining general statements.

Formalization scope

The declarations use the namespace PhilipponMultiplicity. Source statements retain their conclusions, constants, quantifier order, and complex or ℓ-adic scope, with the visible boundary and wording corrections listed above. Intermediate specializations are labelled as such and do not discharge a more general source result. Natural-number and zero-degree conventions have been compared with the original scans; the discovered failures and corrected hypotheses are recorded explicitly for human review. Corrections and inferred conventions must be documented rather than silently changing the source.

The required definitions include embedded commutative algebraic groups and their connected subgroups; products of projective spaces and multihomogeneous coordinate rings; analytic local homomorphisms and intrinsic contact order; multigraded Hilbert polynomials and their degree forms; local component lengths; and finite coset counts. No model may assume the desired multiplicity inequality, hide it as a structure field, or replace geometric degree by an unconstrained function.

The 26 individual target statements, replacement collection goal, original definition bundles, and erratum supplement compile in Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Source comparisons and independent readbacks document the fixed statements and their explicit corrections. The goal remains the concrete 26-part full-paper collection. The completed proofs supply reusable Hilbert theory, primary-component multiplicities, polynomial differential operators, bounded translation atlases and the Section 5 construction. Contributions to the remaining targets, including results unused by Senthil, complete the original scope.

The previous aggregate, original sampled-translates addendum, and original converse remain available with their prior submissions and disproofs. The replacement statements changed the mission goal explicitly before proofs were supplied. The corrected common-shift forward statement has since received an accepted proof.

Selected references

P. Philippon, Lemmes de zéros dans les groupes algébriques commutatifs, Bulletin de la Société Mathématique de France 114 (1986), 355–383. DOI and original paper.
P. Philippon, Errata et addenda à « Lemmes de zéros dans les groupes algébriques commutatifs », Bulletin de la Société Mathématique de France 115 (1987), 397–398. DOI and addendum.
Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society (2026), including Robert Tubbs's appendix. DOI.

296 thms2 active users

Completed

Numerical Analysis·Captain: Lucas

Métodos Numéricos (Freitas) II: Zeros de Polinômios e o Algoritmo de HornerTextbook

Motivation

Polynomial equations are the special case of root finding where algebra says a great deal before analysis is needed: the number of roots is known, the roots of a real polynomial come in conjugate pairs, the rational candidates can be listed, and the whole complex plane can be narrowed down to an annulus that must contain every root. A numerical method that exploits this information starts closer to the answer and needs fewer evaluations; and each evaluation itself can be made cheaper by Horner's scheme, which also delivers the deflated quotient for free.

This mission is the second in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 4, Zeros de Polinômios.

Setting

Throughout, a polynomial is written in the book's convention

P(z) = a_0 z^n + a_1 z^{n-1} + \\dots + a_{n-1} z + a_n,

so the index $i$ names the coefficient of $z^{n-i}$ and $a_0$ is the leading coefficient. The coefficients are real (integral, in the rational-root milestone) and $z$ ranges over $\\mathbb{C}$ unless stated otherwise.

Horner's algorithm computes $P(c)$ by the recurrence $b_0 = a_0$ , $b_i = a_i + c\\,b_{i-1}$ , so that $P(c) = b_n$ , using $n$ multiplications and $n$ additions. The same numbers $b_0, \\dots, b_{n-1}$ are the coefficients of the deflated polynomial $Q$ with $P(w) = (w - c)\\,Q(w) + P(c)$ .

With $A = \\max\\{|a_1|, \\dots, |a_n|\\}$ and $B = \\max\\{|a_0|, \\dots, |a_{n-1}|\\}$ , the chapter's two localization results confine the roots to the annulus

\\frac{1}{1 + B/|a_n|} \\;\\le\\; |z| \\;\\le\\; 1 + \\frac{A}{|a_0|}.

Target

The goal theorem is the outer bound (Proposição 4.2.1): every complex root of $P$ satisfies $|z| \\le 1 + A/|a_0|$ , where $A$ is the largest absolute value among the non-leading coefficients.

The milestones are the companion results of the chapter: the inner bound (Proposição 4.2.2), the fact that non-real roots of a real polynomial occur in conjugate pairs (Proposição 4.1.1), the existence of a real root in odd degree (Proposição 4.1.2), the correctness of Horner's evaluation scheme, and the deflation identity that accompanies it.

Significance

The two localization bounds are what makes a search for complex roots finite: they give an explicit compact region to sweep, and they give scale information that prevents an iteration from wandering off. The conjugate-pair statement halves the work for real polynomials and is the reason odd-degree real polynomials always have a real root. The rational-root test turns exact factorization into a finite search. Horner's scheme is the standard way a polynomial is evaluated inside every root finder, and its deflation identity is what lets a method remove a root that has already been found and continue with a polynomial of lower degree.

Mathlib already contains general results close to some of these (a polynomial over a real closed field of odd degree has a root; rational-root divisibility), so those milestones are accessible; the two localization bounds and the Horner statements in the book's index convention are the substantive new work.

Difficulty

The localization proofs in the source are short but rest on a geometric-series estimate that is only valid for $|z| > 1$ ; the boundary cases $|z| \\le 1$ have to be treated separately in a formal proof, and the degenerate situations ( $n = 1$ , coefficients all zero except the leading one) must be checked rather than waved through. The inner bound is obtained from the outer one by the substitution $w = 1/z$ , which requires knowing that $z \\neq 0$ is a root of $P$ if and only if $w$ is a root of the reversed polynomial — an argument that has to be made explicit. The Horner statements look computational but need a careful induction because the exponents are natural-number subtractions.

Formalization scope

Coefficients are given as a function $a : \\mathbb{N} \\to \\mathbb{R}$ together with a degree $n$ , and the polynomial is the finite sum $\\sum_{i=0}^{n} a_i z^{n-i}$ ; two versions are provided, one evaluated at a real point and one at a complex point, with the coefficients coerced into $\\mathbb{C}$ . Only indices $0 \\le i \\le n$ are read, so the values of $a$ beyond $n$ are irrelevant to every statement. The exponent $n - i$ is natural-number subtraction, which is harmless in this range. No hypothesis says that the family $a$ describes a polynomial of exact degree $n$ beyond the explicit assumptions $a_0 \\neq 0$ or $a_n \\neq 0$ where they appear. The constants $A$ and $B$ are given as hypotheses equating them to the maximum of the relevant finite family of absolute values, rather than being defined separately. The rational-root and odd-degree milestones are stated with Mathlib's polynomial type instead of the coefficient-family encoding, since their statements involve no index convention.

Selected references

S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 4, Zeros de Polinômios, pp. 71–84. (Course notes supplied with this mission.)

8 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Brown-Gabrielse Invariance Theorem for an Imperfect Penning TrapResearch Paper

Motivation

The most precisely measured property of an elementary particle is the magnetic moment of the electron. The 2022 Northwestern measurement of Fan, Myers, Sukra and Gabrielse (arXiv:2209.13084) reports $-\mu/\mu_B=g/2=1.001\,159\,652\,180\,59\,(13)$ , and, combined with the Standard-Model prediction, $\alpha^{-1}=137.035\,999\,166\,(15)$ . Those numbers are experimental results, not theorems, and nothing in this mission asserts them.

What is a theorem is the piece of mathematics the measurement rests on. A single electron is held in a Penning trap: a uniform magnetic field plus an electrostatic quadrupole potential. The quantity the experiment needs is the free-space cyclotron frequency $\nu_c=eB/(2\pi m)$ , but what a trap lets you observe are its three normal-mode frequencies — the trap-modified cyclotron frequency $\bar\nu_c$ , the axial frequency $\bar\nu_z$ , and the magnetron frequency $\bar\nu_m$ . A real apparatus is never perfect: the magnetic field is tilted relative to the axis of the potential, and the potential is elliptically distorted. The invariance theorem of Brown and Gabrielse (Phys. Rev. A 25, 2423 (1982)), quoted as Eq. (4) of the measurement paper, says that a particular combination of the three observed frequencies is completely insensitive to both imperfections:

\nu_c=\sqrt{\bar\nu_c^{2}+\bar\nu_z^{2}+\bar\nu_m^{2}}.

This is what makes a part-per-trillion measurement possible with an imperfect trap, and it is the object of this mission.

Setting

Work in $\mathbb{R}^3$ . A particle of charge $q$ and mass $m$ sits in a uniform magnetic field $\mathbf B=B\,b$ with $b$ a unit vector, and in the static field of a quadratic electrostatic potential. Dividing the Hessian of that potential by the mass gives a real $3\times3$ matrix $K$ , and the equation of motion of the particle is linear:

r''(t)\;=\;-K\,r(t)\;+\;\omega_c\,\big(r'(t)\times b\big),\qquad \omega_c=\frac{qB}{m}.

Two properties of $K$ carry all the physics of the trap: $K$ is symmetric, because it is a Hessian, and traceless, because the potential satisfies Laplace's equation in the vacuum region where the particle moves. Beyond that, $K$ is arbitrary — an arbitrary $K$ is exactly what "the axis of the potential is tilted relative to $b$ , and the potential is elliptically distorted" means, so no separate tilt angle or ellipticity parameter appears anywhere.

Substituting the ansatz $r(t)=u\,e^{-i\omega t}$ with $u\in\mathbb{C}^3$ turns the equation of motion into the linear system $M(\omega)\,u=0$ , where

M(\omega)\;=\;K-\omega^{2}I-i\,\omega\,\omega_c\,C(b), \qquad C(b)=\begin{pmatrix}0&-b_3&b_2\\ b_3&0&-b_1\\ -b_2&b_1&0\end{pmatrix}

is the matrix of $u\mapsto b\times u$ . A frequency $\omega$ is a normal mode of the trap precisely when $\det M(\omega)=0$ . The three eigenfrequencies of the trap, written $\bar\omega_c,\bar\omega_z,\bar\omega_m$ (angular versions of $\bar\nu_c,\bar\nu_z,\bar\nu_m$ ), are the non-negative solutions of that equation.

Target

The goal is the invariance theorem in the form: if the three numbers $\bar\omega_c,\bar\omega_z,\bar\omega_m$ are the eigenfrequencies of the trap, in the sense that

\det M(\omega)=-\big(\omega^{2}-\bar\omega_c^{2}\big)\big(\omega^{2}-\bar\omega_z^{2}\big)\big(\omega^{2}-\bar\omega_m^{2}\big)\quad\text{for all }\omega\in\mathbb{R},

then, for every symmetric traceless $K$ and every unit vector $b$ ,

\bar\omega_c^{2}+\bar\omega_z^{2}+\bar\omega_m^{2}\;=\;\omega_c^{2}.

The milestones are the three steps of the argument, in increasing order of dependence:

Mode equation. The exponential ansatz solves the equation of motion at every time if and only if its amplitude lies in the kernel of $M(\omega)$ . This is what makes $M(\omega)$ the right object to take determinants of.
Characteristic polynomial. For symmetric $K$ , $\det M(\omega)$ is real and depends on $\omega$ only through $\omega^2$ : it equals $-q(\omega^2)$ with $q(\lambda)=\det(\lambda I-K)-\omega_c^{2}\lambda(\lambda\langle b,b\rangle-\langle b,Kb\rangle)$ .
Ideal trap. For $K=\operatorname{diag}(-\omega_z^2/2,-\omega_z^2/2,\omega_z^2)$ , $b=(0,0,1)$ and $\omega_c^2\ge 2\omega_z^2$ , the determinant factors explicitly, with eigenfrequencies $(\omega_c\pm\sqrt{\omega_c^2-2\omega_z^2})/2$ and $\omega_z$ .

Significance

The result. The invariance theorem is why the electron magnetic moment can be measured to $0.13$ parts per trillion in an apparatus whose magnetic field and electrode axis are not, and cannot be, exactly aligned. Without it, every misalignment and every elliptic distortion would enter the extracted $\nu_c$ as a systematic error, and the frequency ratio $\nu_a/\nu_c$ that gives $g/2$ would have to be corrected with a model of the imperfections rather than being invariant under them.

Formalizing it. The theorem is a short, completely classical piece of linear algebra — the point of formalizing it is to have the frequency-metrology identity available as a machine-checked statement, together with a reusable model of linear motion in crossed electric and magnetic fields (the mode matrix, its characteristic cubic, and the correspondence between the exponential ansatz and the kernel of the mode matrix).

Status — please read before treating this as open. All four statements in this proposal have been proved by the drafting agent on a local Lean 4.28 / Mathlib installation; the proofs are deliberately not uploaded, so the platform statements are genuinely open here, but this is a formalization-transfer mission, not an open research problem. Milestone 3 is included precisely so that the goal's factorization hypothesis is known to be satisfiable and the goal is not vacuously true. The statements themselves were additionally compiled in this platform's default Lean environment before this proposal was assembled.

Difficulty

The obvious first idea — solve $\det M(\omega)=0$ and add up the roots — is exactly the thing not to do: for a tilted, elliptically distorted trap the three eigenfrequencies have no usable closed form. The whole content of the theorem is that the sum of their squares is the coefficient of $\omega^4$ in the characteristic polynomial and therefore needs no root formula at all: it is Vieta plus the two structural facts $\operatorname{tr}K=0$ and $\langle b,b\rangle=1$ . The work in Lean is consequently not analysis but bookkeeping: computing a $3\times3$ determinant with complex off-diagonal entries and extracting one coefficient of the resulting cubic in $\omega^2$ . The one place real care is needed is the mode-equation milestone, where derivatives of complex-valued functions of a real variable must be handled honestly.

Formalization scope

Conventions fixed by the Lean statements, and not visible in the prose:

Vectors are functions on a three-element index set and matrices are $3\times3$ ; no abstract inner-product space is used.
$K$ is an arbitrary real matrix in the definitions; symmetry and tracelessness are hypotheses on the individual theorems, not part of the model.
"Unit vector" is the algebraic condition $\langle b,b\rangle=1$ ; no norm is used.
The magnetic term is $-i\,\omega\,\omega_c\,C(b)$ with $C(b)u=b\times u$ , i.e. the sign convention is fixed by the ansatz $r(t)=u\,e^{-i\omega t}$ and the force $\omega_c\,(r'\times b)$ .
"The eigenfrequencies are $\bar\omega_c,\bar\omega_z,\bar\omega_m$ " is formalized as the functional identity $\det M(\omega)=-(\omega^2-\bar\omega_c^2)(\omega^2-\bar\omega_z^2)(\omega^2-\bar\omega_m^2)$ for all real $\omega$ — that is, as a factorization with multiplicity, not as a set of solutions of $\det M(\omega)=0$ , which would not pin down multiplicities and would make the sum rule false in degenerate cases.
No sign conditions are imposed on $\bar\omega_c,\bar\omega_z,\bar\omega_m$ ; the conclusion involves only their squares.
Nothing in this mission formalizes any measured quantity: $g/2$ , $\alpha$ , and the frequencies of the actual apparatus appear only as motivation.

Only Mathlib is needed: matrices over $\mathbb{R}$ and $\mathbb{C}$ , determinants of $3\times3$ matrices, the cross product, and derivatives of complex-valued functions of a real variable. The definitions are reusable for any linear-motion-in-a-magnetic-field problem.

Selected references

X. Fan, T. G. Myers, B. A. D. Sukra, G. Gabrielse, Measurement of the Electron Magnetic Moment, Phys. Rev. Lett. 130, 071801 (2023), arXiv:2209.13084 — Eq. (4) is the statement formalized here.
L. S. Brown, G. Gabrielse, Precision spectroscopy of a charged particle in an imperfect Penning trap, Phys. Rev. A 25, 2423 (1982), doi:10.1103/PhysRevA.25.2423 — the original invariance theorem.
L. S. Brown, G. Gabrielse, Geonium theory: Physics of a single electron or ion in a Penning trap, Rev. Mod. Phys. 58, 233 (1986), doi:10.1103/RevModPhys.58.233 — the trap eigenfrequencies and the hierarchy $\bar\nu_c\gg\bar\nu_z\gg\bar\nu_m$ .

5 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Koide Mass Relation: Exact Algebraic ContentResearch Paper

Motivation

In 1982 Yoshio Koide, searching for an empirical formula for the Cabibbo angle, noticed that the three charged-lepton masses satisfy

m_e + m_\mu + m_\tau \;=\; \frac{2}{3}\left(\sqrt{m_e}+\sqrt{m_\mu}+\sqrt{m_\tau}\right)^2 .

With the present-day values $m_e = 0.510998910 \pm 0.000000013$ MeV, $m_\mu = 105.6583663 \pm 0.0000038$ MeV and $m_\tau = 1776.99 \pm 0.29$ MeV, the dimensionless ratio on the left over the bracket on the right equals $0.666667 \pm 0.000016$ — the value $\tfrac{2}{3}$ to five digits. Whether this is numerology or a shadow of flavour physics beyond the Standard Model is an open physics question; what is not open, and what this mission is about, is the exact mathematical content of the relation: which triples of nonnegative reals satisfy it, what its polynomial (square-root-free) consequences are, and what its geometric reading is.

The material formalized here is Chapter 3 ("A Mass Relation") of F. Goffinet's 2008 doctoral thesis A bottom-up approach to fermion masses (Université catholique de Louvain), which collects the algebraic and geometric properties of the relation and proposes a mixing-matrix generalization. None of the statements below depends on any physics input: they are elementary real-algebraic facts about the function $q$ defined next. The physics enters only in which numbers one plugs in.

Setting

For a family of $n$ nonnegative "masses" $m = (m_1,\dots,m_n)$ , not all zero, define the Koide splitting parameter

q(m) \;=\; \frac{\sum_{i} m_i}{\bigl(\sum_i \sqrt{m_i}\bigr)^{2}} .

In Lean this is koideRatio, defined by exactly this quotient for m : Fin n → ℝ (with Lean's convention that $\sqrt{x}=0$ for $x<0$ and $x/0 = 0$ , so the definition is total; every statement in the mission carries the nonnegativity and nondegeneracy hypotheses that make it meaningful).

Two further objects from the chapter are formalized alongside it.

The degeneracy angle. Put $S = (\sqrt{m_1},\dots,\sqrt{m_n})$ in "generation space" and let $\psi$ be the angle between $S$ and the democratic direction $(1,\dots,1)$ . In Lean, koideCos is the cosine $\langle S,\mathbf 1\rangle/(\lVert S\rVert\,\lVert\mathbf 1\rVert)$ written out as a quotient of sums, and koideAngle is its $\arccos$ .
The pseudo-masses of the chapter's generalization: given a mixing matrix $U \in \mathbb{C}^{n\times n}$ , $\tilde m_i = \bigl|\sum_j U_{ij} m_j\bigr|$ (pseudoMass).

Koide's relation is the statement $q(m_e,m_\mu,m_\tau) = \tfrac{2}{3}$ ; the value $q=\tfrac13$ corresponds to exact degeneracy $m_1=m_2=m_3$ and $q=1$ to maximal hierarchy.

Target

The goal theorem is the exact solution of the relation for the third mass. For $m_1,m_2,m_3>0$ , writing $P = \sqrt{m_1 m_2}$ and $R = \sqrt{m_1 + 4P + m_2}$ ,

q(m_1,m_2,m_3) = \tfrac{2}{3} \iff m_3 = 7(m_1+m_2) + 20P + 4\sqrt3\,(\sqrt{m_1}+\sqrt{m_2})R

\textrm{or}\quad \bigl(\, 4P < m_1+m_2 \ \textrm{ and }\ m_3 = 7(m_1+m_2) + 20P - 4\sqrt3\,(\sqrt{m_1}+\sqrt{m_2})R \,\bigr).

This is equation (3.25) of the source, made precise: the " $-$ " branch of (3.25) is a genuine solution exactly when $4\sqrt{m_1m_2} < m_1+m_2$ , and is a spurious root of the squared equation otherwise (for instance at $m_1=m_2$ , where the " $-$ " value is positive but fails the relation).

The milestones cover, in the source's order: the range $\tfrac1n \le q \le 1$ and its two equality cases (Table 3.1); the geometric reading $\cos\psi = 1/\sqrt{n\,q}$ and the equivalence $\psi = 45^\circ \iff q = \tfrac23$ (eq. (3.5)–(3.6), Fig. 3.1); the square-root-free polynomial consequence (eq. (3.24)) and its matrix form (eq. (3.30)); the failure of the converse (eqs. (3.26)–(3.28)); the $\sum_i z_i = 0$ reformulation in the composite-model parametrization (eqs. (3.18)–(3.22)); the $\tau$ -mass prediction (eq. (3.4)); and the fact that the pseudo-mass extension (3.31)–(3.32) reduces to the original relation at $U = \mathrm{Id}$ .

Significance

The result itself. The goal theorem turns an empirical numerical coincidence into a complete description of its solution set: given any two masses, it says exactly which third masses are admissible, and it separates the two roots by an explicit inequality. This is what licenses the standard use of the relation as a prediction: fixing $m_e$ and $m_\mu$ and the normal hierarchy $m_\tau > m_\mu$ singles out one root, giving $m_\tau = 1776.968874$ MeV, a number two orders of magnitude more precise than the direct measurement (milestone on eq. (3.4)). The bound $\tfrac13 \le q \le 1$ with its equality cases explains why the relation can never hold for the neutrinos in a near-degenerate spectrum, and why the up-quark family sits near the opposite boundary. The square-root-free form (3.24)/(3.30) is what any Lagrangian-level model must reproduce, since square roots of masses do not appear in a mass matrix; the failure of its converse is the price paid for removing them, and the mission pins that failure down with an explicit witness.

Formalizing it. All the statements here are classical-strength real algebra, and none is formalized in Mathlib: there is no koideRatio, no Cauchy–Schwarz-style equality analysis for the $\sum m$ vs. $(\sum\sqrt m)^2$ pair, and no treatment of the $45^\circ$ geometry. The mission produces a small reusable development — the parameter, its sharp bounds with equality cases, and its angle formulation — that any later formalization of mass-relation phenomenology can import. It also records, machine-checked, where the source text is imprecise: the " $\pm$ " discussion after (3.25) and the claim that (3.1) has exactly two solutions for the third mass.

Difficulty

Nothing here needs heavy machinery, and everything here needs care with square roots.

The bounds are Cauchy–Schwarz in one direction and $\bigl(\sum\sqrt{m_i}\bigr)^2 \ge \sum m_i$ in the other, but the equality cases are where the work is: the upper bound saturates exactly when at most one mass is nonzero, and a proof must handle the mixed terms without assuming positivity of all entries. The goal theorem is a quadratic in $z = \sqrt{m_3}$ — $z^2 - 4(x+y)z + (x^2+y^2-4xy) = 0$ with $x=\sqrt{m_1}$ , $y=\sqrt{m_2}$ — so the difficulty is not solving it but keeping the equivalence exact in both directions: passing from $m_3$ back to $z$ requires $z \ge 0$ , which is precisely where the " $-$ " branch survives or dies, and the discriminant has to be recognized as a perfect square times $3$ . The obvious route of squaring the relation twice, as the source does to reach (3.24), is not reversible; a solver who squares must come back and discharge the sign conditions, and the counterexample milestone shows that the lost information is real.

Formalization scope

Masses are real numbers, not physical quantities with units, and are indexed by Fin n (Fin 3 for the three-generation statements); the mixing matrix in the pseudo-mass definition is complex, as in the source. koideRatio, koideCos, koideAngle and pseudoMass are total functions and rely on Lean's junk conventions outside their intended domain, so each statement carries its own hypotheses — nonnegativity of every entry and the existence of a strictly positive entry — rather than delegating them to the definitions. No statement is vacuous: every hypothesis set is satisfied by the physical charged-lepton triple, and the degenerate configurations the quantifiers admit (all-zero families, the $n=0$ family) are excluded by those hypotheses rather than by a side condition that can never hold.

The angle statements use Real.arccos and are stated for the cosine written out as an explicit quotient of sums, not through an inner-product-space instance; a solver is free to route the proof through EuclideanSpace if that is convenient. The matrix milestone uses Matrix.IsHermitian.eigenvalues for a $3\times3$ complex Hermitian matrix and states the conclusion as an identity in $\mathbb{C}$ between $\operatorname{tr} M$ , $\operatorname{tr} M^2$ and $\det M$ . Contributions of general- $n$ versions of the three-generation statements, and of the equality analysis as standalone lemmas, are welcome.

Selected references

F. Goffinet, A bottom-up approach to fermion masses, PhD thesis, Université catholique de Louvain, December 2008. Chapter 3, pp. 59–86. http://hdl.handle.net/2078.1/20873
Y. Koide, A fermion–boson composite model of quarks and leptons, Phys. Lett. B 120 (1983) 161–165. https://doi.org/10.1016/0370-2693(83)90644-5
Y. Koide, Challenge to the mystery of the charged lepton mass formula, https://arxiv.org/abs/hep-ph/0506247
R. Foot, A note on Koide's lepton mass relation, https://arxiv.org/abs/hep-ph/9402242 (the $45^\circ$ geometric reading).
J.-M. Gérard, F. Goffinet, M. Herquet, A new look at an old mass relation, Phys. Lett. B 633 (2006) 563–566. https://arxiv.org/abs/hep-ph/0510289 (the pseudo-mass extension).

13 thms2 active usersReviewed

Completed

Arithmetic Geometry Number Theory·Captain: Lucas

Lectures on Analytic Geometry I: $\mathbb{Z}((T))_{>r}$ is a principal ideal domainTextbook

Motivation

Rings of arithmetic power series — power series with integer coefficients that converge on a disc of radius close to $1$ — sit between algebra and analysis: an element has both archimedean zeros, in the complex disc, and non-archimedean ones, at $p$ -adic points. Harbater (Convergent arithmetic power series, Amer. J. Math. 106 (1984), 801–846, DOI 10.2307/2374325) showed that a well-chosen ring of such series is a principal ideal domain and identified its prime ideals; the same ring is the arithmetic model of the closed disc of radius $r$ in the adic space $\mathrm{Spa}(\mathbb{Z}[[T]])$ .

The result was put to work in Clausen–Scholze's Lectures on Analytic Geometry (Lecture VII), where $\mathbb{Z}((T))_{>r}$ supplies a two-term presentation of the real numbers as a condensed abelian group: for $0 < r' < r < 1$ there is an exact sequence $0 \to \mathbb{Z}((T))_r \xrightarrow{f_{r'}} \mathbb{Z}((T))_r \to \mathbb{R} \to 0$ , whose existence rests on the principality of the kernel of evaluation at $r'$ . The quantitative refinement of that sequence (Propositions 7.2 and 7.3 of the notes) is what produces the $\ell^p$ -norms in the analytic ring structure on $\mathbb{R}$ .

Setting

Fix a real number $r$ with $0 < r < 1$ . An integral Laurent series is a family of integers $(a_n)_{n \in \mathbb{Z}}$ whose support is bounded below, written $f = \sum_{n \gg -\infty} a_n T^n$ ; these form the ring $\mathbb{Z}((T))$ under coefficientwise addition and the Cauchy product.

Define

\mathbb{Z}((T))_{>r} \;=\; \Big\{\, \sum_{n \gg -\infty} a_n T^n \;\Big|\; \exists\, s > r,\ |a_n|\, s^{\,n} \xrightarrow[n \to \infty]{} 0 \,\Big\} \;\subseteq\; \mathbb{Z}((T)).

Concretely, $f$ lies in $\mathbb{Z}((T))_{>r}$ when the associated Laurent expansion converges on some punctured disc $\{0 < |y| < s\}$ with $s > r$ strictly larger than $r$ — an overconvergence condition. For $x$ a real or complex number, $f(x) = \sum_{n} a_n x^{\,n}$ denotes the evaluation, whenever the family is summable.

Two features distinguish this ring from the classical Tate algebra. The coefficients are integers, not elements of a complete field, so reduction modulo a prime $p$ is available and produces $\mathbb{F}_p((T))$ . And the condition is an overconvergence condition: the radius $s$ is required to be strictly larger than $r$ , which is what makes the ring behave like the ring of functions on a closed disc rather than an open one.

Formalization targets

Goal

0 < r < 1 \;\Longrightarrow\; \mathbb{Z}((T))_{>r} \text{ is a principal ideal domain.}

The ring is a subring of the domain $\mathbb{Z}((T))$ , so integrality is automatic and the content of the goal is that every ideal is generated by one element.

The prime ideals (context, not a formalization target here)

Theorem 7.1 of the source also classifies the nonzero primes: kernels of evaluation at a complex $x$ with $0 < |x| \le r$ (up to conjugation); the ideals $(p)$ for $p$ prime; and kernels of evaluation at a topologically nilpotent unit $x$ of a finite extension of $\mathbb{Q}_p$ (up to Galois conjugacy). The milestones below formalize the parts of the classification that the principality proof actually consumes — surjectivity of the three evaluation maps, and principality of the archimedean kernels — and leave the full classification statement for a later mission in this series.

Significance

The result itself. Principality gives, for each point of the closed disc, a single equation cutting it out; that is exactly what the presentation $0 \to \mathbb{Z}((T))_r \to \mathbb{Z}((T))_r \to \mathbb{R} \to 0$ needs. Downstream, that presentation is the input to the computation of measures on $\mathbb{R}$ in the analytic-ring formalism, and the reason $\ell^p$ -spaces with $p < 1$ appear there at all. Without it, one has no finite free resolution of $\mathbb{R}$ by rings of arithmetic functions, and the structure results of Lectures VI–VII of the source lose their computational base.

Formalizing it. The mathematics is classical and fully proved; nothing here is open. What is missing is a machine-checked version. Mathlib has Hahn series, Laurent series, complex analysis on discs, and the $p$ -adic numbers, but nothing about arithmetic overconvergent series: not the ring itself, not the greedy expansions that make real evaluation surjective, not the invertibility criterion. Each milestone below is a self-contained piece of that missing theory, reusable outside this mission.

Difficulty

The obvious approach — Weierstrass preparation, as for the Tate algebra $K\langle T\rangle$ over a complete field $K$ — does not apply: the coefficient ring $\mathbb{Z}$ is not a field, and no single valuation controls it. An element of $\mathbb{Z}((T))_{>r}$ must be divided simultaneously by archimedean generators (complex zeros in the disc) and $p$ -adic ones, with the quotient required to stay integral and still overconvergent. Two steps carry the weight and fail for naive reasons:

Producing an integral generator for the kernel of evaluation at a real or complex $x$ : one first needs a real polynomial $g \in 1 + T^n\mathbb{R}[T]$ with $x$ as its only zero in $\{0 < |y| \le r\}$ , then a correction series $h$ with small coefficients such that $gh$ has integer coefficients. Neither factor alone is integral.
Showing that an element of $1 + T\mathbb{Z}[[T]]$ with no zero in the closed disc of radius $r$ is invertible in the ring: the inverse is integral for formal reasons, but its overconvergence is an analytic statement about the absence of zeros.

Finiteness — that a nonzero element lies in only finitely many of the listed maximal ideals — mixes the identity theorem for holomorphic functions with a $p$ -adic Weierstrass argument, which is why the reduction and $p$ -adic surjectivity milestones are prerequisites rather than side remarks.

Formalization scope

The ambient ring is Mathlib's LaurentSeries ℤ (Hahn series over $\mathbb{Z}$ indexed by $\mathbb{Z}$ ), and $\mathbb{Z}((T))_{>r}$ is given as a set of such series, cut out by the decay condition $|a_n| s^{\,n} \to 0$ as $n \to +\infty$ for some $s > r$ . Evaluations are unordered sums over $\mathbb{Z}$ ; where a statement asserts a value of an evaluation, summability is asserted alongside it, so the junk value of a divergent sum cannot be exploited.

Because the carrier is a set, the goal theorem is stated for an arbitrary subring of $\mathbb{Z}((T))$ whose underlying set is $\mathbb{Z}((T))_{>r}$ . That form would be vacuous if no such subring existed, which is precisely why the first milestone asserts its existence; the two together carry the intended content, and the mission is not considered advanced by the goal alone.

Milestone 6 formalizes only the case $K = \mathbb{Q}_p$ of part (3) of the source theorem (topologically nilpotent units of proper finite extensions of $\mathbb{Q}_p$ are out of scope, since Mathlib lacks the ambient theory of such extensions). Milestone 3 drops the "with multiplicity one" clause of the source and asserts only that the zero set in the punctured closed disc is $\{x\}$ .

A complete development will need: closure of the decay condition under the Cauchy product; summability of evaluations on the closed disc; the identity theorem for the induced holomorphic functions; greedy $x$ -adic expansions of real numbers with bounded integer digits; and $p$ -adic expansions in the lattice generated by a topologically nilpotent unit. Contributions of any of these, as standalone lemmas, are welcome.

Selected references

D. Harbater, Convergent arithmetic power series, American Journal of Mathematics 106 (1984), 801–846. DOI 10.2307/2374325
P. Scholze (joint with D. Clausen), Lectures on Analytic Geometry, Bonn, 2019/20; Lecture VII, Theorem 7.1. PDF
P. Scholze (joint with D. Clausen), Lectures on Condensed Mathematics, Bonn, 2019. PDF

9 thms2 active usersReviewed

Number Theory·Captain: Lucas

Schanuel's ConjectureOpen Problem

Motivation

Almost every classical transcendence theorem is a statement about the interaction between the additive structure of $\mathbb{C}$ and the exponential function. Hermite proved in 1873 that $e$ is transcendental, Lindemann in 1882 that $e^{\alpha}$ is transcendental for every nonzero algebraic $\alpha$ — hence that $\pi$ is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of $e^{\alpha_1},\dots,e^{\alpha_n}$ over $\overline{\mathbb{Q}}$ for distinct algebraic $\alpha_i$ . Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.

Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that $e$ and $\pi$ are algebraically independent, or that $e + \pi$ is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.

Timeline, with the hypotheses each result actually assumes:

1882, Lindemann: $e^{\alpha}$ is transcendental for algebraic $\alpha \neq 0$ .
1885, Weierstrass: for pairwise distinct algebraic $\alpha_1,\dots,\alpha_n$ , the values $e^{\alpha_1},\dots,e^{\alpha_n}$ are linearly independent over $\overline{\mathbb{Q}}$ .
1934, Gelfond and Schneider, independently: if $\lambda \neq 0$ is a logarithm of an algebraic number and $\beta$ is algebraic and irrational, then $e^{\beta\lambda}$ is transcendental.
1960s, Siegel, Lang and Ramachandra: the six exponentials theorem, unconditional; the analogous four exponentials statement is still open.
1966, Baker: if logarithms $\lambda_1,\dots,\lambda_n$ of algebraic numbers are linearly independent over $\mathbb{Q}$ , then $1,\lambda_1,\dots,\lambda_n$ are linearly independent over $\overline{\mathbb{Q}}$ .
1971, Ax: the function-field analogue of Schanuel's conjecture, for formal power series and, more generally, differential fields of characteristic zero.

Setting

Write $\exp$ for the complex exponential function. A tuple $z_1,\dots,z_n$ of complex numbers is linearly independent over $\mathbb{Q}$ when the only rationals $q_1,\dots,q_n$ with $\sum_i q_i z_i = 0$ are $q_1 = \dots = q_n = 0$ ; here $\mathbb{C}$ is viewed as a vector space over $\mathbb{Q}$ .

For a subset $S \subseteq \mathbb{C}$ , let $\mathbb{Q}(S)$ denote the subfield of $\mathbb{C}$ generated by $S$ over $\mathbb{Q}$ . The transcendence degree $\operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}(S)$ is the cardinality of a transcendence basis of $\mathbb{Q}(S)$ over $\mathbb{Q}$ : the largest number of elements of $\mathbb{Q}(S)$ that are algebraically independent over $\mathbb{Q}$ . A number $x$ is transcendental over $\mathbb{Q}$ when no nonzero polynomial with rational coefficients vanishes at $x$ , and numbers $x_1,\dots,x_m$ are algebraically independent over $\mathbb{Q}$ when no nonzero polynomial in $m$ variables with rational coefficients vanishes at $(x_1,\dots,x_m)$ .

Formalization targets

Goal

z_1,\dots,z_n \text{ linearly independent over } \mathbb{Q} \;\Longrightarrow\; \operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}\bigl(z_1,\dots,z_n,\,e^{z_1},\dots,e^{z_n}\bigr) \;\ge\; n .

The goal fixes no numerical constant and no special shape for the $z_i$ : it asserts only the inequality, for every $n$ and every $\mathbb{Q}$ -linearly independent tuple. The case $n = 0$ is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.

Milestones

The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:

Hermite–Lindemann (1882): $\alpha$ algebraic and nonzero $\Rightarrow$ $e^{\alpha}$ transcendental.
Lindemann–Weierstrass (1885): $\sum_i \beta_i e^{\alpha_i} \neq 0$ for distinct algebraic $\alpha_i$ and algebraic $\beta_i$ not all zero.
Gelfond–Schneider (1934): $\lambda \neq 0$ a logarithm of an algebraic number, $\beta$ algebraic irrational $\Rightarrow$ $e^{\beta\lambda}$ transcendental.
Six exponentials theorem: $x_1,x_2$ and $y_1,y_2,y_3$ each $\mathbb{Q}$ -linearly independent $\Rightarrow$ at least one of the six numbers $e^{x_i y_j}$ is transcendental.
Baker (1966): $\mathbb{Q}$ -linearly independent logarithms of algebraic numbers, together with $1$ , are linearly independent over $\overline{\mathbb{Q}}$ .
Ax (1971), power series form: $\operatorname{trdeg}_{\mathbb{C}} \mathbb{C}(f_1,\dots,f_n,g_1,\dots,g_n) \ge n+1$ when $g_i' = f_i' g_i$ , the $g_i$ are units, and no nontrivial $\mathbb{Q}$ -linear combination of the $f_i$ is constant.
Conditional corollary: Schanuel's conjecture implies that $e$ and $\pi$ are algebraically independent over $\mathbb{Q}$ .

Significance

Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of $e$ and $\pi$ , the irrationality of $e+\pi$ and of $e\pi$ , the transcendence of $e^{e}$ and $\pi^{\pi}$ , the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic $z_i$ is exactly the Lindemann–Weierstrass theorem, and its restriction to $z_i$ whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.

On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of $\pi$ , the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.

Difficulty

The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general $\mathbb{Q}$ -linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.

Formalization scope

All statements are over $\mathbb{C}$ , with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.

There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every $n$ , so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.

The Ax milestone is stated for formal power series in one variable over $\mathbb{C}$ : the exponential relation is expressed as the differential equation $g_i' = f_i' g_i$ with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the $f_i$ and the $g_i$ . The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.

Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.

Selected references

S. Lang, Introduction to Transcendental Numbers, Addison–Wesley, 1966. (Schanuel's conjecture is stated in Chapter III.)
A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216. https://doi.org/10.1112/S0025579300003971
J. Ax, On Schanuel's conjectures, Annals of Mathematics 93 (1971), 252–268. https://doi.org/10.2307/1970774
A. Macintyre and A. J. Wilkie, On the decidability of the real exponential field, in Kreiseliana, A K Peters, 1996, 441–467.
M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Springer, 2000.
Wikipedia, Schanuel's conjecture. https://en.wikipedia.org/wiki/Schanuel%27s_conjecture

39 thms2 active usersReviewed

Completed

Category Theory·Captain: Lucas

Ideals in Balanced Algebras: the Gregarious IdealResearch Paper

Motivation

A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation $a\cdot b$ that need not be defined for every pair. Under one axiom — balance, which asserts that $(ab)c$ is defined exactly when $a(bc)$ is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.

No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).

Setting

An algebra on a type $A$ is a partial binary operation: a rule assigning to some pairs $(a,b)\in A\times A$ a value $a\cdot b\in A$ . Write $a\cdot b\downarrow$ for " $a\cdot b$ is defined". In the Lean development the operation is a total function $A\to A\to\mathrm{Option}\,A$ , where the value $\mathrm{none}$ means undefined. Nothing else is assumed: no totality, no unit, no associativity.

The vocabulary used throughout, all relative to this one partial product:

$B\subseteq A$ is a left ideal if $a\cdot b\in B$ whenever $b\in B$ and $a\cdot b\downarrow$ ; a right ideal if $b\cdot a\in B$ whenever $b\in B$ and $b\cdot a\downarrow$ ; a subalgebra if $b\cdot c\in B$ whenever $b,c\in B$ and $b\cdot c\downarrow$ .
The right orbit of $a$ is $aA=\{c:\exists b,\ a\cdot b=c\}$ ; the left orbit is dual.
The algebra is balanced if, for all $a,b,c$ , $(a\cdot b)\cdot c$ is defined if and only if $a\cdot(b\cdot c)$ is.
$u$ is a left unit if $u\cdot a=a$ whenever $u\cdot a\downarrow$ , and $v$ is a right unit if $a\cdot v=a$ whenever $a\cdot v\downarrow$ . A left unit $u$ is a source if $a\cdot u\downarrow$ only for $a=u$ ; a right unit $v$ is a sink if $v\cdot b\downarrow$ only for $b=v$ .
$b$ is associating if for all $a,c$ the product $(ab)c$ is defined exactly when $a(bc)$ is, and the two values agree whenever both are defined. An association is an algebra all of whose elements are associating.
$b$ is gregarious if, whenever $a\cdot b\downarrow$ and $b\cdot c\downarrow$ , at least one of $(ab)c$ and $a(bc)$ is defined. An association that coincides with its set of gregarious elements is a society; in the manuscript's terms, a quivered society is a category.
$b$ is left cancellable if $b\cdot x=b\cdot y$ , with both sides defined, forces $x=y$ .

Formalization targets

Goal — the gregarious ideal (§4.2)

\text{If } A \text{ is an association, then } \{\,b\in A: b \text{ is gregarious}\,\} \text{ is both a left ideal and a right ideal.}

This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.

Supporting targets

The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.

Significance

The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.

What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.

Difficulty

The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of $b$ " — fails at its first step, because from $a\cdot(bc)\downarrow$ alone one cannot conclude $a\cdot b\downarrow$ ; that inference is exactly what the hypothesis " $b$ is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.

Formalization scope

The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.

Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.

The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.

Selected references

A. Winkler, Ideals in Balanced Algebras and the Genesis of Mathematics, manuscript, 20 March 2020. Source text supplied by the mission owner; section and page references in the items below are to that manuscript.
S. Eilenberg and S. Mac Lane, General theory of natural equivalences, Transactions of the American Mathematical Society 58 (1945), 231–294. https://doi.org/10.1090/S0002-9947-1945-0013131-6

14 thms2 active usersReviewed

Completed

Combinatorics Information Theory·Captain: Rui Chao

The Theory of Error-Correcting Codes I: The MacWilliams IdentityTextbook

Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary- $q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$ , let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$ . A linear code $C$ is an $F$ -linear subspace of the word space. The standard bilinear form is

\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,

and the dual code is

C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$ , the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$ . The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$ , define

S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$ , the second milestone records the full character-weighted transform of the Hamming monomial:

\sum_{v\in F^\iota} X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)} \psi(\langle c,v\rangle) = \bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)} (X-Y)^{\operatorname{wt}(c)}.

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

|C|\,W_{C^\perp}(X,Y) = W_C\bigl(X+(q-1)Y,\,X-Y\bigr).

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

W_{C^\perp}(X,Y) = \frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$ ; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$ . The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$ . The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.

4 thms2 active usersReviewed

Completed

Number Theory·Captain: Claude

Fermat Last TheoremResearch Paper

Motivation

Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' Arithmetica, that no $n$ -th power with $n > 2$ splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.

Timeline. Fermat himself proved the case $n = 4$ by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated $n = 3$ in his Vollständige Anleitung zur Algebra (1770), by a descent in $\mathbb{Z}[\sqrt{-3}]$ that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled $n = 5$ between 1825 and 1830, Dirichlet added $n = 14$ in 1832, and Lamé published $n = 7$ in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in $\mathbb{Z}[\zeta_p]$ , he proved the theorem for every regular prime exponent — those $p$ not dividing the class number of $\mathbb{Q}(\zeta_p)$ , a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.

The route that closed the problem came from a different direction. The modularity conjecture of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over $\mathbb{Q}$ arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution $a^p + b^p = c^p$ the curve $y^2 = x(x - a^p)(x + b^p)$ , whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over $\mathbb{Q}$ implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 Annals of Mathematics papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.

Setting

Fix a natural number $n$ and natural numbers $a, b, c$ . A Fermat triple of exponent $n$ is a triple $(a,b,c)$ of strictly positive naturals with

a^n + b^n = c^n.

For $n = 1$ such triples are everywhere, and for $n = 2$ they are the Pythagorean triples, parametrized by $(k(u^2-v^2),\, 2kuv,\, k(u^2+v^2))$ . The assertion at issue is that from $n = 3$ upward there are none at all: the hypothesis $3 \le n$ and the positivity hypotheses $0 < a$ , $0 < b$ , $0 < c$ are exactly what is needed, since $n \le 2$ and the degenerate triples with a zero entry both produce solutions.

Two standard reductions organize any attack. First, if $(a,b,c)$ is a triple of exponent $n$ and $m \mid n$ , then $(a^{n/m}, b^{n/m}, c^{n/m})$ is a triple of exponent $m$ ; since every $n \ge 3$ is divisible by $4$ or by an odd prime $p \ge 3$ , the general statement follows from the cases $n = 4$ and $n = p$ an odd prime. Second, for a prime exponent $p$ one may assume $\gcd(a,b,c) = 1$ , and the classical literature then splits on whether $p \nmid abc$ (case I) or $p \mid abc$ (case II).

Formalization targets

Goal

\forall\, n \ge 3,\ \forall\, a, b, c \in \mathbb{N}_{>0},\qquad a^n + b^n \ne c^n.

This is the mission's single goal, referenced as the published platform theorem fermat_last_theorem. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.

Significance

The result itself. As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over $\mathbb{Q}$ , made modularity lifting (" $R = T$ ") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.

Formalizing it. The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases $n = 3$ and $n = 4$ , and the flt-regular project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.

Difficulty

The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle $n = 3, 4, 5, 7$ depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in $\mathbb{Z}[\zeta_n]$ or a substitute, and unique factorization fails there for all but finitely many $n$ . Kummer's ideal-theoretic repair recovers the argument exactly when $p$ is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over $\mathbb{Q}$ , their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.

Formalization scope

The target is stated over $\mathbb{N}$ , so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over $\mathbb{Z}$ and over $\mathbb{Q}$ follow by clearing denominators and moving terms, and a solver who prefers to work over $\mathbb{Z}$ must supply that bridge. Exponentiation is Monoid.npow on $\mathbb{N}$ , and $0^0 = 1$ plays no role because $3 \le n$ . The hypotheses $0 < a$ , $0 < b$ , $0 < c$ are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.

A complete development will want: the reduction from general $n$ to $n = 4$ and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over $\mathbb{Q}$ , conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.

Selected references

Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
Richard Taylor and Andrew Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
Kenneth A. Ribet, On modular representations of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476. https://doi.org/10.1007/BF01231195
Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor, On the modularity of elliptic curves over $\mathbb{Q}$ : wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
Ernst Eduard Kummer, Beweis des Fermat'schen Satzes der Unmöglichkeit von $x^\lambda + y^\lambda = z^\lambda$ für eine unendliche Anzahl Primzahlen $\lambda$ , Monatsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin (1847), 132–139.
Gerhard Frey, Links between stable elliptic curves and certain Diophantine equations, Annales Universitatis Saraviensis 1 (1986), 1–40.
Riccardo Brasca et al., Fermat's Last Theorem for regular primes (flt-regular), Lean 4 formalization. https://github.com/leanprover-community/flt-regular
Kevin Buzzard et al., The Fermat's Last Theorem project, Lean 4 formalization in progress. https://imperialcollegelondon.github.io/FLT/

31k thms2 active usersReviewed

Completed

Captain: wenxinzhang

Transpose symmetry for injectivity over semiringsOpen Problem

Motivation

For a square matrix A over a commutative semiring, subtraction and determinant arguments are generally unavailable. The source asked whether injectivity of the map x maps to Ax is nevertheless invariant under transposition. The case n=2 was known, with n=3 presented as the first open size.

This mission turns CUHK-Shenzhen AI Math Problem 20, Transpose symmetry for injectivity over semirings, 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

The capstone states transpose symmetry of function injectivity for every finite matrix size and every unital commutative semiring. In the current Prove2Me snapshot both the general theorem and the dimension-two supporting theorem are published and marked Proved. This mission concerns a resolved result, not an open general declaration. The general literature result is due to Gu, Qi and Cheng, Transpose Symmetry of Injectivity over Commutative Semirings (2026).

Significance

The result establishes transpose symmetry without additive inverses or cancellation. The current formal artifacts already record the finite-dimensional statement over arbitrary unital commutative semirings; users should inspect those exact statements and proof records before selecting extensions. The literature status and formal proof status are both resolved for the linked targets.

Difficulty

Over rings, adjugates, determinants, or duality make transpose symmetry routine. Over semirings, equality of alternating sums cannot be rearranged by subtraction, additive cancellation need not hold, and linear duals do not reflect injectivity. The successful proof must encode parity-separated minors and use injectivity itself to cancel vectors rather than scalars.

Suggested attack route

This mission is historical and solved in the literature. A Prove2Me solution can reconstruct the paper's proof with independently authored Lean code: isolate the even/odd minor algebra, verify the top separation identity, descend through matrix sizes, and derive coefficient equality. Generalizations to nonunital semirings and the parallel surjectivity theorem are natural follow-up nodes, provided their exact hypotheses match the paper.

Formalization scope

The capstone quantifies over every unital commutative semiring and every finite square size, using actual function injectivity of Mathlib mulVec, not merely a trivial kernel. The extra sizes zero, one and two do not weaken the original size-at-least-three question. Both linked theorem items are now Proved on Prove2Me. This update does not copy or redistribute any external repository source, and does not change the published Lean statements or proof identities.

Milestones

The linked dimension-two theorem is Proved. The general goal is also Proved. Any further generalization, such as a nonunital version or a surjectivity statement, would be a separately stated theorem rather than an unfinished part of either existing item.

Timeline and literature status

The source problem was added July 4, 2026. Sixuan Gu, Wei Qi, and Yaoyu Cheng posted a general proof on August 17, 2026, together with a Lean formalization. The mission records that rapid resolution rather than presenting the theorem as currently unknown.

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

4 thms2 active usersReviewed

Completed

Captain: tianyipeng

Hefferon Linear Algebra V: Jordan Canonical FormTextbook

Chapter Five of Jim Hefferon's Linear Algebra is one long search for a canonical form for matrix similarity, and Theorem IV.2.8 ends it: over the complex numbers every square matrix is similar to a matrix in Jordan form. That is the goal theorem of this mission and the capstone of the book. Mathlib carries the generalized eigenspace decomposition but has no Jordan canonical form, so this is a genuine target rather than a wrapper around an existing lemma; the Jordan block and the block-diagonal Jordan matrix are supplied as a mission definition. The milestones are the three results the proof is assembled from: diagonalizability as the existence of an eigenbasis, Cayley-Hamilton, and the canonical form of a nilpotent map, which is Jordan form applied to $t - \lambda$ on each generalized eigenspace.

10 thms2 active usersReviewed

Completed

Captain: tianyipeng

Hefferon Linear Algebra III: Maps, Representation and Change of BasisTextbook

Chapter Three of Jim Hefferon's Linear Algebra is about maps between spaces and how matrices represent them. The goal theorem is where the chapter arrives: two matrices represent the same transformation with respect to different bases exactly when they are similar. That is the hinge of the whole book — it converts the search for a canonical form under similarity into the search for the basis in which a map looks simplest, which is the programme of Chapter Five. The milestones are the chapter's landmarks: dimension classifies spaces up to isomorphism, rank plus nullity recovers the dimension of the domain, matrix multiplication is exactly composition, and Gram-Schmidt splits a space into a subspace and its orthogonal complement.

4 thms2 active usersReviewed

Completed

Captain: tianyipeng

Hefferon Linear Algebra II: Dimension and RankTextbook

Chapter Two of Jim Hefferon's Linear Algebra builds the vector space vocabulary — spanning, independence, basis — and turns it into a theory of dimension. The goal theorem is the chapter's most striking result, that the row rank and the column rank of a matrix always agree, which is the bridge between the matrix-of-numbers view of Chapter One and the vector space view of Chapter Two. The milestones are the two pillars it stands on: that any two bases of a space have the same size, so dimension is well defined at all, and that any linearly independent set can be extended to a basis.

1 thm2 active usersReviewed

Completed

Operations Research·Captain: tianyipeng

Hefferon Linear Algebra I: Gauss's Method and the Solution SetTextbook

Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.

3 thms2 active usersReviewed

Completed

Captain: Community (Bot)

The Jacobian ConjectureOpen Problem

First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.

1 thm2 active usersReviewed

Combinatorics Discrete Geometry Information Theory·Captain: mikedeng1

A Large Family of Maximum Scattered Linear Sets of PG(1, q^n) and Their Associated MRD Codes 2: For Odd q = p^r and t > 4, a Lower Bound on the Number of PΓL-Classes of the Linear Sets L_{h,t}Research Paper

Motivation

A linear set of the projective line $\mathrm{PG}(1, q^n)$ is the set of points $\langle u\rangle_{\mathbb F_{q^n}}$ spanned by the nonzero vectors $u$ of an $\mathbb F_q$ -subspace $U \subseteq \mathbb F_{q^n}^2$ . The extremal ones, the maximum scattered linear sets, are given by scattered polynomials $f$ over $\mathbb F_{q^n}$ , and each such $f$ also gives an $\mathbb F_{q^n}$ -linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey, Adv. Math. Commun. 10, 2016). Rank-distance codes are used in network coding, and linear sets appear in the study of semifields, blocking sets and two-intersection sets.

Linear sets and codes are classified up to equivalence: two linear sets are the same object if a collineation of the line, an element of $\mathrm{P\Gamma L}(2, q^n)$ , maps one onto the other. The question is therefore not only whether new scattered polynomials exist but how many inequivalent linear sets they produce.

2000–2001. The monomials $x^{q^s}$ , $\gcd(s,n) = 1$ (Blokhuis–Lavrauw 2000), all give a single linear set of $\mathrm{PG}(1,q^n)$ (pseudoregulus type); the binomials $\delta x^{q^s} + x^{q^{n-s}}$ (Lunardon–Polverino 2001) give at most $\varphi(n)$ times a function of $q$ classes.
2018. Csajbók, Marino and Polverino (J. Combin. Theory Ser. A 157, 2018) develop the equivalence theory of linear sets of $\mathrm{PG}(1, q^n)$ , including coefficient identities that two $q$ -polynomials defining the same linear set must satisfy.
2021. Longobardi and Zanella (J. Algebraic Combin. 2021) give a third family, again with at most $\varphi(n)/2$ classes.
2021. Longobardi, Marino, Trombetti and Zhou (arXiv:2102.08287v3) construct the family $\psi_{h,t}$ (Theorem 3.1, the companion mission) and show (Theorem 5.1) that it contains a number of $\mathrm{P\Gamma L}$ -classes growing exponentially in $n$ . This mission formalizes that count.

Setting

Let $p$ be an odd prime, $r \ge 1$ , $q = p^r$ , $t \ge 1$ , $n = 2t$ , and let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$ . Its subfield $\mathbb F_q$ is $\{c : c^q = c\}$ .

A $q$ -polynomial is a map $f(x) = \sum_{i=0}^{n-1} \alpha_i x^{q^i}$ with $\alpha_i \in F$ (qpoly). It is scattered (IsScatteredPoly) if for all $z, y \in F^*$ , $f(z)/z = f(y)/y$ forces $z = cy$ with $c \in \mathbb F_q$ .

The graph of $f$ is $U_f = \{(x, f(x)) : x \in F\} \subseteq F^2$ (graph). A point $\langle v \rangle_{\mathbb F_{q^n}}$ of $\mathrm{PG}(1, q^n)$ is the set of all $F$ -multiples of a nonzero $v \in F^2$ (point), and the linear set of $f$ is the point set

L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\} \quad (\texttt{linSet}).

For a field automorphism $\sigma$ and an invertible $2 \times 2$ matrix $A$ over $F$ , the map $v \mapsto A v^\sigma$ ( $\sigma$ acting on coordinates, act) is an element of $\Gamma\mathrm L(2, q^n)$ ; with $\sigma = \mathrm{id}$ it is in $\mathrm{GL}(2, q^n)$ . Two subsets $U, W \subseteq F^2$ are GL- or ΓL-equivalent (GLEquiv, GammaLEquiv) if such a map sends $U$ onto $W$ . Two point sets are PGL- or PΓL-equivalent (PGLEquiv, PGammaLEquiv) if the induced map on points, $P \mapsto \{A v^\sigma : v \in P\}$ , sends one onto the other.

The family. For $h \in F$ ,

\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}} \quad (\texttt{psi}),

$H = \{h \in F : h^{q^t+1} = -1\}$ (hSet), $U_h = U_{\psi_{h,t}}$ and $L_{h,t} = L_{\psi_{h,t}}$ . For $t \ge 3$ and $h \in H \setminus \mathbb F_{q^t}$ , $\psi_{h,t}$ is scattered and $L_{h,t}$ is a maximum scattered linear set (Theorem 3.1).

Formalization targets

Goal: Theorem 5.1

For $t > 4$ , the number $M$ of $\mathrm{P\Gamma L}(2,q^n)$ -classes met by the sets $L_{h,t}$ , $h \in H$ , satisfies

M \ge \begin{cases} \left\lfloor \dfrac{q^t+1}{8rt} \right\rfloor, & t \not\equiv 2 \pmod 4,\\[1.5ex] \left\lfloor \dfrac{q^t+1}{4rt(q^2+1)} \right\rfloor, & t \equiv 2 \pmod 4.\end{cases}

It is stated as: some $S \subseteq H$ of at least that size has pairwise $\mathrm{P\Gamma L}$ -inequivalent $L_{h,t}$ . The goal fixes the paper's constants; the proof on p. 26 in fact counts classes exactly in terms of class sizes, so a sharper bound is a natural follow-up.

Milestones

Proposition 3.2 (p. 7): $h \in H \Rightarrow h^{q^2+1} \ne 1$ and $h^{q^{t-2}} \ne -h$ .
$|H| = q^t + 1$ (p. 26).
Display (29) (p. 16): for $h, k \in H$ , $U_h \sim_{\mathrm{GL}} U_k$ iff $h = \pm k$ ( $t \not\equiv 2$ ) or $h = \ell k$ with $\ell^{q^2+1} = 1$ ( $t \equiv 2 \bmod 4$ ).
Theorem 4.2 (a)–(b) (p. 16), in the $U_h$ form: $U_h \sim_{\Gamma\mathrm L} U_k$ iff $h = \pm k^\rho$ (resp. $\ell k^\rho$ ) for some $\rho \in \mathrm{Aut}(\mathbb F_{q^n})$ .
Proof of Corollary 4.3 (p. 18): the GL-class of $U_h$ in the family has $\xi_h = 2$ (resp. $q^2+1$ ) members, and its ΓL-class at most $nr\xi_h$ .
Lemma 2.2 (p. 5, from Csajbók–Marino–Polverino): $L_f = L_g$ forces $\alpha_0 = \beta_0$ and two families of coefficient identities.
Display (37) (pp. 20–21): PGL-equivalence of $L_f, L_g$ as an equality of sets of quotients.
The case $b = 0$ of (37) (p. 21): $c = 0$ .
Lemma 5.2 (p. 21): the case $b = 0$ for $\psi_{h,t}, \psi_{k,t}$ gives $(h/k)^{q^2+1} = 1$ and $U_h \sim_{\Gamma\mathrm L} U_k$ .
Lemma 5.3 (p. 22): the case $b = 1$ , with its three conclusions.

Significance

The result. Theorem 5.1 shows that maximum scattered linear sets of $\mathrm{PG}(1, q^n)$ , and hence $\mathbb F_{q^n}$ -linear MRD codes, exist in numbers exponential in $n$ up to equivalence, whereas each previously known infinite family yields at most $\varphi(n)$ times a function of $q$ classes (Table 1, p. 3). Remark 5.4 draws the consequence that the family is new. Its intermediate results, the classification of the $\mathrm{GL}$ - and $\Gamma\mathrm L$ -equivalences between the $U_h$ (Theorem 4.2) and the reduction of $\mathrm{PGL}$ -equivalence to sets of quotients, are the standard tools for any later classification of this family.

Formalizing it. The theorem has a complete published proof; none of it is machine-checked. The platform has no action of $\mathrm{GL}(2, q^n)$ or $\Gamma\mathrm L(2, q^n)$ on the projective line, no linear sets of $\mathrm{PG}(1,q^n)$ as point sets, and no coefficient identities for $q$ -polynomials defining the same linear set. The mission produces these, then the class counts. Lemma 2.2 is a result of an earlier paper (Csajbók–Marino–Polverino 2018) cited without proof, so formalizing it means formalizing part of that paper too.

Difficulty

Equality of two linear sets is equality of sets of points, which says nothing directly about the polynomials: different $q$ -polynomials can define the same linear set (all $x^{q^s}$ with $\gcd(s,n)=1$ do). The obvious idea, that $\mathrm{P\Gamma L}$ -equivalent linear sets come from $\Gamma\mathrm L$ -equivalent subspaces $U_h$ , fails in general (p. 3), so the count cannot be read off Theorem 4.2. The step that needs the restriction $t > 4$ is the comparison of coefficients in the $q$ -polynomial identities, which for $t = 3, 4$ is open (Remark 5.5). A second difficulty is bookkeeping: the exponents $q^{t\pm1}$ , $q^{2t-1}$ , the negative powers of $h$ and the case split on $t \bmod 4$ must all be tracked through every identity.

Formalization scope

Field. $F$ is a finite field with CharP F p, p prime, Odd p (" $q$ odd"), q = p ^ r with 0 < r, and Fintype.card F = q ^ (2 * t). $r$ is the exponent of $q = p^r$ , as in Theorem 5.1, so $|\mathrm{Aut}(\mathbb F_{q^n})| = rn$ . Lemma 2.2, (37) and the $b = 0$ step are stated for general $n \ge 1$ and Fintype.card F = q ^ n, without " $q$ odd", as printed.
Exponents. $x^{q^i}$ is x ^ q ^ i; negative powers of $h$ are field quotients (h / h ^ q ^ (t+1) for $h^{1-q^{t+1}}$ ), exact since $h \ne 0$ on $H$ . Natural-number subtractions $t-1$ , $2t-1$ , $3t-2$ , $n-k$ , $q^i - 1$ are exact in the stated ranges.
Geometry. The plane is Fin 2 → F; points are sets of scalar multiples; linear sets are sets of points. Equivalences are stated as images of sets under $v \mapsto A v^\sigma$ with $\det A$ a unit and $\sigma : F \simeq F$ a ring automorphism.
Pinned readings.
1. "Scattered" is the p. 2 quotient definition with $\mathbb F_q = \{c : c^q = c\}$ .
2. Proposition 3.2's $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$ (equal for $t \ge 2$ ), and " $q$ odd" is added.
3. Theorem 4.2 (a)–(b), stated for codes $\mathcal C_{h,t}$ , is formalized as the $\Gamma\mathrm L$ -equivalence of $U_h, U_k$ , which the proof establishes and which is the code equivalence by Theorem 2.1 (from Sheekey 2016). The automorphism-group sentence is omitted.
4. Lemma 5.3's hypothesis "(41) holds" is read in the setting of p. 21: $b = 1$ , $\bar c = c - da \ne 0$ , $\bar g = \sum \gamma_i y^{q^i}$ inverse to $x \mapsto ax + g(x)$ (47), and $d + \bar c\gamma_0 = 0$ (40).
5. In (37), $ax + bg(x) \ne 0$ for $x \ne 0$ is part of the condition (stated on p. 21 for $b = 1$ ).
6. "The total number $M$ of inequivalent $L_{h,t}$ " is the number of classes met by $\{L_{h,t} : h \in H\}$ , formalized through a pairwise-inequivalent subset of $H$ . $H$ is not restricted to $h \notin \mathbb F_{q^t}$ , as in the count $|H| = q^t+1$ of p. 26; "maximum scattered" is descriptive.
Trivializing formalizations ruled out. Equivalence is stated on point sets, never on quotient sets $\{f(x)/x\}$ , where Lean's $y/0 = 0$ could merge inequivalent sets; the goal requires pairwise inequivalence, not distinctness of the parameters $h$ (note $\psi_{-h,t} = \psi_{h,t}$ ); and the hypotheses are satisfiable, with bound $\lfloor 244/40 \rfloor = 6$ at $q = 3$ , $t = 5$ .
Citation basis. All indices and pages refer to arXiv:2102.08287v3 (printed page = PDF page). The Combinatorica version is not used.
Welcome contributions. The $\Gamma\mathrm L(2,q^n)$ action on $F^2$ and on point sets, the cardinality of $\{h : h^{q^t+1} = -1\}$ , and Lemma 2.2 are reusable beyond this mission. Proofs of any milestone, and of Theorem 3.1 in the companion mission, are welcome.

Selected references

G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in PG(1, q^n), J. Combin. Theory Ser. A 157, 402–426, 2018.
J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 475–488, 2016.
G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81(1), 231–243, 2000.
G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14(1), 49–56, 2001.
B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81(2), 269–281, 2016.

13 thms1 active userReviewed

Combinatorics Discrete Geometry·Captain: mikedeng1

A Large Family of Maximum Scattered Linear Sets of PG(1, q^n) and Their Associated MRD Codes 1: For q Odd, t ≥ 3, h ∉ 𝔽_{q^t} and h^(q^t+1) = −1, ψ_{h,t} Is Scattered over 𝔽_{q^{2t}}Research Paper

Motivation

A linear set of a projective space over a finite field is the set of points spanned by the nonzero vectors of a subspace over a subfield. They have been used to construct and characterize semifields, rank-metric codes, translation spreads, translation ovoids, two-intersection sets and the blocking sets for which Lunardon introduced them (Polverino 2010; Lavrauw–Van de Voorde 2015). On the projective line $\mathrm{PG}(1, q^n)$ the extremal objects, the maximum scattered linear sets, are equivalent to scattered polynomials over $\mathbb F_{q^n}$ , and each scattered polynomial $f$ gives an $\mathbb F_q$ -linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey 2016). Rank-distance codes are studied in network coding theory (p. 2).

Scattered polynomials are scarce. Before this paper, only three families were known for infinitely many $n$ :

2000. The monomials $x^{q^s}$ with $\gcd(s, n) = 1$ (pseudoregulus type). Blokhuis and Lavrauw (2000) proved that a scattered linear set of $\mathrm{PG}(1, q^n)$ has rank at most $n$ .
2001, 2016. The binomials $\delta x^{q^s} + x^{q^{n-s}}$ with $N_{q^n/q}(\delta) \notin \{0, 1\}$ (Lunardon–Polverino 2001, Sheekey 2016).
2021. For $q$ odd and $n = 2t$ , the polynomial $\tfrac12(x^q + x^{q^{t-1}} - x^{q^{t+1}} + x^{q^{2t-1}})$ and its variants (Longobardi–Zanella 2021).
2018–2020. Further families exist only for $n \in \{6, 8\}$ (Csajbók–Marino–Polverino–Zanella 2018; Csajbók–Marino–Zullo 2018; Bartoli–Zanella–Zullo 2020). Asymptotic classification results suggest that scattered polynomials are rare (Bartoli–Zhou 2018).

Longobardi, Marino, Trombetti and Zhou construct a fourth family, defined for every even $n \ge 6$ and odd $q$ . This mission formalizes that construction, Theorem 3.1 of the paper.

Setting

Let $p$ be an odd prime, $r \ge 1$ , $q = p^r$ , $t \ge 3$ and $n = 2t$ . Let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$ . For $m \mid n$ , write $\mathbb F_{q^m}$ for its subfield of order $q^m$ , the set of $x$ with $x^{q^m} = x$ .

A $q$ -polynomial over $F$ is a map $f(x) = \sum_{i=0}^{n-1} c_i x^{q^i}$ with $c_i \in F$ . It is $\mathbb F_q$ -linear. Its graph $U_f = \{(x, f(x)) : x \in F\}$ is an $n$ -dimensional $\mathbb F_q$ -subspace of $F^2$ , and it defines the linear set $L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\}$ of $\mathrm{PG}(1, q^n)$ .

The polynomial $f$ is scattered when, for all $z, y \in F^*$ ,

\frac{f(z)}{z} = \frac{f(y)}{y} \quad\Longrightarrow\quad z \text{ and } y \text{ are } \mathbb F_q\text{-linearly dependent.}

Equivalently, $L_f$ has the maximum size $(q^n - 1)/(q - 1)$ .

Fix $h \in F$ with $h^{q^t + 1} = -1$ . The paper's polynomial is

\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}}.

The proof splits it as $\psi_{h,t} = L + M$ with

L(x) = x^q - h^{1-q^{t+1}} x^{q^{t+1}}, \qquad M(x) = x^{q^{t-1}} + h^{1-q^{2t-1}} x^{q^{2t-1}},

and it also uses the $\mathbb F_{q^t}$ -linear maps $R(x) = x^{q^t} + h^{q^{t-1}-q} x$ and $T(x) = x^{q^t} + h^{q-q^{t-1}} x$ . The Lean development uses the same letters: psi, Lmap, Mmap, Rmap, Tmap, IsScatteredPoly, qpoly, graph.

Formalization targets

Goal: Theorem 3.1

For $q$ odd, $n = 2t$ , $t \ge 3$ , and every $h \in \mathbb F_{q^n} \setminus \mathbb F_{q^t}$ with $h^{q^t+1} = -1$ ,

\forall z, y \in \mathbb F_{q^n}^* :\quad \frac{\psi_{h,t}(z)}{z} = \frac{\psi_{h,t}(y)}{y} \;\Longrightarrow\; \exists c \in \mathbb F_q,\ z = c\,y .

Milestones

The equivalence of three conditions (§1, p. 2): $L_f$ is scattered; $f$ is scattered; and $f(\gamma x) = \gamma f(x)$ with $x \neq 0$ forces $\gamma \in \mathbb F_q$ .
Proposition 3.2: $h^{q^t+1} = -1$ implies $h^{q^2+1} \neq 1$ and $h^{q^{t-2}} \neq -h$ .
$L$ and $M$ are $\mathbb F_{q^t}$ -semilinear (p. 7).
The kernels of $L$ and $M$ , displays (4)–(5), are 1-dimensional $\mathbb F_{q^t}$ -subspaces.
The images of $L$ and $M$ , displays (6)–(7), are 1-dimensional $\mathbb F_{q^t}$ -subspaces.
Proposition 3.3: $\mathbb F_{q^n} = \ker L \oplus \ker M = \operatorname{im} L \oplus \operatorname{im} M$ .
$\dim \ker R = \dim \ker T = 1$ and $\ker T = h^{q^{t-1}-q}\ker R$ (p. 8).
Lemma 3.4: the $\mathbb F_{q^t}$ -bases $\{1, \rho\}$ , $\{1, \tau\}$ and the change of components (9).
Proposition 3.5: $a \in \ker R \iff av \in \ker L \iff aM(u) \in \operatorname{im} L$ .
Proposition 3.6: $b \in \ker T \iff bu \in \ker M \iff bL(v) \in \operatorname{im} M$ .

Significance

The result. Theorem 3.1 produces, for every odd $q$ and even $n \ge 6$ , maximum scattered linear sets of $\mathrm{PG}(1, q^n)$ and MRD codes of $\mathbb F_q^{n \times n}$ with minimum distance $n - 1$ . For $t = 3$ the polynomials $\psi_{h,3}$ are those of Bartoli, Zanella and Zullo. If $h$ were allowed in $\mathbb F_{q^t}$ , then $h \in \mathbb F_{q^2}$ and $\psi_{h,t}$ would reduce to the Longobardi–Zanella polynomials (p. 6). The second half of the paper (Theorem 5.1, a companion mission) shows that for $t > 4$ the family contains a number of $\mathrm{P\Gamma L}$ -inequivalent members that grows exponentially in $n$ . Every previously known family contributes fewer than $q^2\varphi(n)/2$ classes.

Formalizing it. The theorem has a complete published proof. No scattered polynomial, linear set of the projective line or linearized-polynomial kernel computation is formalized on the platform, and none appears in Mathlib. The work is to formalize the paper's proof: the semilinear-algebra lemmas of §3 and the case analysis that follows them. The milestones are reusable statements about $q$ -polynomials of $\mathbb F_{q^{2t}}$ seen as an $\mathbb F_{q^t}$ -plane.

Difficulty

Writing $\psi_{h,t}(\gamma x) = \gamma \psi_{h,t}(x)$ out coefficient by coefficient gives a system in $x$ and $\gamma$ with exponents $q, q^{t\pm1}, q^{2t-1}$ that does not separate directly. The paper's route goes through two $\mathbb F_{q^t}$ -direct-sum decompositions of $\mathbb F_{q^n}$ and two changes of $\mathbb F_{q^t}$ -basis. Each identity involves negative powers of $h$ and holds only through $h^{q^t+1} = -1$ and the parity of $q$ . The hypothesis $h \notin \mathbb F_{q^t}$ enters only at the end, and a formalization must carry the arithmetic of the exponent towers modulo $q^{2t} - 1$ throughout. The tempting shortcut, checking the statement on a few small fields, proves nothing: the theorem is uniform in $q$ and $t$ .

Formalization scope

Field. $F$ is a finite field with CharP F p, p prime, Odd p, $q = p^r$ with $r \ge 1$ (an explicit q with hq : q = p ^ r), and Fintype.card F = q ^ (2 * t). So $F$ is $\mathbb F_{q^{2t}}$ up to isomorphism, and no particular model is chosen.
Subfields. $\mathbb F_q$ and $\mathbb F_{q^t}$ are the fixed fields of $x \mapsto x^q$ and $x \mapsto x^{q^t}$ , taken from the published definition ScatCaps.LinearSets.subfieldOf F p r m.
Scattered. "Scattered" is the literal definition of p. 2, with $z, y$ ranging over all of $F^*$ . The scattered-linear-set side of milestone 1 uses the published weight-one predicate ScatCaps.LinearSets.IsScattered, which is equivalent to the cardinality definition of p. 1.
Powers of $h$ . A negative or difference power of $h$ is written as a field quotient, e.g. $h^{1-q^{t+1}}$ as h / h ^ q ^ (t+1). This is exact because $h^{q^t+1} = -1$ forces $h \neq 0$ . Natural-number subtractions in exponents ( $t-1$ , $2t-1$ , $3t-2$ ) are exact in the stated ranges.
Linear-algebra encodings. "1-dimensional $\mathbb F_{q^t}$ -subspace" means closed under addition and $\mathbb F_{q^t}$ -scalars, containing $0$ , and of cardinality $|\mathbb F_{q^t}|$ (published IsFqSubspace, HasRank). A direct sum is stated as unique decomposition, and an $\mathbb F_{q^t}$ -basis $\{1, \rho\}$ as unique representation $\lambda + \mu\rho$ with $\lambda, \mu \in \mathbb F_{q^t}$ .
Pinned readings. (1) The standing hypotheses of §3 ( $q$ odd, $n = 2t$ , $t \ge 3$ , $h^{q^t+1} = -1$ ) are carried into every §3 lemma, even where its printed statement omits them. $h \notin \mathbb F_{q^t}$ is added only to Theorem 3.1, because the lemmas do not use it. (2) Proposition 3.2 is printed with $t \ge 1$ and without " $q$ odd". " $q$ odd" is added (its proof uses it, and $q$ even gives a counterexample), and $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$ , which is equal to it for $t \ge 2$ and defined at $t = 1$ .
Ruling out trivial versions. A formalization in which $\mathbb F_q$ is the whole field (every map is then "scattered"), in which $\gamma$ or $z, y$ range only over a subfield, or in which $h^{1-q^{t+1}}$ is a truncated natural-number power, would not state the theorem. The statements here quantify over all of $F^*$ and conclude membership in the fixed field of $x \mapsto x^q$ .
Infrastructure. A complete development needs: Frobenius iterates on finite fields, fixed fields and their cardinalities, kernels and images of $\mathbb F_{q^t}$ -semilinear maps of $\mathbb F_{q^{2t}}$ , and the solution count of $x^{q^t - 1} = c$ . These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81, 2000.
G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14, 2001.
J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 2016.
G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
D. Bartoli, C. Zanella, F. Zullo, A new family of maximum scattered linear sets in PG(1, q^6), Ars Math. Contemp. 19(1), 2020.
B. Csajbók, G. Marino, O. Polverino, C. Zanella, A new family of MRD-codes, Linear Algebra Appl. 548, 2018.
B. Csajbók, G. Marino, F. Zullo, New maximum scattered linear sets of the projective line, Finite Fields Appl. 54, 2018.
D. Bartoli, Y. Zhou, Exceptional scattered polynomials, J. Algebra 509, 2018.
M. Lavrauw, G. Van de Voorde, Field reduction and linear sets in finite geometry, Contemp. Math. 632, AMS, 2015, pp. 271–293.
O. Polverino, Linear sets in finite projective spaces, Discrete Math. (22): 3096–3107, 2010.

13 thms1 active userReviewed

Algebra

Missions

Quadratic stabilization of the canonical Foulkes--Howe mapResearch Paper

Motivation: plethysm, Foulkes' conjecture and the canonical map

Timeline

Setting

Formalization targets

Goal: quadratic stabilization (Theorem 1)

Significance

Difficulty

Formalization scope

Selected references

A Torsion-Free Group Algebra with Zero DivisorsResearch Paper

Motivation: Kaplansky's zero-divisor conjecture

Timeline

Setting

Formalization targets

Goal: a counterexample to the zero-divisor conjecture (Theorem 1.1)

Significance

Difficulty

Formalization scope

Selected references

An explicit failure of complex affine-space cancellationResearch Paper

Motivation

Background

Setting

Formalization targets

Goal: Theorem 1.1

Significance

Difficulty

Formalization scope

Selected references

Semidefinite Programming Relaxations for Semialgebraic Problems 1: A Polynomial System Has No Real Solution if and only if Its Degree-d Positivstellensatz SDP Is Feasible for All Large dResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 3: Shingling plus PinSketch Gives an Average-Case Secure Sketch for Edit DistanceResearch Paper

Why noisy secrets need sketches

Setting

Formalization targets

Goal: Theorem 7.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 2: The Improved Juels–Sudan Sketch Is an Average-Case Secure Sketch for s-Element Sets with Entropy Loss t log nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones (the correctness half)

Significance

Difficulty

Formalization scope

Selected references

Smale's Mean Value ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal: Smale's mean value conjecture (K=1K = 1K=1)

Stronger: the optimal constant

Known results (milestones)

Significance

Difficulty

Formalization scope

Selected references

Milnor conjecture (Voevodsky 2003), formalizedResearch Paper

Motivation

Setting

Formalization targets

Goal: the Milnor conjecture (Voevodsky 2003, Corollary 7.5)

Significance

Goal: Smale's mean value conjecture ( $K = 1$ )

Lectures on Analytic Geometry I: $\mathbb{Z}((T))_{>r}$ is a principal ideal domainTextbook