## Motivation: approximating entire continuous functions
An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. **Polynomial approximation** on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. [Lebl, Theorem 11.7.1](https://www.jirka.org/ra/html/sec_stoneweier.html).
The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s *Basic Analysis*, Volume II. [Source section](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Setting: function algebras and uniform error
A **metric space** is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is **compact** if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$, and write $C(X,K)$ for the continuous functions from $X$ to $K$. Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$, and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$.
A **non-unital function algebra** $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$. It **separates points** if, whenever $x\ne y$, some $g\in A$ satisfies $g(x)\ne g(y)$. It **vanishes nowhere** if, for each $x$, some $g\in A$ satisfies $g(x)\ne0$. The witness may depend on $x$; one everywhere nonzero function is not specified. A complex algebra is **self-adjoint** if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. [Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Uniform convergence** of $f_n$ to $f$ means
$$
\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X,
\qquad |f_n(x)-f(x)|<\varepsilon.
$$
Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$, the **closure** $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is **dense** means $\overline A=C(X,K)$. [Mathlib’s compact-domain convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/CompactConvergence.lean).
## Formalization targets
The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.
**Theorem 11.7.1.** For $K=\mathbb R$ and for $K=\mathbb C$, respectively,
$$
f\in C([a,b],K)\Longrightarrow
\exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad
p_n\longrightarrow f\ \text{uniformly on }[a,b].
$$
The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. [Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Corollary 11.7.4.** For $a\ge0$,
$$
\exists(p_n)\subseteq\mathbb R[t],\qquad
(\forall n,\ p_n(0)=0)\ \land\
p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].
$$
[Source corollary](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.6.** For compact metric $X$ and either scalar field,
$$
A\text{ a non-unital algebra in }C(X,K)
\Longrightarrow\overline A\text{ is such an algebra}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.11.** For an arbitrary set $X$, without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then
$$
\forall x\ne y\;\forall c,d\in K\;\exists f\in A,
\qquad f(x)=c\ \land\ f(y)=d.
$$
Both scalar fields belong to this single target. [Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.12.** For compact metric $X$,
$$
A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere}
\Longrightarrow\overline A=C(X,\mathbb R).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.16, complex Stone–Weierstrass.** For compact metric $X$,
$$
\begin{gathered}
A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\
A\text{ separates points and vanishes nowhere}
\end{gathered}
\Longrightarrow\overline A=C(X,\mathbb C).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Significance: density without an assumed unit
The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.
These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass library](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Difficulty: local distinctions do not give uniform control
Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.
Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. [Library theorem hypotheses](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Formalization scope
Namespace `LeblRA` uses `NonUnitalSubalgebra`, `ContinuousMap`, real and complex polynomials, `TendstoUniformly`, and topological `closure`. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise `star` operation on complex continuous maps.
The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$. Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.
Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. [Non-unital algebra structures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean), [topological closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.7. [Section text](https://www.jirka.org/ra/html/sec_stoneweier.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass and zero-preserving continuous maps](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean), [non-unital algebra closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
## Motivation: limits of families of functions
Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. [Examples 11.6.2–11.6.4](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-6).
The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. [Differential-equation application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-29), [integral-operator application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-30).
The four targets follow §11.6 of Jiří Lebl’s *Basic Analysis*, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. [Author’s book page](https://www.jirka.org/ra/).
## Setting: pointwise control and uniform control
A **metric space** is a set $X$ with a distance $d(x,y)$ that is nonnegative, symmetric, vanishes exactly when $x=y$, and satisfies the triangle inequality. It is **compact** when every cover by open sets has a finite subcover. Here $\mathbb C$ denotes the complex numbers, $|z|$ their absolute value, and $F_n:X\to\mathbb C$ the function at index $n\in\mathbb N$. Write $C(X,\mathbb C)$ for the continuous functions.
The sequence is **pointwise bounded** if each input has its own bound, and **uniformly bounded** if one bound works for every input and index:
$$
\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N,
\quad |F_n(x)|\le M_x,
$$
$$
\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X,
\quad |F_n(x)|\le M.
$$
It is **uniformly equicontinuous** when
$$
\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N,
\quad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.
$$
Thus $\delta$ cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. [Definition 11.6.1](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-4), [Definition 11.6.6](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-13).
A **subsequence** has the form $F_{\varphi(n)}$, where $\varphi:\mathbb N\to\mathbb N$ is strictly increasing. **Pointwise convergence** to $f$ means convergence to $f(x)$ separately for every $x$. **Uniform convergence** means that for each $\varepsilon>0$ there is one $N$ such that $|F_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x$. A subset $D\subseteq X$ is **dense** if its closure $\overline D$ is all of $X$.
## Formalization targets
The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.
**Proposition 11.6.5.** For an arbitrary countable set $X$, without any topology or continuity assumption,
$$
F_n\text{ pointwise bounded}
\Longrightarrow
\exists\varphi,f,\quad
\varphi\text{ strictly increasing}\quad\land\quad
\forall x\in X,\ F_{\varphi(n)}(x)\longrightarrow f(x).
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#prop_subsequenceoncountableX).
**Proposition 11.6.7.** For compact metric $X$,
$$
F_n\in C(X,\mathbb C),\quad F_n\longrightarrow f\text{ uniformly}
\Longrightarrow F_n\text{ uniformly equicontinuous}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-16).
**Proposition 11.6.8.** Every compact metric space satisfies
$$
\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-18).
**Theorem 11.6.9, Arzelà–Ascoli.** Suppose $X$ is compact metric, $F_n\in C(X,\mathbb C)$, and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is
$$
\left(\exists M\in\mathbb R\;\forall n,x,\ |F_n(x)|\le M\right)
\quad\land\quad
\left(\exists\varphi:\mathbb N\to\mathbb N\;\exists f\in C(X,\mathbb C),\quad
\varphi\text{ strictly increasing},\quad
F_{\varphi(n)}\longrightarrow f\text{ uniformly}\right).
$$
Both the global bound and the subsequence conclusion are required. The limit belongs to $C(X,\mathbb C)$, so its continuity is explicit. [Source theorem](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
## Significance: a compactness criterion with explicit hypotheses
The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. [Lebl, Theorem 11.6.9](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. [Mathlib Ascoli development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [countable dense subsets](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).
## Difficulty: preserving the quantifier order
Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every $F_n$ does not give a single $\delta$ valid for all $n$. Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence $x\mapsto x^n$ on $[0,1]$ already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. [Example 11.6.3](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-7).
The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.
## Formalization scope
The development uses namespace `LeblRA`, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by `StrictMono`; pointwise limits use `Tendsto` at `atTop`, uniform limits use `TendstoUniformly`, and density uses `Dense`. Finite and empty domains remain allowed.
The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.
Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. [Uniform-convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [sequence compactness](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Sequences.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.6. [Section text](https://www.jirka.org/ra/html/sec_arzelaascoli.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [General Ascoli theorems](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [uniform convergence](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [topological bases and separability](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).
Elementary Number Theory: Primes, Congruences, and Secrets I: Sums of Two SquaresTextbook
## From individual representations to an arithmetic criterion
Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's *Elementary Number Theory: Primes, Congruences, and Secrets*, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the [author-hosted January 2017 text](https://wstein.org/ent/ent.pdf), using its numbering rather than the numbering of earlier drafts.
## Integers, representations, and prime exponents
A **two-square representation** of an integer $n$ consists of integers $x,y$ satisfying $n=x^2+y^2$. Either coordinate may be zero or negative. A representation is **primitive** when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer $n$ and a prime $p$, the **prime exponent** $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$. The congruence $p\equiv3\pmod4$ means that division of $p$ by four leaves remainder three.
The approximation statement uses a real number $t$, a positive integer $N$, and a **reduced fraction** $a/b$, where $a$ is an integer, $b$ is a positive integer, and their greatest common divisor is one. These conventions agree with [Stein's section and its definition of primitive representations](https://wstein.org/ent/ent.pdf).
## Formalization targets
The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer $n$ with a prime divisor $p\equiv3\pmod4$:
$$\nexists x,y\in\mathbb Z:\quad n=x^2+y^2\quad\text{and}\quad\gcd(x,y)=1.$$
Equation (5.7.1) is the integer identity
$$(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.$$
Lemma 5.7.5 states that, for every real $t$ and positive integer $N$, some reduced fraction satisfies
$$0<b\le N,\qquad |t-a/b|\le\frac{1}{b(N+1)}.$$
The capstone, Theorem 5.7.1, is the complete equivalence
$$n=x^2+y^2\text{ for some }x,y\in\mathbb Z
\quad\Longleftrightarrow\quad
\forall\text{ primes }p\mid n,\quad p\equiv3\pmod4\Longrightarrow v_p(n)\text{ is even},$$
for every positive integer $n$. Both implications are required. These four statements are located on printed pages 117–120 of the [source PDF](https://wstein.org/ent/ent.pdf).
Exercise 5.11, on printed page 122, is an optional downstream target:
$$\forall n\in\mathbb Z,\ \exists k\in\{0,1,2,3\}:\quad
\nexists x,y\in\mathbb Z,\ n+k=x^2+y^2.$$
It describes gaps among represented integers and is not a prerequisite milestone for the capstone.
## What the criterion and its formalization provide
The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in [Stein's treatment](https://wstein.org/ent/ent.pdf).
The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the [sum-of-two-squares development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/NumberTheory/SumTwoSquares.lean) includes the arithmetic criterion and primitive obstruction, and the [Diophantine approximation development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean) supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.
## Why the complete statement matters
A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the [source statements](https://wstein.org/ent/ent.pdf).
## Formalization scope
The namespace is `SteinENT`. Inputs $n,p,N$ use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use `Nat.factorization`; primitivity uses `Int.gcd x y = 1`. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.
No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.
## Selected references
- William Stein, *Elementary Number Theory: Primes, Congruences, and Secrets*, Undergraduate Texts in Mathematics, Springer, 2008; [author-hosted January 2017 version](https://wstein.org/ent/ent.pdf), Section 5.7 and Exercise 5.11. [Author's book page](https://wstein.org/ent/).
- William Stein, [author's source text at commit c4984c7ddb22258674816f8c000b0d8eb485d694](https://github.com/williamstein/ent/blob/c4984c7ddb22258674816f8c000b0d8eb485d694/body.tex), corresponding section and exercises.
- The Mathlib Community, [Mathlib4 at commit 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e](https://github.com/leanprover-community/mathlib4/tree/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e), Lean 4 library, pinned formalization environment; number-theory modules linked above.
Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook
## Motivation
Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.
## Setting
A finite directed graph with arc set $\mathcal{A}$, real arc lengths $a_{ij}$, origin $s$ and destination $t \ne s$ (`BertsekasSPGraph`). Walks are nonempty node lists whose consecutive pairs are arcs (`BertsekasIsWalkFrom`), with length the sum of arc lengths (`BertsekasWalkLength`); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (`BertsekasShortestDistance`). The standing assumption of §2.3: **every cycle has nonnegative length** (negative arcs allowed).
The algorithm state (`BertsekasLCState`) carries labels $d_j \in \overline{\mathbb{R}}$, the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$, all other labels $\infty$, UPPER $= \infty$, OPEN $= \{s\}$. One iteration (`BertsekasLCStep`, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$, and put $j$ in OPEN if $j \ne t$, or update UPPER if $j = t$. The algorithm terminates when OPEN is empty.
## Target
$$\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},$$
for every execution, **under the nonnegative arc length assumption of §2.3** ($a_{ij} \ge 0$ for every arc) — `BertsekasDP.label_correcting_correctness_of_nonneg_arcs` (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (`label_correcting_terminates`) — and the workhorse invariant that every finite label is the length of an actual walk from $s$, which needs neither (`label_correcting_invariant`).
The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$, and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-*cycle* assumption of §2.1 and was disproved by the counterexample $s=0$, $t=2$, $a_{02}=1$, $a_{01}=2$, $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$. Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.
## Significance
Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.
## Difficulty
Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.
## Formalization scope
Finite node type with decidable equality; arcs as a `Finset` of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in `EReal`, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
- E. W. Dijkstra, A note on two problems in connexion with graphs, *Numer. Math.* 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
- R. Bellman, On a routing problem, *Quart. Appl. Math.* 16 (1958), 87–90. https://doi.org/10.1090/qam/102435
Strong Whitney embedding in dimension 2nResearch Paper
## Motivation: an intrinsic manifold in a fixed Euclidean space
A **smooth manifold** is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The **strong Whitney embedding theorem** supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by [LeanEval v1](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean), rather than a substitute formulation.
The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of $2n+1$. The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature ([source and attribution](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml)).
## Setting: topology, smoothness, and the differential
Let $n$ be a natural number satisfying $1\le n$. Let $M$ carry a topology and a smooth atlas modeled on $\mathbb R^n$, with the usual model having no boundary. The topology is **Hausdorff**: distinct points admit disjoint neighborhoods. It is **second countable**: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the [Lean statement](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
A **topological embedding** is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An **immersion** has an injective differential at every point. For a smooth map $e$, write $d e_x$ for the induced linear map on tangent spaces at $x$. These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.
## Formalization target: the single root theorem
For every $n\ge1$ and every $M$ with the structures and hypotheses just stated, establish
$$
\exists e:M\longrightarrow\mathbb R^{2n},\qquad
e\in C^\infty(M,\mathbb R^{2n})
\ \land\ e\text{ is a topological embedding}
\ \land\ \forall x\in M,\ d e_x\text{ is injective}.
$$
The codomain has dimension exactly $2n$. The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is `LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding`, with the binders and conclusion preserved from the [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
## Significance: the full theorem rather than an easier restriction
The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing $2n$ with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the [benchmark's explanation](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.
## Difficulty: the dimension bound and the noncompact scope
The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the $2n$ bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition ([benchmark discussion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
All positive dimensions remain in scope, including $n=1$ and $n=2$. Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.
## Formalization scope: unchanged Mathlib predicates
The source model is `EuclideanSpace ℝ (Fin n)`, and the target is `EuclideanSpace ℝ (Fin (2 * n))`. Smoothness is expressed by `ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e`; the other two conjuncts are `IsEmbedding e` and pointwise `Function.Injective` of `mfderiv`. The type $M$ remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion ([exact declaration](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak $2n+1$ alternative.
## Selected references
- LeanEval contributors, *Whitney embedding theorem (strong form, sharp dimension 2n)*, LeanEval v1 source declaration and manifest, statement revision 1, [pinned source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean) and [manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml). These specify the exact formal target.
- H. Whitney, *The self-intersections of a smooth n-manifold in 2n-space*, Annals of Mathematics (2) **45** (1944), 220–246, [DOI](https://doi.org/10.2307/1969265). Historical attribution as recorded in the LeanEval manifest; no alternate statement from this reference replaces the benchmark goal.
## Motivation: classify three-dimensional periodic symmetry
A **space group** describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in [Oliver Knill’s survey, §94, “Crystallography,” p. 41](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by **LeanEval v1**, not an unsolved classification conjecture. Its authoritative specification is [the declaration `LeanEval.Geometry.SpaceGroupsProblem.space_groups`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
## Setting: groups, transformations, and orientation
For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A **Euclidean isometry** is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the [benchmark’s definitions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $G$ is **discrete** when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.
Such a group is **crystallographic** when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called `cocompact`, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An **affine equivalence** between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An **orientation-preserving affine equivalence** additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The **Sohncke subfamily** restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the [source definitions and notes](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## Target: one conjunction, with all three exact counts
Write $C_{\mathrm{OP}}(d)$ for `crystallographicCountOP d`, $C(d)$ for `crystallographicCount d`, and $C_{\mathrm{OP,only}}(d)$ for `crystallographicCountOPOnly d`. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
$$
C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.
$$
This is the [exact benchmark conjunction](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
## Significance: exact cardinalities for the underlying groups
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in [Knill, §94](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
## Difficulty: a catalog is not a completeness theorem
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the [source’s cardinality assertion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
## Formalization scope: preserve the benchmark model
The Lean representation is `EuclideanSpace ℝ (Fin d)`, with affine isometries and affine equivalences from Mathlib. The [three source counting functions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) use `Set.encard` in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
## Selected references
- LeanEval contributors; problem submitted by Kim Morrison. *LeanEval v1: 230 space groups*, statement revision 1, 2026, repository commit `296b7491ec989d21bcf8636a9a69231a1e5d1d25`. [Exact Lean source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.
Discrete Mathematics—Lecture Notes I: Capacitated Hall MatchingTextbook
## Assigning distinct resources under compatibility constraints
A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.
This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's [Discrete Mathematics—Lecture Notes, §6.1](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html). Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.
## Graphs, matchings, and demands
A **finite simple graph** consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A **bipartition** is a pair of disjoint sets $L,R$ whose union is the vertex set, such that every edge joins a vertex in $L$ to a vertex in $R$. The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow [Definition 1.1 of the notes](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch1.S1.html).
For a vertex $x$, the **neighbor set** $N_G(x)$ contains the vertices joined to $x$. For a set $S$ of vertices, write $N_G(S)=\bigcup_{x\in S}N_G(x)$. A **matching** is an edge set in which no vertex is used twice. It is complete on $L$ if every left vertex is used, and **perfect** if every vertex is used. A **subgraph** may retain selected edges of the original graph. Its degree $\deg_H(x)$ counts the retained neighbors of $x$.
A **demand** is a natural number $d_x$ attached to each $x\in L$. Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.
## Formalization targets
The ordinary matching criterion is [Theorem 6.2](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html):
$$
\exists\text{ a complete matching on }L
\quad\Longleftrightarrow\quad
\forall S\subseteq L,\quad |S|\le |N_G(S)|.
$$
The development also includes Exercise 6.3, asserting that a $k$-regular bipartite graph has a perfect matching when $k>0$. Proposition 6.4 states the quantitative deficit version:
$$
\bigl(\forall S\subseteq L,\ |S|-d\le |N_G(S)|\bigr)
\quad\Longrightarrow\quad
\exists M\text{ matching},\quad |L|-d\le |E(M)|,
\qquad d\ge1.
$$
The capstone is the prescribed-degree equivalence of Exercise 6.5:
$$
\begin{split}
&\exists H\subseteq G:
\bigl(\forall x\in L,\ \deg_H(x)=d_x\bigr)
\land
\bigl(\forall y\in R,\ \deg_H(y)\le1\bigr)\\
&\qquad\Longleftrightarrow\quad
\forall S\subseteq L,\quad
\sum_{x\in S}d_x\le |N_G(S)|.
\end{split}
$$
This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.
The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets $(A_i)_{i\in I}$ has a **system of distinct representatives**, meaning an injective choice $f(i)\in A_i$, exactly when
$$
\forall J\subseteq I,\qquad
|J|\le \left|\bigcup_{i\in J}A_i\right|.
$$
Only the index family is finite; the sets themselves may be infinite.
## What the development provides
The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of [Exercises 6.3 and 6.5 and Proposition 6.4](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html).
Mathlib already provides finite-family and graph versions of Hall's theorem in its [Hall development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/Hall/Finite.lean) and [graph interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/SimpleGraph/Hall.lean). The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.
## Where exact formalization is delicate
Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.
Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.
## Formalization scope
The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.
Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.
The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.
## Selected references
- D. Yogeshwaran, *Discrete Mathematics—Lecture Notes*, Indian Statistical Institute Bangalore, HTML edition generated 2025. [Chapter 6.1](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html); [graph conventions](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch1.S1.html).
- The mathlib community, *Mathlib 4*, revision 777aaa6, 2026. [Finite-family Hall theorem](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/Hall/Finite.lean); [native graph Hall theorem](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/SimpleGraph/Hall.lean).
Lagarias criterion is equivalent to RHResearch Paper
## Motivation
The **Riemann hypothesis** concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in *An Elementary Problem Equivalent to the Riemann Hypothesis* ([Theorem 1.1](https://arxiv.org/abs/math/0008177v2)). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.
The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload ([Lagarias, §3](https://arxiv.org/abs/math/0008177v2)).
## Setting
For a positive integer $n$, its **divisor sum** is
$$\sigma(n)=\sum_{d\mid n}d,$$
where the sum runs over positive divisors, including $1$ and $n$. Its **harmonic number** is
$$H_n=\sum_{j=1}^{n}\frac1j.$$
All inequalities below are inequalities of real numbers. The symbols $\exp$ and $\log$ denote the real exponential and natural logarithm. The **Euler–Mascheroni constant** is $\gamma=\lim_{n\to\infty}(H_n-\log n)$.
The **Riemann zeta function** is obtained by analytic continuation of $\sum_{m=1}^{\infty}m^{-s}$ from $\operatorname{Re}(s)>1$. RH asserts that its nontrivial zeros have real part $1/2$. The **Lagarias elementary criterion** in this mission is the assertion that $\sigma(n)\le H_n+\exp(H_n)\log(H_n)$ for every positive integer $n$. These conventions agree with the arithmetic quantities in [Lagarias, Problem E](https://arxiv.org/abs/math/0008177v2), with the precise equality-clause distinction stated below.
## Formalization targets
### Main goal: the exact LeanEval equivalence
$$\mathrm{RH}\quad\Longleftrightarrow\quad
\forall n\in\mathbb N,\;n>0\Longrightarrow
\sigma(n)\le H_n+\exp(H_n)\log(H_n).$$
There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at $n=1$; the proof of the reverse implication in [Theorem 1.1, p. 8](https://arxiv.org/abs/math/0008177v2) uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.
### Supporting targets from the paper
The milestone list records the following source statements, with their thresholds unchanged:
* Lemma 3.1: for $n\ge3$,
$$e^\gamma n\log\log n\le\exp(H_n)\log(H_n).$$
* Lemma 3.2: for $n\ge20$,
$$H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.$$
* The finite check in the proof of Theorem 1.1: the criterion holds for $1\le n\le5040$, with equality exactly at $n=1$.
* Proposition 3.1, attributed to Robin: assuming RH, for $n\ge5041$,
$$\sigma(n)\le e^\gamma n\log\log n.$$
* Proposition 3.2, attributed to Robin: if RH is false, some fixed $0<\beta<1/2$ and $C>0$ satisfy
$$\sigma(n)\ge e^\gamma n\log\log n+
\frac{Cn\log\log n}{(\log n)^\beta}$$
for arbitrarily large integers $n$.
All five are taken from [Lagarias, §3, pp. 6–8](https://arxiv.org/abs/math/0008177v2); the finite check is explicitly an unnumbered step, not a newly attributed lemma.
## Significance
The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of [Lagarias's theorem](https://arxiv.org/abs/math/0008177v2).
The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.
## Difficulty
The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them ([Lagarias, Propositions 3.1–3.2](https://arxiv.org/abs/math/0008177v2)).
The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.
## Formalization scope
The goal is `LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion`, with type `RiemannHypothesis ↔ LagariasElementaryCriterion`. The criterion definition is copied from the benchmark. `σ 1 n` is natural-valued and cast to the reals; `harmonic n` is rational-valued and cast to the reals. RH remains Mathlib's predicate on `riemannZeta`, excluding negative even trivial zeros and the point $s=1$. No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.
The goal excludes $n=0$ and includes $n=1$. Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining $n\ge3$; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by `Real.rpow`, not natural exponentiation. Constants are chosen before the arbitrary cutoff.
The benchmark pins Lean 4.33.0 and Mathlib `6f1ef4e5dd604a435bddba4747b13970cd65d2a1`. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.
## Selected references
* Jeffrey C. Lagarias, *An Elementary Problem Equivalent to the Riemann Hypothesis*, American Mathematical Monthly **109** (2002), 534–543. [arXiv:math/0008177v2](https://arxiv.org/abs/math/0008177v2), posted 6 May 2001. The theorem, proposition, equation, and page numbers in this proposal refer to this nine-page arXiv version.
* Guy Robin, *Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann*, Journal de Mathématiques Pures et Appliquées **63** (1984), 187–213. [Bibliography entry [18] in Lagarias](https://arxiv.org/abs/math/0008177v2). The milestone formulations are those explicitly reproduced and attributed in Lagarias's Propositions 3.1 and 3.2.
Ordinary p-adic L-functions: Mazur–Tate–Teitelbaum interpolationResearch Paper
## Why construct a p-adic L-function?
A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 ([MTT](https://doi.org/10.1007/BF01388731)); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
## Modular forms, periods, and measures
Fix a prime $p$, a positive integer $N$, and a weight $k\ge2$. Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$. No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$.
The form is **ordinary** when $|\iota_p(a_p)|_p=1$. The **ordinary root** $\alpha$ is the root of
$$X^2-\iota_p(a_p)X+\iota_p(\epsilon(p))p^{k-1}$$
with $|\alpha|_p=1$. This convention also covers the $U_p$ case: if $p\mid N$, then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ ([MTT I.§12](https://doi.org/10.1007/BF01388731)).
A **measure** means a continuous $\mathbb C_p$-linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$. It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's `AbstractMeasure` on `(PadicInt p)ˣ`.
The two **periods** $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write
$$\Phi_j(r)=2\pi\int_0^\infty f(r+it)(r+it)^j\,dt,$$
and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$. A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$, and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in [MTT I.§2](https://doi.org/10.1007/BF01388731); see also the explicit treatment of general eigenforms in [Williams, §11.7](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
## Formalization targets
The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$, where $n\ge0$, and let $0\le j\le k-2$. Put $s=\chi(-1)(-1)^j$. With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$, define the algebraic number $A_{\chi,j}$ by
$$\iota_\infty(A_{\chi,j})=
\frac{m^{j+1}j!}{(-2\pi i)^j\tau(\chi^{-1})\Omega^s}
L(f_{\chi^{-1}},j+1).$$
The required identity is
$$\int_{\mathbb Z_p^\times}\iota_p(\chi(x))x^j\,d\mu(x)
=e_p(\alpha,\chi,j)\,\iota_p(A_{\chi,j}),$$
where all algebraic character values in the following expression are transported by $\iota_p$:
$$e_p(\alpha,\chi,j)=\alpha^{-n}
\left(1-\frac{\iota_p(\chi^{-1}(p)\epsilon(p))p^{k-2-j}}{\alpha}\right)
\left(1-\frac{\iota_p(\chi(p))p^j}{\alpha}\right).$$
This is the scalar period-normalized form of [MTT I.§14](https://doi.org/10.1007/BF01388731). At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$. At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
## What the formalization supplies
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
## Where the difficulty lies
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
## Formalization scope and conventions
The cusp form is Mathlib's analytic `CuspForm`, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$, and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of $\mathbb Q$; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$. The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$, are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$.
The signed projections use a factor of $1/2$. Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$. These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
## Selected references
- B. Mazur, J. Tate and J. Teitelbaum, *On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. [DOI](https://doi.org/10.1007/BF01388731); [digitized original](https://gdz.sub.uni-goettingen.de/download/pdf/PPN356556735_0084/LOG_0007.pdf).
- G. Shimura, *On the periods of modular forms*, Mathematische Annalen 229 (1977), 211–221. [DOI](https://doi.org/10.1007/BF01391466).
- C. Williams, *An introduction to p-adic L-functions II: Modular forms*, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. [Author's notes](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem
# Motivation
The mission is to prove the combined open goal
$$
\text{Problem 97} \;\land\; \text{Problem 96}
$$
for finite point sets in strictly convex position in the Euclidean plane.
## Why Problems 97 and 96 belong together
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every
nonempty convex-independent finite set then has a vertex with at most three
neighbors at each positive radius, in particular at radius $1$. Delete that
vertex and preserve convex independence. Apply the same step to every subset
created by deletion until no points remain.
Charge each unordered unit-distance pair to the first endpoint deleted. Each
deleted vertex receives at most three charges, so an $n$-point set determines
at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound
and therefore $O(n)$. The package uses this one-way dependency; it does not
seek a reverse implication.
# Setting
Let $A\subset\mathbb R^2$ be finite. Strict convex position is represented by
the upstream predicate `EuclideanGeometry.ConvexIndep`: every point of $A$ is
an extreme point of the convex hull of $A$. For $p\in A$, the pinned
multiplicity at radius $r>0$ counts points $q\in A$ with
$\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four
such other points. Problem 96 counts unordered pairs at distance $1$, then
takes the supremum over convex-independent $n$-point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an
earlier three-neighbor version. His 1987 account reports Danzer’s convex
nonagon in which every vertex has three equidistant witnesses, and asks about
four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex
configuration with the same unit distance at every vertex, placing the local
question beside the unit-distance problem.
# Target
The Problem 97 target is the canonical statement that every nonempty finite
convex-independent $A$ has no four-equidistant-point property:
$$
\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A)
\;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).
$$
The Problem 96 target is the canonical asymptotic statement
$$
U_c(n)=O(n),
$$
where $U_c(n)$ is the supremum of the unordered unit-distance counts
determined by convex-independent $n$-point sets. The bound is asymptotic;
the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$
for every natural number $n$.
# Significance
The package records a formal proof route joining a pinned geometric obstruction
to a global extremal bound. A successful Problem 97 proof would immediately
settle Problem 96 with the explicit constant $3$, while preserving the
combinatorial meaning of the count. It also separates the historical
three-neighbor constructions from the still-open four-neighbor assertion.
# Difficulty
The source proof reduces Problem 97 to strong induction on $|A|$. Its counting
engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness
refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib
(2013). This engine forces every counterexample to have at least nine points; a
finite geometric analysis excludes exactly nine points; and the remaining step must
produce a removable vertex for every larger minimal counterexample. The
removable-vertex statement carries the induction hypothesis that every
strictly smaller nonempty convex 4-equidistant set is contradictory. That
large-cardinality geometric step remains open, so both headline targets remain
open. Finite computational certificates can support local cases but do not
replace the universal geometric statement.
# Counterexample routes
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
[`Problem97.IsCounterexample`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/a46894f6078319d3001d06310531df50af0f6bbd/lean/Erdos9796Proof/P97/UniversalProblem97.lean#L24-L29).
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one
finite convex configuration cannot refute it. A counterexample must instead
give convex-independent point sets at arbitrarily large cardinalities whose
unit-distance counts exceed every proposed linear constant. The mission tracks
this superlinear-family statement separately, together with a reduction from
it to the exact negation of Problem 96. This keeps both possible outcomes
visible: a direct or Problem-97-derived linear upper bound, and an explicit
family proving that no such bound exists.
# Formalization scope
The canonical source is pinned at commit
`757d852766f377f7c1a0ffeeef6d3526bc0cb7a4`. Source-repository exports are
[`Problem97.erdos97_rhs`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/UpstreamBridge.lean#L30)
and [`Problem96.erdos96_rhs`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/UpstreamBridge.lean#L96).
The source repository reports closed proofs of the conditional bridge to the $3n$ bound
([`unit_distance_pairs_bound_of_erdos97`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/EuclideanPeeling.lean#L273)),
the $|A|\ge9$ counting milestone
([`counterexample_card_ge_nine`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/Counting.lean#L95)),
and the exact nine-point exclusion
([`FiniteN9Closure`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean#L56)).
The large-cardinality milestone is
[`RemovableVertexOfLarge`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/RemovableVertexAxiom/RemovableVertexOfLarge.lean#L50),
with its minimality hypothesis retained. The current platform draft contains
statement-level sketches and no imported source proofs. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean `v4.27.0`; these mission statements target the
platform's `v4.33.1`. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
Planned milestones are the two canonical roots, their conditional bridge, the
`|A| ≥ 9` count, the `n = 9` exclusion, the `|A| > 9` removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
# References
- Erdős, *On Sets of Distances of n Points* (1946), [DOI](https://doi.org/10.1080/00029890.1946.11991674).
- Erdős, *Some Combinatorial and Metric Problems in Geometry* (1987), [scan](https://www.renyi.hu/~p_erdos/1987-27.pdf).
- Fishburn–Reeds, *Unit Distances Between Vertices of a Convex Polygon* (1992), [publisher record](https://www.sciencedirect.com/science/article/pii/092577219290026O).
- Dumitrescu, *On Distinct Distances from a Vertex of a Convex Polygon* (2006), [Springer record](https://link.springer.com/article/10.1007/s00454-006-1262-y); provenance for the source counting method.
- Nivasch–Pach–Pinchasi–Zerbib, *The Number of Distinct Distances from a Vertex of a Convex Polygon* (2013), [arXiv:1207.1266](https://arxiv.org/abs/1207.1266); provenance for the cap-witness refinements used by the source formalization.
Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper
# Motivation
Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.
This mission formalizes the paper that started the **probabilistic method** as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$. It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$.
**Timeline.** Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.
# Setting
Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$. A **graph** is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$; here vertices are labeled $0, \dots, N-1$. A subset $s \subseteq V$ of size $k$ is a **clique** if every two distinct vertices of $s$ are adjacent, and an **independent set** if every two distinct vertices of $s$ are non-adjacent. A $k$-set that is either a clique or an independent set is **monochromatic**: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).
The ambient probability space is the uniform distribution over **all** graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$. This space has exactly $2^{\binom{N}{2}}$ elements.
A graph with no monochromatic $k$-set is a graph with neither a $k$-clique nor an independent $k$-set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.
# Formalization targets
### Goal: the probabilistic lower bound
$$R(k) > 2^{k/2}, \qquad k \ge 3$$
i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$-set.
### Stronger: the three steps of the proof, as separate targets
1. **Count estimate.** For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$,
$$\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.$$
2. **Union-bound principle.** In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:
$$\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$
3. **Pair-count bound.** Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$-set in $G$ is at most
$$\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.$$
The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.
# Significance
**The result.** The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).
**Formalizing it.** Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$.
# Difficulty
The central difficulty is that the bad events — "the $k$-set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$-sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.
A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$-set ($2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.
# Formalization scope
**Representation.** Graphs are `SimpleGraph (Fin N)`: a relation on $N$ labeled vertices. A candidate set is a `Finset (Fin N)` of cardinality $k$; "monochromatic" is `IsClique ∨ IsIndepSet` on the graph; "no monochromatic $k$-set" is the predicate `NoMonoK`. All counting is cardinality of finite sets; `monoCount N k G` is the number of monochromatic $k$-sets of $G$.
**Conventions.** $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$. The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$, is a natural follow-up contribution).
**Reusability.** The union-bound principle, the monochromatic-$k$-set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining `ramseyNumber` and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.
# Selected references
- Paul Erdős, *Some remarks on the theory of graphs*, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$.
- Noga Alon, Joel H. Spencer, *The Probabilistic Method*, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
- Stanisław Radziszowski, *Small Ramsey Numbers*, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.
## Context: where this sits in the formalization landscape
This mission is **not** a duplicate of existing platform content, and the choice of target is deliberate:
- **Mathlib gap.** The pinned environment (mathlib `0df444a`) contains no Ramsey-number theory at all — nothing in `Combinatorics/SimpleGraph`, no `ramseyNumber`-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
- **Existing Ramsey content is a different quantity.** The platform's fully-proved `Erdos183` mission concerns *multicolour triangle* Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
- **Directly load-bearing for a live open problem.** The public open problem *diagonal_ramsey_asymptotics* (same environment `0df444a`) asks, eventually in $k$, for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$; its upper half is already proved as `ramsey_theory_upper_bound`. The lower half is exactly what this mission's goal supplies: once `ramsey_lower_bound` is proved, closing that open problem reduces to a translation between the graph formulation used here (`SimpleGraph` / `NoMonoK`) and the edge-colouring formulation (`ramseyDiag`) used there, plus the eventual-quantifier wrapper.
- **Formalization convention.** The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$.
## 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/
Picard groups of semi-local or finite semiringsOpen Problem
# Motivation
Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?
This mission turns CUHK-Shenzhen AI Math Problem 19, **Picard groups of semi-local or finite 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 main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.
## Suggested attack route
Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.
## Formalization scope
The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/19.html)
- [Facets of Module Theory over Semirings](https://arxiv.org/abs/2405.18645)
- [MathOverflow discussion](https://mathoverflow.net/questions/511864/picard-group-of-semi-local-or-finite-semirings)
Equality case for compressed convex functional calculusOpen Problem
## Motivation and history
Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The **compression-rigidity question** asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.
The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The [original problem](https://rybindmitry.github.io/problems/2.html) asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.
## Setting
Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A **positive contraction** $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$, and has operator norm at most one. Both zero and the identity are permitted.
Write $S=[0,1]^2$. Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$. Their **joint continuous functional calculus** assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$. It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$. The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is [Dereziński, Lemma 6.6, printed page 43](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
An **orthogonal projection** is an operator $P$ satisfying $P^*=P$ and $P^2=P$. The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$, not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.
## Formalization targets
The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and **strictly convex**: for distinct $x,y\in S$ and $0<t<1$, its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$. For $X,Y,P$ as above, the question is whether
$$
P f(X,Y)P=P f(PXP,PYP)P
\quad\Longrightarrow\quad
PX=XP\ \text{and}\ PY=YP.
$$
Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$. Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the [source](https://rybindmitry.github.io/problems/2.html).
The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$,
$$
\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad
\Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,
$$
where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of [Lemma 6.6](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43), not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.
## Significance
A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.
The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.
## Difficulty
Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.
Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.
## Formalization scope
The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$, $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.
The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$. Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.
Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.
The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.
## Selected references
- Boris Bilich, *Equality case for compressed convex functional calculus*, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. [Original statement](https://rybindmitry.github.io/problems/2.html).
- Jan Dereziński, *Bounded operators*, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. [Joint continuous functional calculus](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
Hatcher Algebraic Topology I: The Fundamental Group of the CircleTextbook
## Motivation
The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; freely available at [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).
This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace `Hatcher`.
## Setting
A **path** in a topological space $X$ is a continuous map $f : I \to X$, where $I = [0,1]$. A **homotopy of paths** is a family $f_t : I \to X$, $0 \le t \le 1$, such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$, $F(s,t) = f_t(s)$, is continuous. A **loop** at a **basepoint** $x_0$ is a path with $f(0) = f(1) = x_0$. The set of homotopy classes $[f]$ of loops at $x_0$ is the **fundamental group** $\pi_1(X, x_0)$; its product is $[f][g] = [f\cdot g]$, where $f\cdot g$ traverses $f$ and then $g$, each at double speed (Hatcher, Proposition 1.3).
The **circle** $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$, so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$. Hatcher's map
$$p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}$$
is `Hatcher.circleCover`. The loops
$$\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},$$
based at $(1,0)$ are `Hatcher.omegaLoopN n`, and $\omega = \omega_1$ is `Hatcher.omegaLoop`; its class $[\omega] \in \pi_1(S^1, 1)$ is `Hatcher.omegaClass`.
A **covering space** of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$, p. 29; such a $U$ is **evenly covered**). A **lift** of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$.
## Formalization targets
### Goal (Theorem 1.7)
$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$. In the form stated in Lean:
$$\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.$$
Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.
### Milestones on the road to the goal
1. $p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
2. Homotopy lifting property (c): for a covering space $p : \tilde X \to X$, a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
3. Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
4. Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
5. Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
6. $[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).
### Applications (Theorems 1.8–1.10)
$$\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.$$
$$\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}$$
$$\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.$$
## Significance
*The result itself.* The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.
*Formalizing it.* Mathlib (revision `0df444a`) already contains the covering-space infrastructure: `IsCoveringMap`, path lifting (`IsCoveringMap.liftPath`, `eq_liftPath_iff'`), homotopy lifting (`IsCoveringMap.liftHomotopy`, `eq_liftHomotopy_iff'`), monodromy, and the fact that `Circle.exp` is a covering map (`Circle.isCoveringMap_exp`). It also has `FundamentalGroup X x` as the endomorphism group of the fundamental groupoid. It does **not** contain the computation $\pi_1(S^1) \cong \mathbb{Z}$, nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as `Complex.exists_root` (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.
## Difficulty
The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$: this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.
Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. `FundamentalGroup Circle 1` multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.
For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$. For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.
## Formalization scope
* $S^1$ is `Circle` (the unit circle in $\mathbb{C}$) with basepoint `1`; $D^2$ is `Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1`; $S^2$ is `Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1`, with $-x$ the antipodal point.
* A covering space is Mathlib's `IsCoveringMap p`. This agrees with Hatcher's condition $(\ast)$; neither requires $p$ to be surjective.
* Paths are continuous maps `C(I, X)` or Mathlib `Path`s; for homotopies of paths, the square is written `I × I` with Hatcher's coordinate order $F(s,t) = f_t(s)$: the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is `Y × I` with $Y$ an arbitrary topological space, as in Hatcher.
* $\pi_1(S^1, 1)$ is Mathlib's `FundamentalGroup Circle 1`, and $[\omega]$ is `FundamentalGroup.fromPath ⟦omegaLoop⟧`. Because the goal quantifies over integer powers of a single element, the order of multiplication in `FundamentalGroup` is immaterial to its truth.
* The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$, so that the generator is pinned to Hatcher's explicit loop; an isomorphism `FundamentalGroup Circle 1 ≃* Multiplicative ℤ` sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
* "Nonconstant polynomial" is `0 < f.degree`, which excludes both the zero polynomial and nonzero constants.
Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in `Circle` that later chapters of the series can import.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- L. E. J. Brouwer, *Über Abbildung von Mannigfaltigkeiten*, Mathematische Annalen 71 (1911), 97–115. [https://doi.org/10.1007/BF01456931](https://doi.org/10.1007/BF01456931)
- K. Borsuk, *Drei Sätze über die n-dimensionale euklidische Sphäre*, Fundamenta Mathematicae 20 (1933), 177–190. [https://doi.org/10.4064/fm-20-1-177-190](https://doi.org/10.4064/fm-20-1-177-190)
- Mathlib, `Mathlib/Topology/Homotopy/Lifting.lean` (path and homotopy lifting for covering maps). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean)
- Mathlib, `Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean` (the fundamental group). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)
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)](https://arxiv.org/abs/2608.16205).
## 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
- [Original problem](https://rybindmitry.github.io/problems/20.html)
- [Resolved 2026 paper](https://arxiv.org/abs/2608.16205)
- [Lean proof repository](https://github.com/wqirocks/transpose-injectivity)
Positive definite matrix integral inequalityOpen Problem
# Motivation
The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.
This mission turns CUHK-Shenzhen AI Math Problem 1, **Positive definite matrix integral inequality**, 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
For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.
## Suggested attack route
Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.
## Formalization scope
The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on May 28, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/1.html)
Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook
## Motivation
Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.
## Setting
The **basic problem** (§1.2 of the book): a discrete-time system
$$x_{k+1} = f_k(x_k, u_k, w_k), \qquad k = 0, 1, \dots, N-1,$$
with state $x_k \in S$, control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$, and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$. A **policy** is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$; it is **admissible** if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is
$$J_\pi(x_0) = \mathbb{E}\Big[ g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, \mu_k(x_k), w_k) \Big].$$
In the Lean development these are `BertsekasDPModel`, `BertsekasDPPolicyCost` (backward recursion on remaining stages), and the DP recursion `BertsekasDPValue`:
$$J_N = g_N, \qquad J_k(x) = \min_{u \in U_k(x)} \mathbb{E}_w\big[ g_k(x,u,w) + J_{k+1}(f_k(x,u,w)) \big].$$
Section 1.6 of the book develops the **minimax** variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$; the mission mirrors it with `BertsekasMinimaxDPModel`, `BertsekasMinimaxPolicyCost`, `BertsekasMinimaxValue`.
## Target
$$J_0(x_0) \;=\; \min_{\pi \text{ admissible}} J_\pi(x_0), \qquad \text{with the minimum attained,}$$
formalized as `BertsekasDP.dp_algorithm_optimality`: the DP value at the horizon is an `IsLeast` of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (`minimax_selection_interchange`) and the minimax DP validity (`minimax_dp_algorithm`).
## Significance
The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).
## Difficulty
The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.
## Formalization scope
Finite disturbance space (`Fintype W`), finite nonempty control-constraint sets (`Finset`, `inf'`), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
- R. Bellman, *Dynamic Programming*, Princeton University Press, 1957.
## The problem
**(a)** In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$. Let $n,m$ be odd positive integers greater than $1$. You have the choice between playing a best-of-$nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of-$n$ of best-of-$m$'s (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of-$nm$.
**(b)** We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$. You have the choice between playing a best-of-$nm_1\cdots m_k$, or a best-of-$n$ of "sets", which are best-of-$m_1$'s of "games", …, which are best-of-$m_k$'s of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.
**(c)** We consider a further generalization where each completed "set" counts toward the match score in an independently random way:
- with probability $a$, the winner gains $1$ in the match score, as usual;
- with probability $b$, the set is ignored and does not count toward the match score;
- with probability $c$, the *loser* gains $1$ in the match score;
with $a+b+c=1$ and $a>c$, so players are still incentivized to win sets (previously we had $a=1$, $b=c=0$). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-$nm_1\cdots m_k$, then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$. Prove that your probability of winning the match is still strictly greater by playing the best-of-$nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).
**(d)** Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$, prove that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.
## Source and connection to Dorner–Hardt
Florian E. Dorner and Moritz Hardt, *Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget*, ICML 2024. [arXiv:2402.02249](https://arxiv.org/abs/2402.02249) (v3, 8 April 2026).
The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.
**Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language.** A point is a single crowdworker label being correct ($q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:
$$a=(p+\epsilon)(1-p),\qquad c=p(1-p-\epsilon),\qquad b=1-a-c,$$
so that $a-c=\epsilon>0$, and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$, $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$. The paper's inequality also allows $n=1$ and $q=1$, which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is **not** claimed here.
**Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$.** The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$, $q=0.6$, $m=3$, $n=1$, the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$.
## Timeline
- **Feb 2024** — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
- **Oct 2024** — arXiv v2.
- **Apr 2026** — arXiv v3; conjecture still stated as open.
- **Aug 2026** — private proof of the Section 3 inequality (strict win, $b\ge1/2$, one level) via exponential tilting of the tie probability.
- **Sep 2026** — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.
## Conventions in the formal statement
"Greater than $1$" is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.
Multiplicative Number Theory I: Siegel–Walfisz and the Three Primes TheoremTextbook
## Primes in progressions, uniformly in the modulus
Applying the circle method to an additive problem about primes requires counting primes
in arithmetic progressions with an error term *uniform in the modulus*: the modulus is
not fixed in advance, it grows with the size of the numbers being represented. The
**Siegel–Walfisz theorem** is the classical statement of that uniformity, valid for every
modulus up to a fixed power of $\log x$, and it is the one analytic ingredient the
standard proof of **Vinogradov's three primes theorem** cannot do without.
The history is a sequence of partial uniformities:
* **1837.** Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains
infinitely many primes, for each fixed $q$, with no rate
([Dirichlet's theorem](https://en.wikipedia.org/wiki/Dirichlet%27s_theorem_on_arithmetic_progressions)).
* **1896–1899.** De la Vallée Poussin proves the prime number theorem with the error
term $O(x e^{-c\sqrt{\log x}})$, and extends the zero-free region from $\zeta$ to
$L(s,\chi)$, obtaining the prime number theorem in progressions for each *fixed* $q$
([PNT](https://en.wikipedia.org/wiki/Prime_number_theorem)).
* **1918–1935.** Landau and Page isolate the obstruction to uniformity: a single real
zero near $s=1$, attached to a quadratic character. Landau shows at most one of two
distinct real primitive characters can have such a zero; Page shows at most one
modulus below a given bound can, yielding unconditional uniformity for $q$ up to a
bounded power of $\log x$
([Page's theorem](https://encyclopediaofmath.org/wiki/Page_theorem)).
* **1935.** Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real
primitive $\chi$, at the price of an ineffective constant
([Siegel](https://eudml.org/doc/205054)).
* **1936.** Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and
obtains uniformity for every fixed power $q \le (\log x)^A$
([Walfisz](https://doi.org/10.1007/BF01218882)).
* **1937.** Vinogradov proves that every sufficiently large odd integer is a sum of
three primes ([Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)).
* **2013.** Helfgott removes the "sufficiently large", settling ternary Goldbach for all
odd $n > 5$ ([arXiv:1312.7748](https://arxiv.org/abs/1312.7748)).
## Setting
The **von Mangoldt function** $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power
and $0$ otherwise. The **Chebyshev function** $\psi(x) = \sum_{n \le x} \Lambda(n)$
counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$.
A **Dirichlet character** modulo $q$ is a multiplicative function
$\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$, supported on the units and taking root-of-unity
values there. The **principal character** $\chi = 1$ is the indicator of the units; a
character is **quadratic** (real) if $\chi^2 = 1$ and $\chi \neq 1$, and **primitive** if
it is not induced by a character of a proper divisor of $q$. The **Dirichlet
$L$-function** $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$, defined for
$\operatorname{Re} s > 1$, extends meromorphically to $\mathbb{C}$, entire except for a
simple pole at $s = 1$ when $\chi$ is principal.
The two counting functions of the mission are the **twisted von Mangoldt sum** and the
**progression sum**
$$\psi(N,\chi) = \sum_{n < N} \Lambda(n)\chi(n), \qquad
\psi(N;q,a) = \sum_{\substack{n < N \\ n \equiv a\ (q)}} \Lambda(n),$$
related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal
and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the
classical zero-free region is an **exceptional zero** (a Siegel zero); the set of such
zeros for a given $\chi$ is the **exceptional set** $E$, which the results below
constrain to have at most one element.
## Formalization targets
The attack path follows Davenport, *Multiplicative Number Theory*, 3rd ed., §§14, 18,
20, 21, 22.
**(1) `zero_free_region` (§14, pp. 88–96).** There is an absolute $c>0$ such that for
every $q \ge 1$ and every $\chi \bmod q$,
$$L(s,\chi) \neq 0 \quad\text{for } s \neq 1,\ \operatorname{Re} s \ \ge\ 1 -
\frac{c}{\log\big(q(|\operatorname{Im} s| + 2)\big)},$$
with at most one exception, which is real, lies in $(0,1)$, is a simple zero, and can
occur only for quadratic non-principal $\chi$.
**(2) `pnt_dlvp` (§18, pp. 111–114).** For some $c > 0$ and all $x \ge 2$,
$$\psi(x) = x + O\!\left(x\,e^{-c\sqrt{\log x}}\right).$$
**(3) `psi_char_of_region` (§20, pp. 121–125).** For a region constant $c>0$ there are
$c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with
respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$,
$$\psi(N,\chi) = \delta_\chi N - \sum_{\beta \in E} \frac{N^\beta}{\beta}
+ O\!\left(N e^{-c_1\sqrt{\log N}}\right).$$
**(4) `siegel` (§21, pp. 126–131).** For every $\varepsilon > 0$ there is
$C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,
$$L(1,\chi) > C(\varepsilon)\, q^{-\varepsilon}.$$
**(5) `siegel_zero` (§21, second form).** For every $\varepsilon > 0$ there is
$C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,
$$L(\sigma,\chi) \neq 0 \quad \text{for all real } \sigma > 1 - C(\varepsilon)q^{-\varepsilon}.$$
**(6) `siegelWalfisz` (§22, pp. 132–134).** For every $A > 0$ there are $C, c > 0$ such
that for all $q \ge 1$, all $\chi \bmod q$, and all $N \ge 2$ with $q \le (\log N)^A$,
$$\big\lVert \psi(N,\chi) - \delta_\chi N \big\rVert \le C N e^{-c\sqrt{\log N}}.$$
This is literally the platform proposition `ThreePrimes.SiegelWalfisz`.
A corollary, not a milestone, records the progression form `siegel_walfisz_ap`: for
$(a,q)=1$ and $q \le (\log N)^A$,
$$\psi(N;q,a) = \frac{N}{\varphi(q)} + O_A\!\left(N e^{-c\sqrt{\log N}}\right).$$
**Goal (`three_primes`, §26).** There is $N_0$ such that every odd $n \ge N_0$ is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing `ThreePrimes.ThreePrimesExistence` from `ThreePrimes.SiegelWalfisz`. The goal
leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
## What the result gives, and what remains to be formalized
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method
for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without
it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace `ThreePrimes`
(by user `tabbott`), following Vaughan, *The Hardy–Littlewood Method*, Ch. 3, and
Davenport §26. It is **conditional**: it takes Siegel–Walfisz as an explicit hypothesis
`ThreePrimes.SiegelWalfisz`. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of $L(s,\chi)$
([`DirichletCharacter.LFunction`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/DirichletContinuation.html)),
its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$,
Dirichlet's theorem, and the Chebyshev function. It does **not** contain the zero-free
region for $L(s,\chi)$, the explicit formula for $\psi(x,\chi)$, Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
[PNT+ project](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) contour
machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$
inequality, a zero-free rectangle, and `MediumPNT`,
$\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$. That is a template for the $L(s,\chi)$
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
## Where the obvious argument fails
The first idea is to run the $\zeta$ argument character by character. It works for
complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off
$\operatorname{Re} s = 1$ compares $\chi$, $\chi^2$ and the trivial character at nearby
points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of
$L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the
inequality degrades from "no zeros" to "at most one zero" and stops there. Every later
step inherits that unexcluded zero: milestone (3) can only be stated with the
$N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for
$q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and
nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on
$\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results
are qualitative, carry no rate, and are not uniform in $q$.
## Formalization scope
Sums run over $n < N$ with $N \in \mathbb{N}$, matching `Vino.vmSumChar` and
`ThreePrimes.SiegelWalfisz`; Davenport sums over $n \le x$. The two differ by the single
term $\Lambda(N) \le \log N$, negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's `Chebyshev.psi`. $L(s,\chi)$ is Mathlib's
`DirichletCharacter.LFunction`, so no continuation is reconstructed.
The zero-free region is `Davenport.InRegion c q s`, namely
$\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$; the exceptional zero
is packaged as `IsExceptionalSet c χ E`: $E$ is a subsingleton, every element is a real
zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$,
and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$. Milestone (1) adds
simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$.
Milestone (3) takes the region constant $c > 0$ as a *parameter* rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large $c$ the
hypothesis `IsExceptionalSet c χ E` may be unsatisfiable for some $\chi$, making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for *every*
$\chi$, so instantiating milestone (3) at that $c$ discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for `χ.IsQuadratic`, `χ ≠ 1`, `χ.IsPrimitive` characters, with
the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$; since $L(1,\chi)$ is real
for real $\chi$, this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are **ineffective**; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term $N$
(`if χ = 1 then (N : ℂ) else 0`); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal $\chi$.
Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a
genuine saving over the trivial $\psi(N,\chi) \ll N$; with $c = 0$ allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for
$L(s,\chi)$ as an entire function of order $1$, the zero-counting estimate $N(T,\chi)$
(§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120),
Perron-type contour truncation, and the imprimitive-to-primitive reduction
$|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$. All of it is reusable well
beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's
theorem, and effective Chebotarev. Contributions of these supporting results, of
alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the
$\pi(x;q,a)$ versions, and of sharper constants are welcome.
## Selected references
- H. Davenport, *Multiplicative Number Theory*, 3rd ed., revised by H. L. Montgomery,
GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26.
[doi:10.1007/978-1-4757-5927-3](https://doi.org/10.1007/978-1-4757-5927-3)
- H. L. Montgomery and R. C. Vaughan, *Multiplicative Number Theory I: Classical
Theory*, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16,
12.10; Corollaries 11.10, 11.12, 11.17, 11.19).
[doi:10.1017/CBO9780511618314](https://doi.org/10.1017/CBO9780511618314)
- R. C. Vaughan, *The Hardy–Littlewood Method*, 2nd ed., Cambridge University Press,
1997. Ch. 3. [doi:10.1017/CBO9780511470929](https://doi.org/10.1017/CBO9780511470929)
- C. L. Siegel, *Über die Classenzahl quadratischer Zahlkörper*, Acta Arithmetica 1
(1935), 83–86. [eudml:205054](https://eudml.org/doc/205054)
- A. Walfisz, *Zur additiven Zahlentheorie II*, Mathematische Zeitschrift 40 (1936),
592–607. [doi:10.1007/BF01218882](https://doi.org/10.1007/BF01218882)
- I. M. Vinogradov, *Representation of an odd number as a sum of three primes*, Doklady
Akad. Nauk SSSR 15 (1937), 291–294.
[Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)
- H. A. Helfgott, *The ternary Goldbach conjecture is true*, 2013.
[arXiv:1312.7748](https://arxiv.org/abs/1312.7748)
- *Siegel–Walfisz theorem*, Wikipedia.
[link](https://en.wikipedia.org/wiki/Siegel%E2%80%93Walfisz_theorem)
- *Page theorem*, Encyclopedia of Mathematics.
[link](https://encyclopediaofmath.org/wiki/Page_theorem)
- A. Kontorovich et al., *PrimeNumberTheoremAnd* (PNT+), Lean formalization project.
[github](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)
- Mathlib, `Mathlib.NumberTheory.LSeries.DirichletContinuation`.
[docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/DirichletContinuation.html)
## Motivation
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
## Timeline
- **1963.** Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show *any* norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
- **1981.** Beck and Fiala ([Discrete Appl. Math.](https://doi.org/10.1016/0166-218X(81)90022-6)) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
- **1980s.** Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's *Ten Lectures* (1987) as the central open problem of the area.
- **1985.** Spencer ([Trans. AMS](https://doi.org/10.1090/S0002-9947-1985-0784009-0)) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
- **1998.** Banaszczyk ([Random Struct. Algorithms](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
- **2010–2016.** The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg ([STOC 2016](https://arxiv.org/abs/1605.02882)) give a polynomial-time algorithm matching Banaszczyk's bound.
- **2023.** Kunisky ([SIAM J. Discrete Math.](https://arxiv.org/abs/2111.02974)) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
- **2025.** Bansal and Jiang ([arXiv:2508.03961](https://arxiv.org/abs/2508.03961)) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.
## Setting
Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A **sign vector** is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the **discrepancy** of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The **Komlós property at constant $K$** — `KomlosBound K` — says that *every* such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.
Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.
## Formalization targets
### Goal — the Komlós conjecture
$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$
The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.
### Milestones — the known ladder
Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.
## Significance
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
## Difficulty
Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.
## Formalization scope
The Lean model commits to: vectors as `EuclideanSpace ℝ (Fin m)`, whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads `‖v i‖ ≤ 1`); the $\ell^\infty$ conclusion written coordinatewise as `∀ j, |∑ i, ε i * v i j| ≤ K`, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with `ε i = 1 ∨ ε i = -1`; and set systems as matrices `A : Fin m → Fin n → ℝ` with an entrywise $0/1$ hypothesis and column-degree counted by `Set.ncard`. Quantifier order matters everywhere: in `KomlosBound K` the constant is fixed *before* $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In `beck_fiala` the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.
Welcome contributions: any milestone in any order — `beck_fiala` and `komlos_implies_beck_fiala` are self-contained finite arguments and the natural entry points; `spencer_six_deviations` and `banaszczyk_bound` each import a major technique; `komlos_lower_bound` needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
## Selected references
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Applied Mathematics 3 (1981). [doi:10.1016/0166-218X(81)90022-6](https://doi.org/10.1016/0166-218X(81)90022-6)
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985). [doi:10.1090/S0002-9947-1985-0784009-0](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- W. Banaszczyk, *Balancing vectors and Gaussian measures of n-dimensional convex bodies*, Random Structures & Algorithms 12 (1998). [doi link](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)
- N. Bansal, D. Dadush, S. Garg, *An algorithm for Komlós conjecture matching Banaszczyk's bound*, FOCS 2016 / SIAM J. Comput. [arXiv:1605.02882](https://arxiv.org/abs/1605.02882)
- N. Bansal, H. Jiang, *Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk*, 2025. [arXiv:2508.03961](https://arxiv.org/abs/2508.03961)
- D. Kunisky, *The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant*, SIAM J. Discrete Math. 37 (2023). [arXiv:2111.02974](https://arxiv.org/abs/2111.02974)
- B. Chazelle, *The Discrepancy Method*, Cambridge University Press, 2000. [author's page](https://www.cs.princeton.edu/~chazelle/pubs/book.pdf)
The Hardy-Littlewood Method I: Weyl's InequalityTextbook
## Motivation
The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their *Partitio Numerorum* series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer $n$ as a sum of $s$ terms drawn from a prescribed set — $k$-th powers, primes, values of a polynomial.
Its engine is an estimate for **exponential sums**. If a sum $\sum_{x<N} e(\alpha x^k)$, where $e(\theta)=\exp(2\pi i\theta)$, exhibits cancellation for every $\alpha$ not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate $k$.
A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent $2^{1-k}$, in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining $G(k)\le (k-2)2^{k-1}+5$ for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large $k$, reducing the bound to $O(k\log k)$; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small $k$ — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.
## Setting
For a real number $\theta$ write
$$e(\theta) \;=\; \exp(2\pi i \theta),$$
the standard additive character of $\mathbb{R}/\mathbb{Z}$: it satisfies $e(x+y)=e(x)e(y)$, $|e(x)|=1$, and $e(x)=1$ exactly when $x\in\mathbb{Z}$.
For a real number $\theta$ write $\|\theta\|$ for the distance from $\theta$ to the nearest integer. It is periodic with period $1$, vanishes exactly on $\mathbb{Z}$, satisfies the triangle inequality, and is at most $\tfrac12$.
Given a finite set $A\subseteq\mathbb{Z}$, its generating function is $f_A(\theta)=\sum_{a\in A}e(a\theta)$. The basic identity of the subject is
$$\int_0^1 f_A(\theta)^s\,e(-n\theta)\,d\theta \;=\; \#\{(a_1,\dots,a_s)\in A^s : a_1+\cdots+a_s=n\},$$
a consequence of the orthogonality relation $\int_0^1 e(m\theta)\,d\theta=[\,m=0\,]$.
A **Weyl sum** of degree $k$ is $\sum_{0\le x<N} e(\alpha x^k)$. The whole difficulty is to bound it for $\alpha$ in the *minor arcs* — those $\alpha$ admitting no rational approximation $a/q$ with $q$ small.
## Target
Fix $k\ge 2$. For every $\varepsilon>0$ there is a constant $C=C(k,\varepsilon)$ such that whenever $(a,q)=1$, $q\ge 1$, and $\left|\alpha-\frac{a}{q}\right|\le \frac{1}{q^2}$,
$$\left|\sum_{0\le x<N} e(\alpha x^{k})\right| \;\le\; C\,N^{1+\varepsilon}\left(\frac{1}{q}+\frac{1}{N}+\frac{q}{N^{k}}\right)^{2^{1-k}}.$$
The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, Hua's fourth-moment inequality for $k=2$, and the degree-two case of the inequality itself.
## Significance
*The result itself.* Weyl's inequality is what makes the minor arcs negligible. Applied with $q$ in the range $N^{\delta}\le q\le N^{k-\delta}$ it gives a power saving over the trivial bound $N$, and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.
*Formalizing it.* Mathlib currently contains the analytic prerequisites — Fourier characters on `AddCircle`, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: **53 theorems** covering the character $e$, the norm $\|\cdot\|$, the geometric sum bound $\left|\sum_{x<N}e(x\theta)\right|\le\min\!\left(N,\frac{1}{2\|\theta\|}\right)$, both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of $f_A$, are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.
## Difficulty
The obvious approach fails immediately. One would like to sum $\left|\sum_{x<N}e(\alpha x^k)\right|$ by comparing it to the linear case, where the geometric series gives $\min(N,\frac{1}{2\|\alpha\|})$ outright. But for $k\ge2$ the summand is not a geometric progression and there is no closed form.
Weyl's device is to square and difference: $\left|\sum_x e(\phi(x))\right|^2=\sum_{x,y}e(\phi(x)-\phi(y))$, and the substitution $y=x+h$ turns the inner polynomial into one of degree $k-1$ in $x$. Iterating $k-1$ times reduces to a linear sum, at the cost of raising the estimate to the power $2^{1-k}$ — which is why the saving is so weak for large $k$, and why Vinogradov's method eventually supersedes it.
The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not $[0,N)$ and must be handled uniformly; (ii) the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, needed to count the $h$ for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the $\varepsilon$-dependent constants through $k-1$ iterations without the informal $\ll$ notation.
## Formalization scope
Statements are given over the Prove2Me default environment (Lean `v4.30.0`, Mathlib `c5ea003`), in the shared namespace `CircleMethod`, and build on two published definitions: `CircleMethod_char` (the character `e` and the norm `nrm`) and `CircleMethod_genfun` (the generating function `f`).
Conventions this mission commits to:
- $\|\theta\|$ is `nrm θ = |θ - round θ|`. Mathlib's `round` breaks ties upwards, so `round` is *not* an odd function; the characterisation to use is minimality, `nrm θ ≤ |θ - n|` for every integer `n`, which is published as `CircleMethod.nrm_le`.
- Sums run over `Finset.range N`, that is $0\le x<N$, and $N$ is a natural number. Hypotheses `0 < N` and `0 < q` are stated explicitly rather than left implicit.
- Asymptotic notation is eliminated in favour of explicit existential constants: $X\ll_\varepsilon Y$ is rendered as `∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y`, with the constant quantified *outside* the parameters it may depend on and *inside* nothing else. Solvers should not weaken this by allowing $C$ to depend on $N$, $q$ or $\alpha$.
- Exponents such as $N^{1+\varepsilon}$ and $2^{1-k}$ are real powers (`Real.rpow`), not natural powers.
- Coprimality is `Nat.Coprime a.natAbs q`, which is the correct notion for a possibly negative numerator.
One trivialising formalization to rule out: the goal must not be read with $C$ permitted to depend on $N$, since then $C=N$ makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.
Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.
## Selected references
- H. Weyl, *Über die Gleichverteilung von Zahlen mod. Eins*, Mathematische Annalen 77 (1916), 313--352. [DOI:10.1007/BF01475864](https://doi.org/10.1007/BF01475864)
- G. H. Hardy and J. E. Littlewood, *Some problems of 'Partitio Numerorum' I--VI*, 1920--1928.
- R. C. Vaughan, *The Hardy--Littlewood Method*, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997. (Weyl's inequality is Lemma 2.4; the geometric sum bound is Lemma 2.1.)
- I. M. Vinogradov, *New estimates for Weyl sums*, Doklady Akademii Nauk SSSR 8 (1935), 195--198.
- T. D. Wooley, *Vinogradov's mean value theorem via efficient congruencing*, Annals of Mathematics 175 (2012), 1575--1627. [DOI:10.4007/annals.2012.175.3.12](https://doi.org/10.4007/annals.2012.175.3.12)
- J. Bourgain, C. Demeter and L. Guth, *Proof of the main conjecture in Vinogradov's mean value theorem for degrees higher than three*, Annals of Mathematics 184 (2016), 633--682. [DOI:10.4007/annals.2016.184.2.7](https://doi.org/10.4007/annals.2016.184.2.7)
Existence of complete sets of mutually unbiased basesOpen Problem
# Motivation
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, **Existence of complete sets of mutually unbiased bases**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
## Suggested attack route
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
## Formalization scope
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/16.html)
- [Durt et al., review of MUBs](https://arxiv.org/abs/1004.3348)
First-passage time of Brownian motion to an exponentially decaying boundaryOpen Problem
> **Submission hold — source-fidelity repair (2026-09-04).** The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
# Motivation
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, **First-passage time of Brownian motion to an exponentially decaying boundary**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
## Suggested attack route
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
## Formalization scope
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
## Milestones
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/13.html)
Markov Entanglement: Index Policies for Restless Bandits are Asymptotically SeparableResearch Paper
Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on *index policies* — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by *value decomposition*: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.
Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its *measure of Markov entanglement*, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.
The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its *configuration*: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.
The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.