## Motivation
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
## Setting and goal
For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.
## Relationship to the five-primes mission
The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as [Every Odd Number Greater Than 1 is the Sum of at Most Five Primes](https://prove2.me/missions/Every%20Odd%20Number%20Greater%20Than%201%20is%20the%20Sum%20of%20at%20Most%20Five%20Primes). The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.
## Formalization scope
The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.
## Proof approach
A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.
## Reference
H. A. Helfgott, [The ternary Goldbach conjecture is true](https://arxiv.org/abs/1312.7748), 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.
## Motivation
A number field $\mathbb{K}$ has a unit group $E = \mathcal{O}(\mathbb{K})^\times$ which, by Dirichlet's unit theorem, is free of $\mathbb{Z}$-rank $r_1 + r_2 - 1$ modulo roots of unity. Fix a prime $p$ and embed the units diagonally into the units of the completions of $\mathbb{K}$ at the primes above $p$. The topological closure of the image is a finite free a $\mathbb{Z}_p$-module modulo roots of unity, and its $\mathbb{Z}_p$-rank can in principle be smaller than $r_1 + r_2 - 1$: units that are independent over $\mathbb{Z}$ may become dependent $p$-adically. **Leopoldt's conjecture** asserts that this never happens.
The conjecture controls how many independent $\mathbb{Z}_p$-extensions a number field has. Iwasawa showed that if $\Omega(\mathbb{K})$ is the maximal $p$-abelian $p$-ramified extension of $\mathbb{K}$, then $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2 + 1 + \mathcal{D}_L(\mathbb{K})}$, where $\mathcal{D}_L(\mathbb{K})$ is the defect defined below. So a positive defect means extra $\mathbb{Z}_p$-extensions beyond the ones accounted for by the archimedean places, and for a totally real field it means a non-cyclotomic $\mathbb{Z}_p$-extension exists. Non-vanishing of the $p$-adic regulator is also what makes $p$-adic $L$-functions and $p$-adic class number formulas behave as their complex analogues do.
Timeline of what is actually proved, under which hypotheses:
- **1962** — Leopoldt conjectures non-vanishing of the $p$-adic regulator for abelian fields (H. Leopoldt, *Zur Arithmetik in Abelschen Zahlkörpern*, J. reine angew. Math. 209).
- **1965–1967** — Ax reduces the abelian case to a $p$-adic analogue of Baker's theorem on linear forms in logarithms; Baker proves the archimedean version; Brumer adapts it $p$-adically and proves the conjecture **for abelian extensions of $\mathbb{Q}$** (A. Brumer, *On the units of algebraic number fields*, Mathematika 14, 1967).
- **1976** — Greenberg relates the conjecture to a case of his own conjecture: Leopoldt for totally real fields implies the $T$-part of the relevant Iwasawa module is finite.
- **1981** — Waldschmidt proves the general bound $\mathcal{D}_L(\mathbb{K}) \le r/2$, where $r$ is the $\mathbb{Z}$-rank of the units: at least half of the expected $p$-adic rank is always attained.
- **1984, 1987–2007** — Emsalem–Kisilevsky–Wales settle some small non-abelian Galois groups by representation theory plus Baker theory; Jaulent handles fields of small discriminant.
- **2011–2016** — Mihăilescu posts a claimed proof for **all CM fields at odd $p$** (arXiv:1105.4544). It is currently an unpublished preprint, and its proof invokes a separate preprint asserting the vanishing of Iwasawa's $\mu$-invariant for cyclotomic $\mathbb{Z}_p$-extensions of CM fields, with an appendix that is said to avoid that assumption.
Beyond the abelian case the conjecture is open. This mission takes the CM claim as its target.
## Setting
Let $p$ be a prime and $\mathbb{K}$ a number field with ring of integers $\mathcal{O}(\mathbb{K})$ and units $E = \mathcal{O}(\mathbb{K})^\times$.
Let $P = \{\wp \subset \mathcal{O}(\mathbb{K}) : (p) \subset \wp\}$ be the set of primes above $p$, a finite set. For $\wp \in P$ write $\mathbb{K}_\wp$ for the completion and $\mathcal{O}_\wp$ for its valuation ring. Set
$$U \;=\; \prod_{\wp \in P} \mathcal{O}_\wp^{\times},$$
the group of **semilocal units** at $p$, and let
$$\iota : E \longrightarrow U$$
be the diagonal embedding, whose $\wp$-component is the completion map. Define the **$p$-adic closure of the global units**
$$\bar{E} \;=\; \bigcap_{n > 0} \iota(E) \cdot U^{p^n} \;\subseteq\; U ,$$
where $U^{p^n} = \{u^{p^n} : u \in U\}$ and the product of the two subgroups is taken inside the abelian group $U$. Finally, the **Leopoldt defect** of $\mathbb{K}$ at $p$ is
$$\mathcal{D}_L(\mathbb{K}) \;=\; \mathbb{Z}\text{-rk}(E) \;-\; \mathbb{Z}_p\text{-rk}(\bar{E}),$$
the difference between Dirichlet's unit rank $r_1 + r_2 - 1$ and the free $\mathbb{Z}_p$-rank of $\bar{E}$. The defect is always non-negative, and it is positive exactly when units that are independent over $\mathbb{Z}$ satisfy a $p$-adic relation after the diagonal embedding.
A number field $\mathbb{K}$ is **CM** when it is a totally complex quadratic extension of its maximal real subfield $\mathbb{K}^+$. For CM fields a positive defect is equivalent to the vanishing of the $p$-adic regulator of $\mathbb{K}$.
## Formalization targets
### Goal — Leopoldt's conjecture for CM fields at odd $p$
$$p \text{ odd prime}, \quad \mathbb{K}/\mathbb{Q} \text{ CM} \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) = 0 .$$
This is Theorem 1 of arXiv:1105.4544. It fixes no constants and no auxiliary choices, so it is stable under any later improvement of the argument.
### Supporting targets
$$\mathcal{D}_L(\mathbb{K}) = 0 \quad \text{for } \mathbb{K}/\mathbb{Q} \text{ abelian} \qquad \text{(Brumer, 1967)}$$
$$\mathcal{D}_L(\mathbb{K}) \le r/2, \quad r = \mathbb{Z}\text{-rk}(E) \qquad \text{(Waldschmidt, 1981)}$$
$$\mathcal{D}_L(\mathbb{F}) > 0 \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) > 0 \quad \text{for every finite } \mathbb{K}/\mathbb{F}$$
The last is Remark 1.A of the source, attributed there to Laurent: a defect is inherited by finite extensions, because the $p$-adic relations among $\mathbb{Z}$-generators of the units are preserved under the embedding of unit groups.
## Significance
*The result itself.* Leopoldt's conjecture for CM fields would pin down $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2+1}$ for every CM field and, via the totally real subfield, would rule out non-cyclotomic $\mathbb{Z}_p$-extensions of the totally real fields underlying them. It would remove a standing hypothesis from results in Iwasawa theory and $p$-adic $L$-functions that are currently stated conditionally on Leopoldt. Without it, the $\mathbb{Z}_p$-rank of the $p$-ramified Galois group is only known to lie in a range.
*Formalizing it.* Nothing in this area is formalized today. Mathlib has Dirichlet's unit theorem, the archimedean regulator, CM fields, and the completions of a number field at its finite places, but no $p$-adic regulator, no $p$-adic logarithm, and no Iwasawa theory. This mission first pins down a machine-checked statement of the conjecture itself — which is where the mathematical content of Theorem 1 sits, since the theorem is one sentence long — and then attacks it. Because the target is an unrefereed argument, a serious attempt to formalize it is also a test of it: a step that cannot be closed localizes a gap, and a milestone that turns out to be unprovable is itself the finding.
## Difficulty
The obvious approach is transcendence theory, and it is the one that works in the abelian case: a $p$-adic relation among units is a vanishing linear form in $p$-adic logarithms of algebraic numbers, and Baker-type lower bounds forbid it. This is exactly Ax's reduction and Brumer's theorem. It stalls immediately beyond abelian fields, because the argument needs units whose Galois structure is explicit — for abelian fields the cyclotomic units supply them, and in general nothing does. Waldschmidt's $\mathcal{D}_L \le r/2$ is the limit of what the transcendence route has delivered in general, and it has not been improved by that route. The source therefore abandons transcendence entirely and argues in Iwasawa theory, constructing a CM $\mathbb{Z}_p$-extension of a field where the conjecture is assumed to fail and deriving a contradiction from the classes of primes that split completely in it. That route needs the structure theory of $\Lambda$-modules, $\mu$- and $\lambda$-invariants, Tate cohomology of class group limits, and the vanishing of $\mu$ — none of which exists in Lean.
## Formalization scope
The development commits to the following conventions, all of them visible in the definition file.
$P$ is the subtype of height-one primes $\wp$ of $\mathcal{O}(\mathbb{K})$ with $p \in \wp$, and carries a `Finite` instance. $U$ is the dependent product over $P$ of the unit groups of the valuation rings `adicCompletionIntegers`, so it is a commutative topological group. $\bar{E}$ is defined by the intersection displayed above rather than as a topological closure: the source gives both descriptions, and the intersection is the one that needs no choice of topology on $\prod_\wp \mathbb{K}_\wp$. The two can differ by a finite subgroup, which does not affect the $\mathbb{Z}_p$-rank.
$\mathbb{Z}_p\text{-rk}(\bar{E})$ is defined as the largest $n \le [\mathbb{K}:\mathbb{Q}]$ for which $\mathbb{Z}_p^n$ admits a **continuous** injective homomorphism into $\bar{E}$. Continuity is not decoration: as abstract groups $\mathbb{Z}_p^n$ embeds into $\mathbb{Z}_p$ for every $n$, so the topological requirement is what makes the rank the intended one; and since $\mathbb{Z}_p^n$ is compact and $U$ is Hausdorff, such an injection is automatically a closed embedding. For a closed subgroup of $U$, which is isomorphic to a finite group times $\mathbb{Z}_p^d$, such injections exist exactly for $n \le d$. The cut-off at $[\mathbb{K}:\mathbb{Q}]$ is carried only so that the supremum ranges over a visibly bounded set of naturals rather than falling back on a junk value; since the $\mathbb{Z}_p$-rank of the whole semilocal unit group $U$ is already $[\mathbb{K}:\mathbb{Q}]$, it never binds.
The defect subtracts in $\mathbb{N}$, hence truncates. Since the $\mathbb{Z}_p$-rank never exceeds the $\mathbb{Z}$-rank, truncation is never triggered and $\mathcal{D}_L(\mathbb{K}) = 0$ is equivalent to the two ranks being equal.
One trivializing formalization is worth ruling out. The goal is not vacuous: it is neither provable nor refutable by unfolding the definitions, and it has genuine content whenever $\mathbb{Z}\text{-rk}(E) > 0$, that is for every CM field other than the imaginary quadratic ones, where Dirichlet's rank is $0$ and the statement is trivially true.
A complete development needs, beyond what Mathlib supplies: the $p$-adic logarithm on the units of a local field and the resulting $p$-adic regulator; the Iwasawa algebra acting on inverse limits of $p$-class groups along a $\mathbb{Z}_p$-extension, with $\mu$- and $\lambda$-invariants and the decomposition of Definition 1 of the source; CM $\mathbb{Z}_p$-extensions; and Tate cohomology of these modules. All of that is reusable well beyond this mission — it is the missing foundation of Iwasawa theory in Lean. Contributions of any of these pieces as definitions, and of the three supporting targets as theorems, are welcome independently of the goal.
## Selected references
- P. Mihăilescu, *On CM $\mathbb{Z}_p$-extensions and the Leopoldt conjecture for CM fields*, arXiv:1105.4544 (2011–2016). https://arxiv.org/abs/1105.4544
- H. Leopoldt, *Zur Arithmetik in Abelschen Zahlkörpern*, J. reine angew. Math. 209 (1962), 54–71. https://doi.org/10.1515/crll.1962.209.54
- A. Brumer, *On the units of algebraic number fields*, Mathematika 14 (1967), 121–124. https://doi.org/10.1112/S0025579300003703
- J. Ax, *On the units of an algebraic number field*, Illinois J. Math. 9 (1965), 584–589. https://doi.org/10.1215/ijm/1256059299
- A. Baker, *Linear forms in the logarithms of algebraic numbers I, II, III*, Mathematika 13–14 (1966–67).
- M. Waldschmidt, *Transcendance et exponentielles en plusieurs variables*, Invent. Math. 63 (1981), 97–127. https://doi.org/10.1007/BF01389194
- M. Emsalem, H. Kisilevsky, D. Wales, *Indépendance linéaire sur $\overline{\mathbb{Q}}$ de logarithmes $p$-adiques de nombres algébriques et rang $p$-adique du groupe des unités d'un corps de nombres*, J. Number Theory 19 (1984), 384–391. https://doi.org/10.1016/0022-314X(84)90040-1
- R. Greenberg, *On the Iwasawa invariants of totally real fields*, Amer. J. Math. 98 (1976), 263–284. https://doi.org/10.2307/2373625
- K. Iwasawa, *On $\mathbb{Z}_\ell$-extensions of number fields*, Ann. of Math. 98 (1973), 246–326. https://doi.org/10.2307/1970784
- M. Laurent, *Rang $p$-adique d'unités et action de groupes*, J. reine angew. Math. 399 (1989), 81–108. https://doi.org/10.1515/crll.1989.399.81
The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is $[c_F,\infty)$, where
$$
c_F=\frac{2221564096+283748\sqrt{462}}{491993569}
=4.527829566160879\ldots.
$$
The formalization must establish membership of every real number at least $c_F$, including the endpoint, and show that no half-line starting below $c_F$ is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
### Source material
- [Proof report (PDF)](https://drive.google.com/file/d/13jj7vJy-OtTsJIe_vp4Qd1PaUIeoLt8f/view?usp=sharing) — the complete argument, exact certificate appendices and corrected English translation of Freiman's Russian text. [Download PDF](https://drive.google.com/uc?export=download&id=13jj7vJy-OtTsJIe_vp4Qd1PaUIeoLt8f).
- [Verification package (ZIP)](https://drive.google.com/file/d/18AWfMKCJ0XPfRs2k6c_hf0ovbljaPL2u/view?usp=sharing) — the report, its LaTeX sources, the Russian source, certificate data, verification programs and reproduction instructions. [Download ZIP](https://drive.google.com/uc?export=download&id=18AWfMKCJ0XPfRs2k6c_hf0ovbljaPL2u).
Start with `README.md` and `PROOF_GUIDE.md` in the package. The files `formalization/MISSION.md` and `formalization/MILESTONES.md` describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
## Motivation
An **elliptic curve** over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the **rank**. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The **Birch and Swinnerton-Dyer conjecture** predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, [*The Birch and Swinnerton-Dyer Conjecture*](https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf) (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
**Timeline.**
- 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901).
- 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function.
- 1965: B. Birch and H. P. F. Swinnerton-Dyer, [*Notes on elliptic curves II*](https://doi.org/10.1515/crll.1965.218.79), state the conjecture, found experimentally on the EDSAC computer.
- 1977: J. Coates and A. Wiles, [*On the conjecture of Birch and Swinnerton-Dyer*](https://doi.org/10.1007/BF01402975): for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite.
- 1986: B. Gross and D. Zagier, [*Heegner points and derivatives of L-series*](https://doi.org/10.1007/BF01388809): for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order.
- 1989–1990: V. Kolyvagin, [*Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*](https://doi.org/10.1070/IM1989v032n03ABEH000779): for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty).
- 1995–2001: A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118559)), R. Taylor and A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118560)), and C. Breuil, B. Conrad, F. Diamond and R. Taylor ([J. Amer. Math. Soc. 14](https://doi.org/10.1090/S0894-0347-01-00370-8)): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$.
- 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem.
- 2014: M. Bhargava, C. Skinner and W. Zhang, [*A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*](https://arxiv.org/abs/1407.1826): the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open.
## Setting
A **Weierstrass equation** over $\mathbb{Q}$ is
$$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$
with discriminant $\Delta$; in Lean, `WeierstrassCurve ℚ`. It is an **elliptic curve** when $\Delta \ne 0$ (Mathlib's typeclass `IsElliptic`). Its **rational points** $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (`W.toAffine.Point`). The **rank** is the rank of this group as a $\mathbb{Z}$-module,
$$r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$$
the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$.
The **Hasse–Weil $L$-series** is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is *minimal at $p$* (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (**good reduction**). The local factor is
$$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$
and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's `WeierstrassCurve.LSeries W s`, defined by exactly this recipe (`WeierstrassCurve.LFunction` is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's `LSeries` takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there.
An **$L$-function of $E$** is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (`BSD.IsLFunction W Λ`). By the identity theorem there is at most one; by modularity there is exactly one. The **order of vanishing** of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, `analyticOrderAt Λ 1`, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$.
## Formalization targets
### Goal: the Birch and Swinnerton-Dyer conjecture (`BSD.birch_swinnerton_dyer`)
For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that
$$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$
This is Wiles' *Conjecture (Birch and Swinnerton-Dyer)*: $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open.
### Weaker target: the weak conjecture (`BSD.weak_birch_swinnerton_dyer`)
There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open.
### Milestones: what Wiles lists as known
1. **Mordell's theorem** (`BSD.mordell`): $E(\mathbb{Q})$ is a finitely generated abelian group.
2. **Convergence of the $L$-series** (`BSD.lSeriesSummable`): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$."
3. **Analytic continuation** (`BSD.exists_isLFunction`): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.
4. **Gross–Zagier–Kolyvagin** (`BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one`): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds."
A bridging lemma, `BSD.isLFunction_unique`, records that an $L$-function of $E$ is unique when it exists.
## Significance
*The result itself.* The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions.
*Formalizing it.* None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named `birch_swinnerton_dyer` are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step `WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex` (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and `WeierstrassCurve.modularity_of_semistableModel` from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to `WeierstrassCurve.LSeries` would give milestone 3 for semistable curves.
## Difficulty
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
## Formalization scope
- $E$ is any `WeierstrassCurve ℚ` with `IsElliptic` ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.
- The rank is `Module.finrank ℤ W.toAffine.Point`: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's `finrank` is $0$, a case milestone 1 excludes.
- The $L$-series is Mathlib's `WeierstrassCurve.LSeries`, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. `BSD.IsLFunction` constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique.
- The order of vanishing is `analyticOrderAt Λ 1 : ℕ∞`; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$.
*No trivializing formalization.* The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without `IsElliptic` the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative.
*Out of scope.* The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$.
*Infrastructure needed and welcome contributions.* Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's `WeierstrassCurve.LSeries` to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about `WeierstrassCurve.LFunction` (its values at primes, multiplicativity, independence of the model) are welcome.
## Selected references
- A. Wiles, *The Birch and Swinnerton-Dyer Conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf
- B. J. Birch, H. P. F. Swinnerton-Dyer, *Notes on elliptic curves II*, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79
- L. J. Mordell, *On the rational solutions of the indeterminate equations of the third and fourth degrees*, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192.
- J. Coates, A. Wiles, *On the conjecture of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975
- B. H. Gross, D. B. Zagier, *Heegner points and derivatives of L-series*, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809
- V. A. Kolyvagin, *Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779
- A. Wiles, *Modular elliptic curves and Fermat's Last Theorem*, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
- R. Taylor, A. Wiles, *Ring-theoretic properties of certain Hecke algebras*, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
- C. Breuil, B. Conrad, F. Diamond, R. 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
- J. B. Tunnell, *A classical Diophantine problem and modular forms of weight 3/2*, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327
- M. Bhargava, C. Skinner, W. Zhang, *A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*, 2014. https://arxiv.org/abs/1407.1826
- J. H. Silverman, *The Arithmetic of Elliptic Curves*, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6
Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem
## Motivation
An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The **obstacle number** asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.
The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$, have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.
## Setting
A finite simple graph $G$ has a **$k$-obstacle drawing** when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that
$$
uv\in E(G)
\quad\Longleftrightarrow\quad
[p(u),p(v)]\text{ meets no obstacle}.
$$
Graph vertices lie outside every obstacle. The **ordinary obstacle number** $\operatorname{obs}(G)$ is the least such $k$. The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.
The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.
## Formalization targets
### The two-part OPG record
The source records both
$$
\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1
$$
and
$$
\exists k\in\mathbb N\ \forall\text{ finite planar }H,
\ \operatorname{obs}(H)\le k.
$$
The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.
### Published first part
A milestone formalizes the stronger published statement
$$
\exists\text{ finite planar }G,
\qquad \operatorname{obs}(G)\le2
\quad\text{and}\quad
\operatorname{obs}(G)\not\le1.
$$
This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.
### Universal bound
The open milestone asks for a single natural number $k$, chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.
## Significance
The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.
Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.
## Difficulty
A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.
Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$.
## Formalization scope
All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.
The repository's fixed-placement polygonization argument and finite arrangement code are `candidate_only`. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.
## Selected references
- L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, *Graphs with Obstacle Number Greater than One*, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
- J. Gimbel, P. Ossona de Mendez, and P. Valtr, *Obstacle Numbers of Planar Graphs*, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
- M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, *Bounding and Computing Obstacle Numbers of Graphs*, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
- Open Problem Garden / UnsolvedMath, *OPG-37357*. https://www.unsolvedmath.com/problems/OPG-37357
Clique Partitions of Chordal Graphs (Erdos Problem 81)Open Problem
## Motivation
An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.
Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.
## Setting
A finite simple graph is **chordal** when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.
An **edge partition into cliques** is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$. Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.
The asymptotic notation
$$
\frac{n^2}{6}+O(n)
$$
means that there are constants $C>0$ and $n_0\ge1$, chosen independently of $G$ and $n$, such that every chordal $n$-vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.
## Formalization targets
### Erdős Problem 81
The root theorem is
$$
\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\
\forall G\text{ chordal on }n\text{ vertices},
\qquad
\operatorname{cp}(G)\le \frac{n^2}{6}+Cn.
$$
The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.
### Leading-coefficient milestone
The supporting target records the weaker uniform statement
$$
\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\
\forall G\text{ chordal on }n\text{ vertices},
\qquad
\operatorname{cp}(G)\le
\left(\frac16+\varepsilon\right)n^2.
$$
This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$.
## Significance
The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$. It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.
Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.
## Difficulty
Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$.
The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$.” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$.
## Formalization scope
Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.
The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is `candidate_only`, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.
## Selected references
- P. Erdős, E. T. Ordman, and Y. Zalcstein, *Clique Partitions of Chordal Graphs*, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
- P. E. Haxell and V. Rödl, *Integer and Fractional Packings in Dense Graphs*, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
- R. Yuster, *Integer and fractional packing of families of graphs*, 2003. https://arxiv.org/abs/math/0305350
- Erdős Problems, *Problem 81*. https://www.erdosproblems.com/81
Weak Pentagon Colorings of Triangle-Free Cubic Graphs (OPG-434)Open Problem
## Motivation
The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.
Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.
## Setting
Let $G$ be a finite simple triangle-free cubic graph. A **five-edge coloring** here is any symmetric assignment
$$
c:E(G)\longrightarrow\{1,2,3,4,5\}.
$$
It need not be proper or surjective. For a color $i$, delete all edges with label $i$ while retaining every vertex. The coloring is a **weak-pentagon coloring** when each of the five resulting spanning graphs is bipartite.
Equivalently, each color class is an **odd-cycle edge transversal**: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.
A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.
## Formalization targets
### Weak pentagon conjecture
The root target is
$$
\forall G\text{ finite, simple, triangle-free, and cubic},
\qquad
\exists c:E(G)\to[5]\ \forall i\in[5],
\quad G-c^{-1}(i)\text{ is bipartite}.
$$
No condition is imposed on adjacent edges receiving different labels.
### Odd-cycle equivalence
For every fixed graph and fixed five-edge labeling,
$$
\bigl(\forall i,\ G-c^{-1}(i)\text{ is bipartite}\bigr)
\quad\Longleftrightarrow\quad
\bigl(\forall i,\ c^{-1}(i)\text{ meets every odd cycle of }G\bigr).
$$
This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.
### Sixteen-vertex homomorphism formulation
For every finite simple graph $G$,
$$
G\text{ has a weak-pentagon coloring}
\quad\Longleftrightarrow\quad
G\longrightarrow H_{16},
$$
where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.
## Significance
The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.
Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.
## Difficulty
The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.
High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.
## Formalization scope
Colors are `Fin 5`. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.
The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are `candidate_only`; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.
## Selected references
- R. Šámal, *Weak pentagon problem*, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
- M. DeVos and R. Šámal, *High-girth cubic graphs are homomorphic to the Clebsch graph*, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
- P. Kolman, B. Lidický, and J.-S. Sereni, *On Minimum Fair Odd Cycle Transversal*, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
- Open Problem Garden / UnsolvedMath, *OPG-434*. https://www.unsolvedmath.com/problems/OPG-434
Two Acyclic Colors for Planar Orientations (OPG-169)Open Problem
## Motivation
The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.
Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.
## Setting
Let $G$ be a finite simple planar graph. An **orientation** $D$ assigns exactly one direction to every edge of $G$, with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$, the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$.
A two-coloring is a map
$$
c:V(D)\longrightarrow\{0,1\}.
$$
It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.
Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.
## Formalization targets
### Two Color Conjecture
The goal is
$$
\forall D\text{ an orientation of a finite simple planar graph},
\qquad
\exists c:V(D)\to\{0,1\},
\quad D[c^{-1}(0)]\text{ and }D[c^{-1}(1)]\text{ are acyclic}.
$$
Disconnected graphs and empty color classes are included.
### Least-order counterexample structure
A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:
$$
D\text{ least-order counterexample}
\quad\Longrightarrow\quad
D\text{ strongly connected and }\delta(U(D))\ge3.
$$
The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.
### Semidegree candidate
A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains `candidate_only`.
## Significance
The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.
The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.
## Difficulty
Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.
Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.
## Formalization scope
A directed graph is a binary relation, coupled to a `SimpleGraph` by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.
The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.
Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.
## Selected references
- Open Problem Garden / UnsolvedMath, *OPG-169: The Two Color Conjecture*. https://www.unsolvedmath.com/problems/OPG-169
- B. Mohar, *Eigenvalues and colorings of digraphs*, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
- Z. Li and B. Mohar, *Planar digraphs of digirth four are 2-colourable*, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114
## Motivation
The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, [*Existence and smoothness of the Navier–Stokes equation*](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.
**Timeline.**
- 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
- 1934: Jean Leray, [*Sur le mouvement d'un liquide visqueux emplissant l'espace*](https://doi.org/10.1007/BF02547354) (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global *weak* solutions with finite energy always exist. Their smoothness and uniqueness are left open.
- 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph [*The Mathematical Theory of Viscous Incompressible Flow*](https://archive.org/details/mathematicaltheo0000lady), 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
- 1984: Tosio Kato, [*Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$*](https://doi.org/10.1007/BF01174182) (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
- 1976–1998: partial regularity. Scheffer, then [Caffarelli, Kohn and Nirenberg](https://doi.org/10.1002/cpa.3160350604) (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
- 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.
## Setting
Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is `NavierStokes.Vec n`. A **velocity field** assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A **pressure** is a real function $p(x,t)$. The **viscosity** $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).
For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the **divergence** is
$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$
in Lean `NavierStokes.div`, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The **Laplacian** $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The **gradient** $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is `NavierStokes.gradNormSq`.
**Admissible initial data** (Fefferman's condition (4), `NavierStokes.IsInitialData`): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,
$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$
In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.
A **physically reasonable solution** on a set $S$ of times (`NavierStokes.IsSolutionOn`; $S = [0,\infty)$ for `NavierStokes.IsSolution`) is a pair $(u,p)$ such that
1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,
$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$
3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.
## Formalization targets
### Goal: Fefferman's statement (A)
Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:
$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).$$
This is `NavierStokes.existence_and_smoothness_R3`. It is open; a proof would settle the Millennium Prize Problem in the affirmative.
### Milestones: what Fefferman lists as known
1. **Local existence** (`NavierStokes.local_existence_R3`): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. **Global existence for small data** (`NavierStokes.small_data_global_existence_R3`): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with
$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$
Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies.
3. **The two-dimensional case** (`NavierStokes.existence_and_smoothness_R2`): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."
A bridging lemma, `NavierStokes.isInitialData_iff_schwartz`, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.
## Significance
*The result itself.* Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."
*Formalizing it.* None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.
## Difficulty
The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is *supercritical*: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.
The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.
## Formalization scope
- $\mathbb{R}^n$ is `EuclideanSpace ℝ (Fin n)` with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
- A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
- Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's `ContDiffOn` of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
- Derivatives are Mathlib's total functions (`fderiv`, `deriv`, `iteratedFDeriv`, `gradient`, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
- The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
- No normalization is imposed on the pressure, as in Fefferman's text.
*No trivializing formalization.* The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.
*Infrastructure needed and welcome contributions.* The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the `NavierStokes` namespace, decompositions of the milestones, and Mathlib lemmas about `ContDiffOn` on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.
## Selected references
- C. L. Fefferman, *Existence and smoothness of the Navier–Stokes equation*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
- J. Leray, *Sur le mouvement d'un liquide visqueux emplissant l'espace*, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
- O. A. Ladyzhenskaya, *The Mathematical Theory of Viscous Incompressible Flow*, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
- T. Kato, *Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions*, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
- L. Caffarelli, R. Kohn, L. Nirenberg, *Partial regularity of suitable weak solutions of the Navier–Stokes equations*, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
- A. J. Majda, A. L. Bertozzi, *Vorticity and Incompressible Flow*, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
- J. C. Robinson, J. L. Rodrigo, W. Sadowski, *The Three-Dimensional Navier–Stokes Equations: Classical Theory*, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143
Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper
## Motivation
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in *Algorithmica* in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$-regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a `ResearchPaper` mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
## Setting
For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$, the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$. The cut is **nontrivial** when both shores are nonempty. It is a **matching cut** when each vertex is incident with at most one crossing edge. A graph is called **immune** in the cited paper when it has no matching cut.
The **girth** is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$-regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A **perfect matching** pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
## Formalization targets
### Lemma 5 — immune high-girth graphs
The main theorem follows the paper's structural lemma:
$$
\forall g\ge3\ \exists G,
\quad G\text{ is finite, connected, bipartite, and $14$-regular},
$$
$$
\operatorname{girth}(G)\ge g,
\qquad
G\text{ has no matching cut},
\qquad
G\text{ has a perfect matching}.
$$
The graph may depend on $g$. The existence quantifier does not request an efficient algorithm or a numerical order bound.
### Negative OPG consequence
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
$$
\forall g\ge3\ \exists G,
\qquad
\overline d(G)=14<15,
\quad \operatorname{girth}(G)\ge g,
\quad G\text{ has no matching cut}.
$$
Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$.
## Significance
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$, Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$. Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
## Difficulty
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
## Formalization scope
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$, so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are `candidate_only` and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
## Selected references
- C. Feghali, F. Lucke, D. Paulusma, and B. Ries, *Matching Cuts in Graphs of High Girth and H-Free Graphs*, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
- C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
- A. Lubotzky, R. Phillips, and P. Sarnak, *Ramanujan graphs*, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
- Open Problem Garden, *Matching cut and girth*. https://www.openproblemgarden.org/op/matching_cut_and_girth
## Motivation and history
The **Collatz conjecture**, also called the **$3x+1$ problem**, asks whether one elementary
iteration rule has the same long-term behavior for every positive integer. It belongs to
number theory and discrete dynamical systems: the rule is deterministic and trivial to
compute for any fixed input, but no argument is known that controls every orbit. The problem
has served as a test case for methods involving congruences, stopping times, probabilistic
models, computation, and arithmetic dynamics. Jeffrey Lagarias's survey, *The $3x+1$ Problem
and Its Generalizations*, organized much of the classical theory and explains why strong
results about large classes of starting values do not settle the universal statement
([Lagarias 1985](https://websites.umich.edu/~lagarias/3x%2B1.html)).
The problem has a long record of partial results. By 1985, the literature already included
results on stopping-time densities, possible cycles, and divergent trajectories, summarized
by Lagarias. In 2019, Terence Tao proved that for every function $f(N)$ tending to infinity,
the minimum value attained by the orbit of $N$ is at most $f(N)$ for almost all positive
integers $N$, where “almost all” is measured using logarithmic density
([Tao 2019](https://arxiv.org/abs/1909.03562)). This is a strong statement about typical
orbits, but it does not cover every starting value. Computational verification has also been
pushed to very large finite ranges; David Barina describes algorithms and verification
methods for this task in *Convergence Verification of the Collatz Problem*
([Barina 2021](https://doi.org/10.1007/s11227-020-03368-x)). A finite verification bound,
regardless of size, leaves all larger starting values outside its scope.
## Setting
For a natural number $n$, define the **Collatz step** $C(n)$ by
$$
C(n)=
\begin{cases}
n/2, & \text{if } n \text{ is even},\\
3n+1, & \text{if } n \text{ is odd}.
\end{cases}
$$
Write $C^m(n)$ for the result of applying $C$ exactly $m$ times, with $C^0(n)=n$.
The forward orbit of $n$ is therefore
$$
n,\ C(n),\ C^2(n),\ C^3(n),\ldots.
$$
The familiar orbit beginning at $6$, for example, starts
$6,3,10,5,16,8,4,2,1$. Reaching $1$ is the relevant event; after that point the
usual map continues around the cycle $1,4,2,1$.
## Formalization target
The mission goal is the universal assertion
$$
\forall n\in\mathbb N,\quad n>0\Longrightarrow
\exists m\in\mathbb N,\quad C^m(n)=1.
$$
The existential index $m$ may be zero, so the case $n=1$ is included directly. The
hypothesis $n>0$ excludes $0$, whose behavior under the total natural-number definition of
$C$ is irrelevant to the conjecture.
The goal is the existing public prove2.me theorem `collatz_conjecture`, rather than a new
copy. Its statement follows the Collatz declaration in the
[Formal Conjectures collection](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean).
## Significance
A proof would classify every positive-integer orbit with respect to reaching $1$. It would
simultaneously rule out an orbit that escapes forever without visiting $1$ and any nontrivial
cycle disjoint from $1$. Partial density results and finite computations establish neither
universal exclusion.
The formalization goal is to make the universal quantifiers, parity split, finite iteration,
and boundary cases explicit in Lean 4. Supporting contributions can isolate reusable facts
about iterates, stopping times, accelerated odd-only maps, residue classes, and finite
certificates. Such components may also support formal work on related piecewise-affine
integer dynamical systems, while every contribution remains tied to a precisely stated
theorem.
## Difficulty
Individual trajectories can be computed, and many families of inputs can be reduced by
elementary parity arguments, but the map combines contraction and expansion. Even steps
halve the current value, while odd steps replace it by the larger value $3n+1$. Local
information about a bounded initial segment of an orbit does not supply a uniform bound on
all later values or on the time required to reach $1$.
Statistical control of most inputs also leaves exceptional inputs unresolved. Likewise,
excluding cycles up to a finite length does not exclude longer cycles, and checking all
inputs below a finite threshold does not constrain every larger input. The mission therefore
requires statements whose quantifiers genuinely cover all positive natural numbers; a large
finite computation or an almost-everywhere theorem cannot by itself close the goal.
## Formalization scope
The existing Lean statement works over `ℕ`. Its local `collatzStep` definition branches on
the proposition that $n$ is even, uses natural-number division by $2$ on the even branch,
and uses $3n+1$ on the odd branch. Iteration is represented by the standard finite function
iterate notation. The theorem quantifies over a positive starting value $n$ and asserts the
existence of a finite iterate index $m$ at which the value is exactly $1$.
The positivity hypothesis is essential: the total function sends $0$ to $0$, so including
$0$ would make the universal statement false. The mission does not replace the universal
quantifier by a fixed numerical bound, and it does not encode a predetermined stopping-time
limit. A complete solution must account for every positive starting value.
Useful supporting formalizations include exact relations between the classical and
accelerated maps, composition laws for finite iteration, stopping-time predicates, cycle
exclusion statements, descent criteria, and checked finite ranges. Each supporting theorem
should state its own hypotheses and trust boundary explicitly. Computational artifacts are
welcome when their finite scope is stated precisely and their result is connected to a Lean
consumer through a checked certificate or another accepted verification boundary.
## Selected references
- Jeffrey C. Lagarias, *The $3x+1$ Problem and Its Generalizations*, American Mathematical
Monthly 92 (1985), 3–23. https://websites.umich.edu/~lagarias/3x%2B1.html
- Terence Tao, *Almost All Orbits of the Collatz Map Attain Almost Bounded Values*, 2019;
published in Forum of Mathematics, Pi 10 (2022). https://arxiv.org/abs/1909.03562
- David Barina, *Convergence Verification of the Collatz Problem*, The Journal of
Supercomputing 77 (2021), 2681–2688. https://doi.org/10.1007/s11227-020-03368-x
- Google DeepMind, *Formal Conjectures: Collatz Conjecture*, Lean 4 statement.
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean
Formalization of the Poincaré ConjectureResearch Paper
**Our goal**
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's [Notes on Perelman's Papers](https://arxiv.org/abs/math/0605667).
**Important references**
[Poincare-Conjecture](https://github.com/frenzymath/Poincare-Conjecture) and [DifferentialGeometry](https://github.com/qinz1yang/differential-geometry) are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
**OpenGA's role**
[OpenGA](https://github.com/MathNetwork/OpenGA) focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The `PoincareConjecture` directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
## Motivation
Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a **magic state**, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the **stabilizer rank** -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few *unconditional* obstructions to classical simulation available at all.
A timeline of what is established for the standard magic state $|H\rangle$:
- **2016.** Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$, hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$, and prove a lower bound of order $\sqrt{n}$.
- **2020.** Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$, such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ ([arXiv link](https://doi.org/10.1109/TIT.2020.3004427)).
- **2022.** Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank ([arXiv:2106.03214](https://arxiv.org/abs/2106.03214)).
- **2024.** A quadratic lower bound is obtained for the approximate stabilizer rank ([arXiv:2305.10277](https://arxiv.org/abs/2305.10277)).
Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.
## Setting
Index the computational basis of an $n$-qubit system by bit strings $x\in\{0,1\}^n$, so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$.
The **Pauli operators** are $X^aZ^b$ for $a,b\in\{0,1\}^n$, acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$, where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the **Pauli group** is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$. A unitary $U$ is a **Clifford unitary** when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$, and a **stabilizer state** is a vector $U|0\cdots0\rangle$ for some Clifford $U$. There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.
The **stabilizer rank** $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$.
The **magic state** is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$, and $|H^{\otimes n}\rangle$ its $n$-fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$.
## Target
The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with
$$\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},$$
equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$.
Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.
## Significance
*The result itself.* A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a *polynomial* upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$, and via postselection $\mathrm{P}=\mathrm{NP}$. There is also a purely classical payoff -- improving the known bound even to super-*linear* would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$, resolving a separate open question.
*Formalizing it.* The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$-qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.
## Difficulty
Counting settles the problem for *random* states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$, which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.
The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.
## Formalization scope
State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are **not** required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$. The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by-$H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.
One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$; if no decomposition existed the rank would be $0$ for every state and the goal would be *false* rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$.
A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.
## Selected references
- S. Peleg, A. Shpilka, B. L. Volk, *Lower Bounds on Stabilizer Rank*, Quantum 6 (2022) 652; [arXiv:2106.03214](https://arxiv.org/abs/2106.03214).
- S. Bravyi, G. Smith, J. Smolin, *Trading Classical and Quantum Computational Resources*, Phys. Rev. X 6 (2016) 021043; [arXiv:1506.01396](https://arxiv.org/abs/1506.01396).
- C. Huang, M. Newman, M. Szegedy, *Explicit Lower Bounds on Strong Quantum Simulation*, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
- *Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach*, STOC 2024; [arXiv:2305.10277](https://arxiv.org/abs/2305.10277).
## Motivation
Quantum query algorithms are known to beat classical ones on problems with algebraic
structure -- period finding, hidden subgroups, forrelation. No such speedup is known for
a problem with no structure at all. **Aaronson and Ambainis** proposed making that
observation into a theorem, and reduced it to a question with no quantum content: a
statement about bounded low-degree polynomials on the Boolean cube
([Aaronson--Ambainis 2009](https://arxiv.org/abs/0911.0996)).
The question has resisted since. A timeline of what is actually established:
- **2009.** Aaronson and Ambainis state the conjecture and prove that it implies
almost-everywhere classical simulation of quantum query algorithms.
- **2012.** Montanaro settles the case of block-multilinear forms whose coefficients all
have the same magnitude.
- **2016.** O'Donnell and Zhao reduce the general conjecture to a restricted class,
the one-block decoupled polynomials.
- **2019.** Aaronson surveys a decade of partial progress
([retrospective](https://scottaaronson.blog/?p=4414)).
- **2022.** Bansal, Sinha and de Wolf prove the conjecture for *completely bounded*
degree-$d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at
constant variance ([arXiv:2203.00212](https://arxiv.org/abs/2203.00212)).
- **2024.** The conjecture is established for a non-negligible fraction of random
restrictions ([arXiv:2402.13952](https://arxiv.org/abs/2402.13952)).
The cases that are settled are settled under structural hypotheses -- block-multilinearity,
complete boundedness, symmetry, Boolean range. The general statement is open.
## Setting
Let $N$ be a positive integer. The **Boolean cube** is $\{0,1\}^N$, carrying the uniform
distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real
multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a
function $f$ on the cube write
$$\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).$$
The **variance** of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$.
Writing $x^{\oplus i}$ for $x$ with its $i$-th bit flipped, the **influence** of coordinate
$i$ on $p$ is
$$\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].$$
These are the combinatorial forms of both quantities, as used in the source; no
Fourier--Walsh expansion is required to state anything below. The **degree** of $p$ is its
total degree as a polynomial. Call $p$ **bounded** when $0\le p(x)\le 1$ at every cube
point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$.
## Target
The goal is the conjecture in the shape stated by its authors: there is an absolute
constant $C$ such that for all $N$, all $d$, every polynomial $p$ of degree at most $d$
that is bounded on the cube, and every $\varepsilon>0$ with
$\operatorname{Var}[p]\ge\varepsilon$, some coordinate $i$ satisfies
$$\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.$$
The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the
entire content: bounds that degrade exponentially in $d$ are already known, and a goal
naming a specific exponent would be superseded by the next improvement.
## Significance
*The result itself.* Aaronson and Ambainis prove that the conjecture implies that the
acceptance probability of any bounded-error $T$-query quantum algorithm on a Boolean input
can be approximated, to small error on all but a small fraction of inputs, by a classical
algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure
in a precise sense. The conjecture also has purely classical content, asserting that
boundedness plus low degree forces variance to concentrate on some single coordinate rather
than spread across all $N$. Without it, no such concentration is known at any rate
polynomial in $1/d$.
*Formalizing it.* The conjecture is open, so this mission does not formalize a known proof
of the goal. What it produces is a machine-checked statement of the conjecture together with
formalizations of the partial results above, each currently existing only on paper. The
milestone chain also yields reusable infrastructure for analysis of Boolean functions, of
which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no
variance on the cube.
## Difficulty
The elementary bound is the Poincare inequality on the cube,
$4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$, which yields a coordinate with
influence at least $4\varepsilon/N$. This is tight for the dictator $p(x)=x_1$ and depends
on $N$, so it says nothing: the conjecture demands a bound free of $N$ entirely.
The natural repair is the route available when $p$ takes only the values $0$ and $1$. A
Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which
immediately produces an influential one. That argument does not survive relaxing the range
to the interval $[0,1]$: a bounded real-valued polynomial of low degree need not depend on
boundedly many coordinates, and every known substitute loses a factor exponential in $d$.
Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and
it is where all of the partial results stop.
## Formalization scope
Polynomials are `MvPolynomial (Fin N) ℝ` and degree is Mathlib's `totalDegree`, so the
statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$
rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping
is `Function.update x i (!x i)`. Boundedness is asserted at cube points only. Variance and
influence are the combinatorial definitions above, published as the definition
`AaronsonAmbainis`.
Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as
an existentially quantified natural number with no leading multiplicative constant, since
admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at
least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the
bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The
hypothesis $\deg p\le d$ is universally quantified over $d$, which is equivalent to the
source's exact-degree form because the smallest admissible $d$ gives the strongest
conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$
fails for a constant polynomial.
A complete development needs, beyond the published definitions, a Fourier--Walsh layer with
Parseval's identity, the level-$k$ machinery used by the partial results, and -- for the
completely bounded case -- operator-space norms on multilinear forms. All of the
Boolean-analysis material is reusable well beyond this mission. Contributions of any
milestone are welcome, as are alternative formalizations of the definitions in
function-level rather than polynomial-level form.
Out of scope: the quantum simulation consequence is not formalized here. Stating it requires
a formal quantum query model, which no Lean library currently provides.
## Selected references
- S. Aaronson, A. Ambainis, *The Need for Structure in Quantum Speedups*, Theory of Computing 10 (2014) 133--166; [arXiv:0911.0996](https://arxiv.org/abs/0911.0996). Conjecture 6.
- N. Bansal, M. Sinha, R. de Wolf, *Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms*, CCC 2022; [arXiv:2203.00212](https://arxiv.org/abs/2203.00212).
- *Aaronson--Ambainis Conjecture Is True For Random Restrictions*, 2024; [arXiv:2402.13952](https://arxiv.org/abs/2402.13952).
- S. Aaronson, *The Aaronson-Ambainis Conjecture (2008-2019)*, [blog retrospective](https://scottaaronson.blog/?p=4414).
- S. Arunachalam, J. Briet, C. Palazuelos, *Quantum query algorithms are completely bounded forms*, SIAM J. Comput. 48 (2019); [arXiv:1711.07285](https://arxiv.org/abs/1711.07285).
- AIM problem list, *Analysis on the hypercube with applications to quantum computing*, [aimpl.org/hypercubequantum](http://aimpl.org/hypercubequantum/1/).
## Motivation
A polynomial $f \in \mathbb{Q}[x]$ is **split** if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.
Say $\alpha$ is **$k$-collapsible** if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, **collapsible** if it is $1$-collapsible, and **eventually collapsible** if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of *eventual* collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and **degree $3$ is open**. That one-step cubic case is this mission's goal.
## Setting
Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a **depressed cubic**
$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$
with **discriminant** $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is *totally real* (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as
$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$
and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant
$$\tau = e^2/d^3$$
determines the problem up to scaling: the search space is one rational parameter, not two.
## Formalization targets
### Goal — every cubic algebraic number is collapsible
$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$
This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
### Supporting targets
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
1. the **product criterion** — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. **affine invariance**, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two **sufficient conditions**: square discriminant, and the power-family condition subsuming it;
4. three **obstructions**: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.
The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
## Significance
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are **not** proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.
## Difficulty
The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces
$$\deg f \ \ge\ \pi/\psi.$$
As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.
## Formalization scope
**Representation.** `IsSplit f` says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. `Collapsible α` is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.
**Ruling out a trivialisation.** `Collapsible` places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
**Conventions in the archimedean milestones.** In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.
In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.
**Infrastructure.** A complete development needs `Polynomial`, `Multiset`, `minpoly`, and for the archimedean bound `Real.arctan`, `Complex.arg`, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.
## Selected references
- Griffin Macris, *List of open problems*, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
- Miles, *Collapsible algebraic numbers*, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.
## Motivation
A positive integer is **perfect** when it equals the sum of its proper divisors: $6 = 1 + 2 + 3$, $28 = 1 + 2 + 4 + 7 + 14$, then $496$, $8128$, and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.
The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if $2^p - 1$ is prime then $2^{p-1}(2^p - 1)$ is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.
A timeline of what is actually proved about a hypothetical odd perfect number $N$:
- **Euler** (published posthumously in 1849): $N = p^k m^2$ with $p$ prime, $p \equiv k \equiv 1 \pmod 4$, and $p \nmid m$. In particular $N$ is not a perfect square.
- **Servais (1887), Sylvester (1888)**: lower bounds on the number $\omega(N)$ of distinct prime divisors; Sylvester obtained $\omega(N) \ge 5$, and $\omega(N) \ge 8$ when $3 \nmid N$.
- **Touchard (1953)**: $N \equiv 1 \pmod{12}$ or $N \equiv 9 \pmod{36}$. Shorter proofs were later given by Satyanarayana (1959) and Holdener (2002).
- **Chein (1979) and Hagis (1980)**, independently: $\omega(N) \ge 8$; Nielsen (2007): $\omega(N) \ge 9$; Nielsen (2015): $\omega(N) \ge 10$.
- **Nielsen (2003)**: an upper bound in terms of $\omega$, namely $N < 2^{4^{\omega(N)}}$ — the first bound of its kind, later sharpened by Nielsen himself.
- **Ochem–Rao (2012)**: $N > 10^{1500}$; **Ochem–Rao (2014)**: $N$ has at least $101$ prime factors counted with multiplicity.
None of these results, alone or together, rules out an odd perfect number.
## Setting
For $n \ge 1$ write $\sigma(n) = \sum_{d \mid n} d$ for the sum of all positive divisors of $n$. Then $n$ is **perfect** exactly when
$$\sigma(n) = 2n,$$
equivalently when the divisors of $n$ other than $n$ itself sum to $n$. The function $\sigma$ is **multiplicative**: $\sigma(ab) = \sigma(a)\sigma(b)$ whenever $\gcd(a,b) = 1$, and $\sigma(p^a) = 1 + p + \cdots + p^a$ for a prime power. The quantity $\sigma(n)/n$ is the **abundancy index** of $n$, so a perfect number is one of abundancy index exactly $2$.
Write $\omega(n)$ for the number of distinct prime divisors of $n$. In Lean, $\omega(n)$ is `n.primeFactors.card`, and perfection is Mathlib's `Nat.Perfect n`, which unfolds to `∑ i ∈ n.properDivisors, i = n ∧ 0 < n` — the positivity clause is part of the definition, so $n = 0$ is not perfect.
## Formalization targets
### Goal
$$\forall n \in \mathbb{N}, \quad \sigma(n) = 2n \ \Longrightarrow\ 2 \mid n.$$
Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.
### Milestones
The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number $N$:
$$N = p^k m^2, \quad p \text{ prime}, \quad p \equiv k \equiv 1 \ (\mathrm{mod}\ 4), \quad p \nmid m \qquad \text{(Euler)}$$
$$N \text{ is not a perfect square} \qquad \text{(Euler)}$$
$$\omega(N) \ge 3, \qquad \omega(N) \ge 5 \qquad \text{(Servais, Sylvester)}$$
$$N \equiv 1 \ (\mathrm{mod}\ 12) \quad \text{or} \quad N \equiv 9 \ (\mathrm{mod}\ 36) \qquad \text{(Touchard)}$$
$$N < 2^{4^{\omega(N)}} \qquad \text{(Nielsen)}$$
## Significance
*The result itself.* A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be $2^{p-1}(2^p-1)$ for a Mersenne prime $2^p - 1$. A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than $1500$ decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of $\sigma$, and about the multiperfect numbers.
*Formalizing it.* Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (`Archive/Wiedijk100Theorems/PerfectNumbers.lean`, as `Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect` and `Theorems.perfect_iff_even_and_mersenne`), and the main library carries the divisor-sum API around `Nat.Perfect` in `Mathlib/NumberTheory/Divisors.lean`, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing $\sigma$-arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of $\sigma$ on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.
## Difficulty
The obvious approach — take Euler's form $N = p^k m^2$ and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation $\sigma(N) = 2N$ has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing $\omega$ weakens the constraints rather than strengthening them, which is why the lower bounds on $\omega$ have advanced by one prime factor per decade at very high computational cost. The upper bound $N < 2^{4^{\omega(N)}}$ makes the search space finite for each fixed $\omega$, but astronomically so.
## Formalization scope
The development is stated over `ℕ` with Mathlib's `Nat.Perfect`, so positivity is built into the hypothesis and no separate `0 < n` assumption appears. Oddness is `Odd n`, the number of distinct prime divisors is `n.primeFactors.card`, and Euler's form is stated with explicit residues `p % 4 = 1`, `k % 4 = 1`, together with `¬ p ∣ m` and `n = p ^ k * m ^ 2`. No custom definitions are introduced; everything rests on Mathlib's `Nat.sigma` / `Nat.Perfect` API.
One caution on the shape of the milestones. Each is stated conditionally, for an $n$ assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved *unconditionally* in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.
Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for $\sigma$ on odd numbers. Sharper published bounds — larger values of $\omega$, the improved Nielsen bound $N < 2^{4^{\omega(N)} - 2^{\omega(N)}}$, the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.
## Selected references
- L. Euler, *De numeris amicabilibus*, Commentationes arithmeticae 2 (1849), 627–636.
- J. J. Sylvester, *Sur les nombres parfaits*, Comptes Rendus de l'Académie des Sciences CVI (1888), 403–405.
- J. Touchard, *On prime numbers and perfect numbers*, Scripta Mathematica 19 (1953), 35–39.
- J. A. Holdener, *A theorem of Touchard on the form of odd perfect numbers*, American Mathematical Monthly 109 (2002), 661–663.
- P. P. Nielsen, *An upper bound for odd perfect numbers*, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14.
- P. P. Nielsen, *Odd perfect numbers have at least nine distinct prime factors*, Mathematics of Computation 76 (2007), 2109–2126.
- P. P. Nielsen, *Odd perfect numbers, Diophantine equations, and upper bounds*, Mathematics of Computation 84 (2015), 2549–2567.
- P. Ochem and M. Rao, *Odd perfect numbers are greater than $10^{1500}$*, Mathematics of Computation 81 (2012), 1869–1877.
- P. Ochem and M. Rao, *On the number of prime factors of an odd perfect number*, Mathematics of Computation 83 (2014), 2435–2439.
- Overview and further pointers: https://en.wikipedia.org/wiki/Perfect_number
Monochromatic Reachability in Three-Colored Tournaments (OPG-1808)Open Problem
## Motivation
Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.
The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly `candidate_only`: it is bounded search evidence, not a proof of the unrestricted theorem.
## Setting
A **tournament** is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.
A **rainbow directed triangle** is a cyclically oriented triangle
$$
a\to b\to c\to a
$$
whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.
A vertex $s$ is a **monochromatic source** when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.
The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.
## Formalization targets
### Root theorem
For every nonempty finite tournament $T$ with a three-coloring of its arcs,
$$
T\text{ has a rainbow directed triangle}
\quad\lor\quad
\exists s\in V(T)\ \forall t\in V(T),\
\text{$s$ reaches $t$ monochromatically}.
$$
No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.
### Finite order milestone
The first milestone freezes the exact bounded claim supported by the replay package:
$$
1\le |V(T)|\le 11\text{ and no rainbow directed triangle}
\quad\Longrightarrow\quad
T\text{ has a monochromatic source}.
$$
The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.
## Significance
The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.
The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.
## Difficulty
The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.
The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.
## Formalization scope
Lean represents the tournament as a binary relation `D` with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.
The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.
## Selected references
- Open Problem Garden, *Monochromatic reachability versus rainbow triangles*, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
- B. Sands, N. Sauer, and R. Woodrow, *On monochromatic paths in edge-coloured digraphs*, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
- A. Georgakopoulos and P. Sprüssel, *On 3-coloured tournaments*, 2009. https://arxiv.org/abs/0904.1967
- A. Trygub, *Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles*, 2023. https://arxiv.org/abs/2304.14579
Circular (20,7)-Coloring of Triangle-Free Subcubic Planar Graphs (OPG-401)Open Problem
## Motivation
Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio $20/7$.
The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.
## Setting
For integers $p\ge 2q>0$, a **$(p,q)$-coloring** of a finite simple graph $G$ is a map
$$
\varphi:V(G)\longrightarrow \mathbb Z_p
$$
such that the shortest cyclic distance between $\varphi(u)$ and $\varphi(v)$ is at least $q$ for every edge $uv$. Equivalently, using representatives in $\{0,\ldots,p-1\}$, the modular difference lies between $q$ and $p-q$, inclusive. The **circular chromatic number** is the infimum of the ratios $p/q$ for which such a coloring exists.
The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.
## Formalization targets
### Root question
The central target is
$$
G\text{ finite, simple, planar, triangle-free, and }\Delta(G)\le 3
\quad\Longrightarrow\quad
G\text{ has a }(20,7)\text{-coloring}.
$$
This is exactly the claim $\chi_c(G)\le 20/7$ in a form suitable for finite Lean data.
### Local extension table
A reusable finite milestone freezes the local palette arithmetic. For $a\in\mathbb Z_{20}$, let $A(a)$ be the colors at cyclic distance at least seven from $a$. For all $a,b$,
$$
|A(a)\cap A(b)|=7-d_{20}(a,b),
\qquad
A(a)\cap A(b)\ne\varnothing\iff d_{20}(a,b)\le6.
$$
This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only `candidate_only`; the mission publishes the statement as an open formal target rather than claiming it as proved.
## Significance
A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.
Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.
## Difficulty
The obvious induction on vertices fails at degree two. A coloring of $G-v$ need not extend over $v$: if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of $G-v$ has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.
A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield $(20,7)$-colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.
## Formalization scope
Lean represents colors by `Fin 20` and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound $7$ and the formal upper bound $13$. Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.
The definition bundle contains no theorem and no `sorry`. Draft theorem items contain exactly one `:= by sorry`. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.
## Selected references
- X. Zhu, *Circular chromatic number of triangle-free planar graphs with maximum degree three*, open-problem page. https://www.math.nsysu.edu.tw/~zhu/open-problems/chic-k3free-planar.htm
- Open Problem Garden, *OPG-401*. https://www.unsolvedmath.com/problems/OPG-401
- X. Zhu, *The fractional version of Hedetniemi's conjecture is true*, European Journal of Combinatorics, 2011. https://doi.org/10.1016/j.ejc.2011.03.004
- Z. Dvořák, J.-S. Sereni, and J. Volec, *Subcubic triangle-free graphs have fractional chromatic number at most 14/5*, Journal of the London Mathematical Society, 2014. https://arxiv.org/abs/1301.5296
Diaz's modulus conjecture: if |u| is algebraic, e^u is transcendentalOpen Problem
**If $|u|$ is algebraic and $u \neq 0$, is $e^{u}$ transcendental?** Guy Diaz asked this in 2004 and it is still open. Note it is $e^{u}$, not $e^{|u|}$ — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that $u$ itself may be transcendental while only its modulus is constrained.
## The question
Write $\bar{\mathbb{Q}}$ for the algebraic numbers in $\mathbb{C}$ and
$$\mathcal{L}=\{u\in\mathbb{C}\ :\ e^{u}\in\bar{\mathbb{Q}}^{\times}\}$$
for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of $\mathcal{L}$ has algebraic modulus. He states it as
> « Soit $u \in \mathbb{C}\setminus\{0\}$ avec $|u| \in \bar{\mathbb{Q}}$ ; alors $\mathrm{e}^{u}$ est transcendant. »
The statement fits on one line and needs no machinery beyond $\exp$ and $|\cdot|$. It has been open for twenty-two years.
It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.
## Why it suits a distributed platform
The mission decomposes into work that can be done **now**, without any open input.
Two milestones are *conditional* theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all `Prop`-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.
A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where $u$ and $\bar u$ are $\mathbb{Q}$-linearly dependent.
The remaining two milestones are classical theorems that the platform's Mathlib does not have: **Hermite--Lindemann** and the **six exponentials theorem**. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.
Only the top node needs genuinely new transcendence.
One structural remark that shapes the whole ladder: **Hermite--Lindemann is a special case of the goal**, not just an input to it. If $a \neq 0$ is algebraic then $|a|^{2} = a\bar a$ is algebraic, hence so is $|a|$, and the goal applied to $u := a$ gives that $e^{a}$ is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.
## Timeline
| | |
|---|---|
| 1873, 1882 | Hermite, then Lindemann: $e^{a}$ is transcendental for algebraic $a \neq 0$. In particular every non-zero element of $\mathcal{L}$ is itself transcendental, so a counterexample $u$ would be a transcendental number with algebraic modulus and algebraic exponential. |
| 1934--35 | Gelfond and Schneider settle Hilbert's seventh problem. |
| 1966 | Lang's *Introduction to Transcendental Numbers* records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The **four** exponentials conjecture stays open, and still is. |
| 1966 | Baker's theorem on linear forms in logarithms. |
| 1997 | Diaz studies the companion condition $\lvert\tau\rvert^{2}\in\mathbb{Q}$, assertion (4-1), p. 237. |
| 2000 | Waldschmidt's *Diophantine Approximation on Linear Algebraic Groups* states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with $y_1 = \lambda$, $y_2 = \lvert\lambda\rvert$ at p. 15. |
| 2004 | Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps $z \mapsto \bar z$ and $z \mapsto \lvert z\rvert$ enter a transcendence proof at all? |
| 2026 | A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched. |
## What is known not to work
For a candidate $u$ one has $u\bar u = |u|^{2}$ with $|u|^{2}$ algebraic, hence
$$\bar u = \frac{|u|^{2}}{u}.$$
So $\bar u$ is not independent data: complex conjugation on $\bar{\mathbb{Q}}(u)$ is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at <https://github.com/carlok/diaz-modulus-lean>: a ring homomorphism fixing $\bar{\mathbb{Q}}$ and carrying $u$ to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over $\bar{\mathbb{Q}} \oplus \bar{\mathbb{Q}}u \oplus \bar{\mathbb{Q}}\bar u$ separates a candidate from an ordinary complex number placed on the same circle.
The practical consequence for solvers: **accumulating algebraic relations between $u$ and $\bar u$ until they collide cannot settle this.** A successful attack has to introduce information that is not a rational function of $u$ over $\bar{\mathbb{Q}}$ — which is precisely Diaz's own methodological question, still open.
## Mathlib gaps a solver will meet
- **Hermite--Lindemann is not in Mathlib.** Only the analytic half is present, in `Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean` — verified in all three of the platform's pinned revisions (`0df444a3`, `c5ea0035`, `777aaa61`), none of which contains `transcendental_exp`. Hence the choice to carry it as a `Prop` and give it its own milestone rather than assume it. There is an open PR, [leanprover-community/mathlib4#28013](https://github.com/leanprover-community/mathlib4/pull/28013) (*feat: Lindemann-Weierstrass Theorem*, opened 2025-08-05, label `awaiting-author` as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.
- **Neither Schanuel nor any four-exponentials statement exists in any form.** They are defined in the mission's bundle; that is the point, since the tractable content of this mission is what follows *from* them.
- **`Algebra.trdeg` has almost no computational API.** It is cardinal-valued, with transcendence bases and `lift_cardinalMk_eq_trdeg`, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if $S \subseteq K(t)$ with $t$ transcendental over $K$ then $\operatorname{trdeg}_K K[S] \le 1$". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.
## Sources
- G. Diaz, *Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle*, J. Théor. Nombres Bordeaux **16** (2004), no. 3, 535–553, [doi:10.5802/jtnb.459](https://doi.org/10.5802/jtnb.459) — the conjecture is §5.1, p. 550; the methodological question is p. 551.
- G. Diaz (1997) — the companion condition $|\tau|^{2}\in\mathbb{Q}$ is assertion (4-1), p. 237.
- M. Waldschmidt, *Diophantine Approximation on Linear Algebraic Groups*, Grundlehren der mathematischen Wissenschaften **326**, Springer 2000 — pp. 15, 399, 614, and Exercise 15.16.
- S. Lang, *Introduction to Transcendental Numbers*, Addison-Wesley 1966, Ch. 2 (six exponentials, Schanuel's conjecture).
- A. Baker, *Transcendental Number Theory*, Cambridge University Press 1975, Theorem 1.4 (Hermite--Lindemann).
Six Colors for Star Edge-Coloring Subcubic Graphs (OPG-37271)Open Problem
## Motivation
A **star edge coloring** is a proper edge coloring with an additional local restriction: no path or cycle of four edges may use only two colors. It sits between ordinary proper edge coloring and strong edge coloring. The problem is local enough to admit finite obstruction searches, but global enough that independently valid local colorings may fail to fit together.
Dvořák, Mohar, and Šámal proved in 2013 that every subcubic multigraph has a star edge coloring with seven colors and conjectured that six always suffice. The Open Problem Garden records the simple-graph version as [OPG-37271](https://www.openproblemgarden.org/comment/reply/37271). The value six would be best possible because the complete bipartite graph $K_{3,3}$ has star chromatic index six.
Subsequent work has proved the six-color bound under additional hypotheses. Lei, Shi, and Song proved it for subcubic multigraphs with maximum average degree less than $5/2$ and obtained a five-color result below $24/11$. Casselgren, Granholm, and Raspaud proved the conjecture for cubic Halin graphs and several bipartite families. These results leave the unrestricted finite subcubic case as the target of this mission.
## Setting
Let $G$ be a finite simple undirected graph. An edge coloring assigns to each unordered edge of $G$ one color from a finite palette. It is **proper** if two distinct edges incident with the same vertex always have different colors.
A simple path of four edges has five pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ and consecutive edges $v_0v_1,v_1v_2,v_2v_3,v_3v_4$. It is bichromatic in a proper coloring exactly when the first and third edges have the same color and the second and fourth edges have the same color. The path need not be induced: additional chords do not remove it. A four-cycle has four pairwise distinct vertices and is bichromatic under the analogous alternating equalities, including the closing edge.
A coloring is a **star edge coloring** when it is proper and contains neither type of bichromatic four-edge configuration. The star chromatic index $\chi'_s(G)$ is the least palette size admitting such a coloring. A graph is **subcubic** when every vertex has at most three neighbors.
## Formalization targets
### Goal — the six-color conjecture
The main target is the exact OPG-37271 assertion for finite simple graphs:
$$
\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 6.
$$
In the Lean statement, this is expressed directly as the existence of a coloring by `Fin 6`; no separate minimization operator is needed.
### Known upper bound
The first literature milestone is the established seven-color theorem:
$$
\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 7.
$$
Formalizing this result provides a checked baseline and infrastructure that a six-color argument can reuse.
### Sharpness at $K_{3,3}$
The second literature milestone records both sides of the exact value
$$
\chi'_s(K_{3,3})=6.
$$
Thus the mission cannot be completed by weakening the goal to a larger universal constant.
## Significance
A proof would determine the universal star chromatic-index bound for graphs of maximum degree three and would match the known lower-bound example $K_{3,3}$. A counterexample, if one exists, would separate six from the established seven-color bound and identify the first genuinely seven-chromatic subcubic graph.
The formalization contributes a reusable definition of star edge coloring on Mathlib finite simple graphs. In particular, it fixes several conventions that are easy to blur in informal or computational work: forbidden paths have four edges rather than four vertices; they are simple but need not be induced; four-cycles are checked separately; and properness is not inferred merely from the absence of an alternating four-edge pattern. These definitions can support certified bounded searches, verified coloring certificates, and later formalizations of sparse or planar special cases.
The current research repository contains candidate-only local extension criteria and finite certificates. They may motivate future milestones, but they are not treated here as proofs of the conjecture, as admitted evidence, or as replacements for the literature milestones.
## Difficulty
A direct greedy coloring argument can fail at a newly inserted edge because a color may be forbidden either by an adjacent edge or by a bichromatic four-edge path created several incidences away. Deleting a low-degree vertex and coloring the remaining graph therefore does not guarantee that the old coloring extends without recoloring. Explicit small configurations already witness failure of this zero-recoloring strategy while remaining globally six-colorable.
The known seven-color proof has one extra color available to break such interactions. Reaching six requires coordinating local recolorings or extracting stronger structure from a minimal counterexample. Finite searches can test configurations and produce certificates, but bounded verification alone cannot establish the universal quantifier over all finite graphs.
## Formalization scope
The mission uses `SimpleGraph` with an arbitrary finite vertex type. Edges are unordered edge-set elements, and palettes are the labeled finite types `Fin k`. The graph need not be connected, cubic, planar, or nonempty; isolated vertices and the empty graph are included. “Subcubic” means degree at most three, not degree exactly three.
A forbidden path is represented by five pairwise distinct vertices and four consecutive adjacencies. It is not required to be induced. A forbidden cycle is represented separately by four pairwise distinct vertices and four cyclic adjacencies. Under the properness hypothesis, equality of opposite edge colors is precisely the bichromatic alternating pattern.
A complete development should supply the known seven-color theorem, certify the exact value for $K_{3,3}$, and then address the six-color goal. Contributions formalizing faithful special cases or reusable extension lemmas are welcome, but sampled graph families and successful SAT searches remain finite evidence unless converted into a general Lean proof.
## Selected references
- Z. Dvořák, B. Mohar, and R. Šámal, *Star chromatic index*, Journal of Graph Theory 72 (2013), 313–326. [arXiv:1011.3376](https://arxiv.org/abs/1011.3376)
- H. Lei, Y. Shi, and Z.-X. Song, *Star chromatic index of subcubic multigraphs*, Journal of Graph Theory 88 (2018), 566–576. [arXiv:1701.04105](https://arxiv.org/abs/1701.04105)
- C. J. Casselgren, J. B. Granholm, and A. Raspaud, *On star edge colorings of bipartite and subcubic graphs*, Discrete Applied Mathematics 298 (2021), 21–33. [arXiv:1912.02467](https://arxiv.org/abs/1912.02467)
- Open Problem Garden, *Star chromatic index of subcubic graphs*, OPG-37271. [Problem page](https://www.openproblemgarden.org/comment/reply/37271)
- Vibe Mathing candidate repository, *OPG-37271 star chromatic index of subcubic graphs*, candidate-only artifacts at commit `ddc49c1978a196490702150bb75264793a658457`. [Repository](https://github.com/vibemathing/problem-opg-37271-star-chromatic-index-cubic/tree/ddc49c1978a196490702150bb75264793a658457)
P3-Partitions of Cubic 3-Connected Graphs (OPG-46613)Open Problem
## Motivation
A **$P_3$-packing** in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.
A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of [*Packing 3-vertex Paths in Cubic 3-connected Graphs*](https://arxiv.org/abs/0910.2766v2), the question is whether every cubic 3-connected graph $G$ satisfies $\lambda(G)=\lfloor |V(G)|/3\rfloor$. Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. [OPG-46613](https://www.unsolvedmath.com/problems/OPG-46613) records the divisible-order form targeted here.
A 2026 candidate analysis in the [Vibe Mathing problem repository](https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition) investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a $P_3$-factor. Candidate C02 gives an explicit proposed family $H_q$ of order $18+12q$ that has $P_3$-factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.
## Setting
All graphs are finite and simple. A graph is **cubic** when every vertex has exactly three neighbors. It is **3-vertex-connected** here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.
A **$P_3$-factor** is represented by a natural number $b$, together with a bijection
$$
\operatorname{Fin}(b)\times\operatorname{Fin}(3)\simeq V(G),
$$
such that, in every block, positions $0$ and $1$ are adjacent and positions $1$ and $2$ are adjacent. The path is not required to be induced: an ambient edge between positions $0$ and $2$ is allowed because the two selected path edges still form a copy of $P_3$.
A **2-factor** is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A **divisible matching complement** is a perfect matching $M$ such that the relative complement $G\setminus M$ is a divisible 2-factor.
The explicit graph $H_q$ is defined on $\operatorname{Fin}(18+12q)$. Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.
## Formalization targets
### Main goal
For every finite simple graph $G$,
$$
\bigl(G\text{ cubic}\bigr)\land
\bigl(G\text{ 3-vertex-connected}\bigr)\land
3\mid |V(G)|
\quad\Longrightarrow\quad
G\text{ has a }P_3\text{-factor}.
$$
This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.
### Literature and route milestones
The mission also formalizes the $(z1)\Leftrightarrow(z8)$ part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a $P_3$-factor. Two route lemmas state that divisible 2-factors split into $P_3$-factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.
### Candidate boundary milestones
The C02 milestones ask first for the complete 18-vertex statement and then for the full family:
$$
\forall q\in\mathbb N,\quad
H_q\text{ is cubic and 3-vertex-connected, has a }P_3\text{-factor, and has no divisible matching complement}.
$$
This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every $H_q$ in the proposed family explicitly satisfies the desired $P_3$ conclusion.
## Significance
A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a $P_3$-factor; the C02 family does not claim this.
Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced $P_3$-factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.
## Difficulty
The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated $P_3$-factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.
The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to $G$ on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and $P_3$ must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.
## Formalization scope
The development targets Lean 4.33.1 and Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. Graphs use `SimpleGraph` on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.
The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The $H_q$ family includes $q=0$. The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in `sorry`; the shared definition module itself is sorry-free.
Welcome contributions include proofs of the model lemmas, the finite $H_0$ statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.
## Selected references
- A. Kelmans, *Packing 3-vertex Paths In Cubic 3-connected Graphs*, arXiv:0910.2766v2, 2011, Problem 1.10 (p. 3) and Theorem 3.1 (pp. 7–8). https://arxiv.org/abs/0910.2766v2
- UnsolvedMath, *OPG-46613: P3-partitions of cubic 3-connected graphs*. https://www.unsolvedmath.com/problems/OPG-46613
- Vibe Mathing, *C01: divisible-cycle implication and a 30-vertex obstruction*, fixed repository revision `14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a`. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md
- Vibe Mathing, *C02: an 18-vertex obstruction and an infinite family with P3-factors*, fixed repository revision `14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a`. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md
## Motivation: when pairwise square conditions limit a set
**Diophantine equations** ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.
The paper [*There is no Diophantine quintuple*](https://arxiv.org/abs/1610.04020v2), by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.
## Setting: positive integers and pairwise perfect squares
A **perfect square** is an integer of the form $r^2$ for a natural number $r$. A **Diophantine $m$-tuple** is a set of $m$ distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here $m$ records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members ([definition in Section 1](https://arxiv.org/html/1610.04020v2#S1)).
Write those five integers as $a_1,\ldots,a_5$. Positivity means $a_i>0$ for every index. Distinctness means $a_i\ne a_j$ whenever $i\ne j$. The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.
The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.
## Formalization target: no Diophantine quintuple
The single goal is the following nonexistence statement:
$$
\nexists\,a_1,\ldots,a_5\in\mathbb Z_{>0}\quad
\left[
(\forall i\ne j,\ a_i\ne a_j)
\ \land\
(\forall\,1\le i<j\le5,\ \exists r_{ij}\in\mathbb N,\ a_i a_j+1=r_{ij}^{,2})
\right].
$$
This is [Theorem 1 of the paper](https://arxiv.org/abs/1610.04020v2). The mission's goal is the existing declaration [`no_diophantine_quintuple`](https://prove2.me/theorems/780bea2d-21a2-4653-82ae-842b3c4a1927).
The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.
## Significance: an exact obstruction to larger sets
The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.
A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.
## Difficulty: the quantifier over all positive integers
Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.
The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's [proof overview in Section 2](https://arxiv.org/html/1610.04020v2#S2) describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.
## Formalization scope: five indexed natural numbers
The Lean declaration represents the entries by a function `a : Fin 5 → Nat`. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.
The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.
The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.
## Selected references
- Bo He, Alain Togbé, and Volker Ziegler, *There is no Diophantine quintuple*, arXiv preprint, 2016; revised 2018, arXiv:1610.04020v2. [Paper](https://arxiv.org/abs/1610.04020v2). The target is Section 1, Theorem 1; the definition precedes it, and Section 2 gives the proof overview.
Every Odd Number Greater Than 1 is the Sum of at Most Five PrimesResearch Paper
## Motivation
An additive question about the primes asks how many of them are needed to represent
every integer. **Shnirelman's constant** is the least $k$ such that every natural number
greater than $1$ is a sum of at most $k$ primes; that such a $k$ exists at all is
Shnirelman's theorem (1930). The even Goldbach conjecture would give $k = 3$, and is
close to equivalent to that claim, but Goldbach is open, so every bound on $k$ has come
from the circle method together with explicit numerical input.
The history is a sequence of shrinking bounds, each one effective and each one resting on
a numerical verification available at the time:
* **1937.** Vinogradov proves that every *sufficiently large* odd integer is a sum of
three primes, with no effective threshold
([Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)).
* **1956.** Borozdkin makes the threshold effective; later work reduces it, and Liu and
Wang bring it to $\exp(3100)$
([Liu–Wang, 2002](https://doi.org/10.4064/aa105-2-3)).
* **1995.** Ramaré proves that every even natural number is a sum of at most six primes,
giving Shnirelman's constant $k \le 7$
([Ramaré](http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/)).
* **1995.** Kaniecki obtains "at most five primes" **under the Riemann hypothesis**
([Kaniecki](https://doi.org/10.4064/aa-72-4-361-374)).
* **2012.** Tao removes the hypothesis: every odd number greater than $1$ is a sum of at
most five primes, unconditionally, lowering Shnirelman's constant to $k \le 6$
([arXiv:1201.6656](https://arxiv.org/abs/1201.6656)). This mission's goal.
* **2013.** Helfgott proves the ternary Goldbach conjecture outright — every odd
$n > 5$ is a sum of three primes — which supersedes the statement above
([arXiv:1312.7748](https://arxiv.org/abs/1312.7748)). Neither result is formalized.
## Setting
For a real number $\theta$ write $e(\theta) = \exp(2\pi i\theta)$. The **von Mangoldt
function** $\Lambda(n)$ equals $\log p$ when $n = p^m$ is a prime power and $0$
otherwise; it is Mathlib's `ArithmeticFunction.vonMangoldt`.
The paper does not work with the sharp-cutoff exponential sum
$S(x,\alpha) = \sum_{n \le x} \Lambda(n)e(\alpha n)$ but with a **smoothed** variant. For
a piecewise smooth $\eta : \mathbb{R} \to \mathbb{C}$ and a modulus $q_0$, set
$$S_{\eta,q_0}(x,\alpha) \;:=\; \sum_{n} \Lambda(n)\,e(\alpha n)\,
\mathbf{1}_{(n,q_0)=1}\,\eta(n/x).$$
The modulus $q_0$ is a technical device: taking $q_0 = 2$ restricts the sum to odd $n$
and saves a factor of two in the explicit constants. Because of that restriction it is
$4\alpha$, not $\alpha$, that gets approximated by a rational $a/q$.
Two explicit cutoffs are fixed. The **Lipschitz cutoff**
$$\eta_0(t) := 4\big(\log 2 - |\log 2t|\big)_+$$
has unit mass and is supported on $[1/4, 1]$; it is chosen because it factorises the Type
II sums. The **$L^2$-normalised cutoff**
$$\eta_1(t) := \big(1 - 10\,\mathrm{dist}(t,[0.2,0.8])\big)_+$$
is supported on $[0.1,0.9]$ and symmetric, $\eta_1(1-t) = \eta_1(t)$.
Throughout, $O^*(Y)$ denotes a quantity of magnitude at most $Y$ — an explicit bound, not
an asymptotic one. Two numerical constants are fixed once and for all:
$T_0 := 3.29\times 10^9$ and $N_0 := 4\times 10^{14}$.
## Formalization targets
### Goal (Theorem 1.4)
$$\forall n \text{ odd},\ n > 1 \;\Longrightarrow\;
\exists\, p_1,\dots,p_k \text{ prime},\ k \le 5,\ n = p_1 + \cdots + p_k.$$
The goal fixes no constants and no thresholds, so no later improvement can invalidate it.
The milestone list is the paper's own attack path, in its numbering: the two numerical
verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that
together settle $n \le 8.7\times10^{36}$; the $L^2$ apparatus (Lemma 4.4, Proposition
4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1)
and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis
(Proposition 7.2); and the circle-method core (Theorem 8.2).
## Significance
*The result itself.* Theorem 1.4 lowers Shnirelman's constant from $7$ to $6$ and removes
the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content,
however, is not the headline but the **explicit exponential sum estimate** of Theorem
1.3: a bound on $|S_{\eta_0,q_0}(x,\alpha)|$ with constants small enough to be useful for
$x$ between $10^{30}$ and $10^{1300}$, a range where the asymptotically superior estimates
of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to
apply. That estimate is the reusable object; it has been improved since
([Helfgott–Platt](https://arxiv.org/abs/1305.3062)) but not superseded in method.
*Formalizing it.* Status honesty matters here. Theorem 1.4 is **closed mathematics**, and
as a *statement* it was superseded within a year by Helfgott's ternary Goldbach theorem,
which gives three primes for every odd $n > 5$ and hence five a fortiori. Neither Tao's
theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be
attacking an open problem: the work is formalizing a known, fully explicit proof. That
proof happens to be an unusually good formalization target, because every constant in it
is written down.
The platform already hosts the surrounding infrastructure. The `CircleMethod` namespace
carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and
the `ThreePrimes` namespace carries a machine-checked proof of Vinogradov's three primes
theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and
should import from them rather than rebuild.
## Difficulty
The obvious route — deduce five primes from three primes — fails on the range where it is
needed. Vinogradov's theorem is asymptotic, and the best effective threshold is
$\exp(3100)$; below it the theorem says nothing, and $\exp(3100)$ is far beyond any
possible exhaustive check. So the entire difficulty lives in the window
$8.7\times10^{36} \le x \le \exp(3100)$, which must be handled by a circle-method argument
carrying explicit constants at every step.
Within that window the specific obstruction is the minor arc
$T_0/x \ll \|\alpha\|_{\mathbb{R}/\mathbb{Z}} \ll 1/N_0$. A direct Plancherel bound on the
$L^2$ side costs a factor of $\log x$, which is more than the argument can afford;
Montgomery's uncertainty principle cuts the loss to roughly $2\log x/\log N_0$, and only a
large-sieve estimate on prime pairs brings it down to a bounded factor of $8$. On the
$L^\infty$ side, Theorem 1.3 must be non-trivial across the whole window, which is why the
refinements (1.10)–(1.12) for $q$ near $1$ and near $x$ exist at all. Neither bound alone
suffices; the proof closes only because both are pushed to explicit constants
simultaneously.
## Formalization scope
The goal is stated over $\mathbb{N}$ as a `Multiset ℕ` of cardinality at most $5$ whose
members are all `Nat.Prime` and whose `sum` is $n$. A multiset, not a list or a finset:
repetition is essential ($9 = 3+3+3$) and order is not. **"At most five" is not "exactly
five"** — $3$ is a sum of one prime and cannot be a sum of five, since the least sum of
five primes is $10$. A formalization asserting exactly five primes is false, not merely
weaker.
The goal admits no trivializing reading: the empty multiset has sum $0 \ne n$, and the
cardinality bound is on the multiset itself, so no prime can be counted with multiplicity
zero to evade it.
Everything else in the mission is stated with explicit constants and $O^*(\cdot)$ bounds
rather than asymptotic notation, matching the paper: $X = O^*(Y)$ becomes $\|X\| \le Y$
outright. Sums over $n$ are unrestricted sums against a compactly supported cutoff, not
sums over `Finset.range`. Real powers are `Real.rpow`. The two cutoffs $\eta_0,\eta_1$ and
the sum $S_{\eta,q_0}$ are published as mission definitions; solvers should use them
verbatim rather than re-deriving equivalent forms.
**Three of the milestones are honest dead weight for a solver to attempt directly, and are
listed so the dependency graph is truthful rather than because they are tractable.**
Theorem 1.5 (all zeroes of $\zeta$ up to height $3.29\times10^9$ lie on the critical line)
and Theorem 1.6 (every even number up to $4\times10^{14}$ is a sum of two primes) are
finite, decidable statements that Lean can express and that are true, but each represents a
verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone
is $2\times10^{14}$ cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on
Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on
the analytic milestones, and the circle-method core (Theorem 8.2) can be closed
independently of them.
A complete development additionally needs the smoothed Vaughan identity bookkeeping, the
large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum
(Proposition 7.1), and Bourgain's trick of taking one of the three summands of size $x/K$.
The exponential sum machinery is reusable well beyond this mission — it is the standard
input to every explicit Goldbach-type result. Contributions to any milestone are welcome
independently, and a formalization of Helfgott's theorem that closes the goal by a
different route would be an entirely acceptable solution.
## Selected references
- T. Tao, *Every odd number greater than 1 is the sum of at most five primes*,
Mathematics of Computation 83 (2014), 997–1038.
[arXiv:1201.6656](https://arxiv.org/abs/1201.6656)
- H. A. Helfgott, *The ternary Goldbach conjecture is true*, 2013.
[arXiv:1312.7748](https://arxiv.org/abs/1312.7748)
- H. A. Helfgott and D. Platt, *Numerical verification of the ternary Goldbach
conjecture up to $8.875\cdot10^{30}$*, 2013.
[arXiv:1305.3062](https://arxiv.org/abs/1305.3062)
- O. Ramaré, *On Shnirel'man's constant*, Ann. Scuola Norm. Sup. Pisa 22 (1995), 645–706.
[numdam](http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/)
- L. Kaniecki, *On Shnirelman's constant under the Riemann hypothesis*, Acta Arithmetica
72 (1995), 361–374. [doi:10.4064/aa-72-4-361-374](https://doi.org/10.4064/aa-72-4-361-374)
- J. Richstein, *Verifying the Goldbach conjecture up to $4\cdot10^{14}$*, Mathematics of
Computation 70 (2001), 1745–1749.
[doi:10.1090/S0025-5718-00-01290-4](https://doi.org/10.1090/S0025-5718-00-01290-4)
- O. Ramaré and Y. Saouter, *Short effective intervals containing primes*, Journal of
Number Theory 98 (2003), 10–33.
[doi:10.1016/S0022-314X(02)00029-X](https://doi.org/10.1016/S0022-314X(02)00029-X)
- M. C. Liu and T. Z. Wang, *On the Vinogradov bound in the three primes Goldbach
conjecture*, Acta Arithmetica 105 (2002), 133–175.
[doi:10.4064/aa105-2-3](https://doi.org/10.4064/aa105-2-3)
- H. L. Montgomery, *The analytic principle of the large sieve*, Bulletin of the AMS 84
(1978), 547–567. [doi:10.1090/S0002-9904-1978-14497-8](https://doi.org/10.1090/S0002-9904-1978-14497-8)
- R. C. Vaughan, *The Hardy–Littlewood Method*, 2nd ed., Cambridge University Press, 1997.
[doi:10.1017/CBO9780511470929](https://doi.org/10.1017/CBO9780511470929)
More Asymmetry Bound: omega < 2.37134Research Paper
## Motivation
The **matrix-multiplication exponent** measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.
Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound $\omega<2.371339$. The mission targets the slightly weaker rational endpoint $2.37134$, keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. [*More Asymmetry Yields Faster Matrix Multiplication*, version 2, SODA 2025](https://arxiv.org/abs/2404.16349v2).
## Setting
Fix an arbitrary field $K$. The **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ represents multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition `matMulExp K` is the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ for integer dimensions $n\ge2$, with value $3$ at the excluded dimensions $0$ and $1$. This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.
The source tensor is the literal fourth power $T=CW_5^{\otimes4}$ of the **Coppersmith–Winograd tensor**. The public parenthesization is $(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$. Its asymptotic rank is at most $7^4=2401$. Its canonical coarse components are indexed by triples $(i,j,k)$ with $i+j+k=8$. This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. [More Asymmetry, Section 7](https://arxiv.org/abs/2404.16349v2).
A **complete split distribution** records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level $\ell\ge1$, these words have length $2^{\ell-1}$ over the alphabet $\{0,1,2\}$. Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified $\varepsilon\ge0$. An **interface tensor** is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. [More Asymmetry, Definitions 3.4–3.6 and 4.1](https://arxiv.org/abs/2404.16349v2).
## Formalization targets
The goal is the unconditional field-uniform statement
$$\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237134}{100000}.$$
Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.
The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.
The chosen internal parameter is $\tau_0=3952233/5000000$, so
$$2.371339<3\tau_0=2.3713398<2.37134.$$
The substantive value target is the existence of a real $V>2401$ such that the actual source has six-symmetrized $\tau_0$-value at least $V$ in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.
## Significance
This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. [More Asymmetry, Sections 2, 4–6](https://arxiv.org/abs/2404.16349v2); [Dupont et al., Section 2](https://arxiv.org/abs/2608.16884v1).
The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.
## Difficulty
The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. [More Asymmetry, Section 4.1 and Figure 1](https://arxiv.org/abs/2404.16349v2).
Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. [More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7](https://arxiv.org/abs/2404.16349v2).
## Formalization scope
The environment is pinned to Mathlib `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and Lean `v4.29.0-rc3`. The development reuses `TensorObj`, `MMObj`, restrictions, degenerations, tensor powers, existing tau-value predicates, and `matMulExp`. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written `Restrict A B`. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.
Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.
The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.
## Selected references
- Josh Alman, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou, *More Asymmetry Yields Faster Matrix Multiplication*, SODA 2025. [Pinned version 2](https://arxiv.org/abs/2404.16349v2).
- Authors' code and parameters for the original fourth-power bounds. [OSF release](https://osf.io/mw5ak/).
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, FOCS 2023. [Version 5](https://arxiv.org/abs/2210.10173v5).
- Emilien Dupont et al., *Improving the matrix multiplication exponent with modern optimization and AlphaEvolve*, 2026 preprint. [Version 1](https://arxiv.org/abs/2608.16884v1).