Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 85 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Klimov, Pil'tai, Sheptitskaya (1972): $115$ ; Riesel–Vaughan (1983): $19$ for all integers, using zero-based prime-counting estimates.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's earlier values ( $100\,001$ down to $151$ ) came from Schnirelmann's method with every constant written out, using only weak Chebyshev lower bounds for $\pi(y)$ . This entry keeps the same machinery as the $151$ entry but feeds it Chebyshev's sharper lower bound $\psi(x) \ge ax - 5\log x + 5$ with $a \approx 0.9212$ , obtained from the weights $1, -1, -1, -1, +1$ at $1, 2, 3, 5, 30$ . No zeta-zero input is used.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 85,\ \textstyle\sum s = n.

This is the campaign template with the value $85$ filled in.

How the bound arises

Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$ . We show $\sigma(A) \ge 1/42$ , then conclude with Mann's theorem as in the $241$ entry. Write $L = \log y$ for the scale.

Chebyshev's constant $a \approx 0.9212$ . For $x \ge 30$ , $\psi(x) \ge ax - 5\log x + 5$ with $a = \tfrac{7}{15}\log 2 + \tfrac{3}{10}\log 3 + \tfrac16 \log 5$ (Chebyshev's argument with $\log \lfloor x \rfloor!$ and Stirling-type bounds; ported from the PrimeNumberTheoremAnd library with explicit bounds for $\log 3$ and $\log 5$ ). Since $\psi(x) \le \pi(x)\log x$ , this gives $\pi(x) \ge (ax - O(\log x))/\log x$ . On its own it covers $L \lesssim 76$ through $B \subseteq A$ .
Small-shift range (Riesel–Vaughan 1983, Lemma 8), $76 \le L \le 7000$ . Fix the first $300$ odd primes $p_1 \le 1993$ and let $R(s)$ count $s = p_1 + q$ with $q$ prime. Then $\sum_s R(s)$ needs only the lower bound for $\pi$ , and $\sum_s R(s)^2$ needs an upper bound for prime pairs $q, q + d$ with a fixed even shift $d$ . That bound is the Selberg sieve for $a(a+d)$ on an interval, whose local data are those of the existing Goldbach sieve with $s := d$ . The weight sum $\sum_{p_1 \ne p_2} C(p_1 - p_2)$ over these primes is a finite kernel computation. Cauchy–Schwarz then gives $\#\{s \le y : R(s) > 0\} \ge y/83$ on this range.
Large range $L \ge 7000$ : the Selberg pointwise bound $r(s) \le b\,C(s)\,s/\log^2 s$ with $b = 8.13$ , the weighted first moment (now with constant $a^2$ ), the sixteenth moment of $C(s)$ , and Hölder, as in the $241$ entry, at a much higher threshold.
Mann's theorem turns $42\,\sigma(A) \ge 1$ into $42A = \mathbb{Z}_{\ge 0}$ , so every odd $n \ge 171$ is a sum of exactly $85$ primes ( $84$ odd primes plus one $3$ , padded with twos and threes for small $n$ ), and small $n$ are handled with twos and threes: $K = 2 \cdot 42 + 1 = 85$ .

Significance

The argument stays elementary: no prime number theorem and no zeros of $\zeta$ or $L$ -functions. New reusable components:

Explicit Selberg upper bound for prime pairs $(q, q+d)$ with a fixed shift, uniform in $d$ .
The Riesel–Vaughan small-shift second-moment argument.
A self-contained Lean proof of Chebyshev's lower bound $\psi(x) \ge ax - 5\log x + 5$ ( $a \approx 0.9212$ ), carried into the sieve moments.

Formalization scope

The Lean statement is the campaign template verbatim with $85$ in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev function $\psi$ with $\psi(x) \le \pi(x)\log x$ and the Λ² sieve framework.

Selected references

H. Riesel, R. C. Vaughan, On sums of primes, Ark. Mat. 21 (1983), 45–74.
P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
Chebyshev's lower bound as formalized in PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).
Explicit improvement of the $151$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $85$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 159 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Klimov, Pil'tai, Sheptitskaya (1972): $115$ ; Riesel–Vaughan (1983): $19$ for all integers, using zero-based prime-counting estimates.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's earlier values ( $100\,001$ down to $241$ ) came from Schnirelmann's method with every constant written out. Those arguments stall near $241$ because the medium range relies only on a Chebyshev lower bound for $\pi(y)$ . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 159,\ \textstyle\sum s = n.

This is the campaign template with the value $159$ filled in.

How the bound arises

Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$ . We show $\sigma(A) \ge 1/79$ , then conclude with Mann's theorem as in the $241$ entry. Write $L = \log y$ for the scale.

Chebyshev constant $\log 2$ . Mathlib's $\psi(x) \ge (x-1)\log 2 - \log(x+2)$ gives $\pi(x) \ge (x \log 2 - O(\log x))/\log x$ , better than the constant $2/3$ used in earlier entries. On its own it covers $L \lesssim 90$ through $B \subseteq A$ .
Small-shift range (Riesel–Vaughan 1983, Lemma 8). Fix the first $150$ odd primes $p_1$ (up to $877$ ) and let $R(s)$ count $s = p_1 + q$ with $q$ prime. Then $\sum_s R(s)$ needs only $\pi$ , and $\sum_s R(s)^2$ needs an upper bound for prime pairs $q, q + d$ with a fixed even shift $d$ . That bound is the Selberg sieve for $a(a+d)$ on an interval, whose local data are those of the existing Goldbach sieve with $s := d$ . The weight sum $\sum_{p_1 \ne p_2} C(p_1 - p_2)$ over these primes is a finite computation. Cauchy–Schwarz then gives $\#\{s \le y : R(s) > 0\} \ge y/158$ for $90 \lesssim L \le 3000$ .
Large range $L \ge 3000$ : the Selberg pointwise bound $r(s) \le b\,C(s)\,s/\log^2 s$ , the weighted first moment (now with constant $(\log 2)^2$ ), a high moment of $C(s)$ , and Hölder, as in the $241$ entry, at a much higher threshold.
Mann's theorem turns $79\,\sigma(A) \ge 1$ into $79A = \mathbb{Z}_{\ge 0}$ , so every odd $n$ beyond a small bound is a sum of $158$ odd primes plus one $3$ , and small $n$ are handled with twos and threes: $K = 2 \cdot 79 + 1 = 159$ .

Significance

The argument stays elementary: no prime number theorem and no zeros of $\zeta$ or $L$ -functions. New reusable components:

Explicit Selberg upper bound for prime pairs $(q, q+d)$ with a fixed shift, uniform in $d$ .
The Riesel–Vaughan small-shift second-moment argument.
Chebyshev's $\log 2$ constant from Mathlib carried into the sieve moments.

Formalization scope

The Lean statement is the campaign template verbatim with $159$ in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).

Selected references

H. Riesel, R. C. Vaughan, On sums of primes, Ark. Mat. 21 (1983), 45–74.
P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
Explicit improvement of the $241$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $159$ ; not peer reviewed.

2 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 151 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Klimov, Pil'tai, Sheptitskaya (1972): $115$ ; Riesel–Vaughan (1983): $19$ for all integers, using zero-based prime-counting estimates.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 151,\ \textstyle\sum s = n.

This is the campaign template with the value $151$ filled in.

How the bound arises

Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$ . We show $\sigma(A) \ge 1/75$ , then conclude with Mann's theorem as in the $241$ entry. Write $L = \log y$ for the scale.

Chebyshev constant $\log 2$ . Mathlib's $\psi(x) \ge (x-1)\log 2 - \log(x+2)$ gives $\pi(x) \ge (x \log 2 - O(\log x))/\log x$ , better than the constant $2/3$ used in earlier entries. On its own it covers $L \lesssim 90$ through $B \subseteq A$ .
Small-shift range (Riesel–Vaughan 1983, Lemma 8). Fix the first $500$ odd primes $p_1$ (up to $3581$ ) and let $R(s)$ count $s = p_1 + q$ with $q$ prime. Then $\sum_s R(s)$ needs only $\pi$ , and $\sum_s R(s)^2$ needs an upper bound for prime pairs $q, q + d$ with a fixed even shift $d$ . That bound is the Selberg sieve for $a(a+d)$ on an interval, whose local data are those of the existing Goldbach sieve with $s := d$ . The weight sum $\sum_{p_1 \ne p_2} C(p_1 - p_2)$ over these primes is a finite computation. Cauchy–Schwarz then gives $\#\{s \le y : R(s) > 0\} \ge y/150$ for $90 \lesssim L \le 10^4$ .
Large range $L \ge 10^4$ : the Selberg pointwise bound $r(s) \le b\,C(s)\,s/\log^2 s$ , the weighted first moment (now with constant $(\log 2)^2$ ), a high moment of $C(s)$ , and Hölder, as in the $241$ entry, at a much higher threshold.
Mann's theorem turns $75\,\sigma(A) \ge 1$ into $75A = \mathbb{Z}_{\ge 0}$ , so every odd $n$ beyond a small bound is a sum of $150$ odd primes plus one $3$ , and small $n$ are handled with twos and threes: $K = 2 \cdot 75 + 1 = 151$ .

Significance

The argument stays elementary: no prime number theorem and no zeros of $\zeta$ or $L$ -functions. New reusable components:

Explicit Selberg upper bound for prime pairs $(q, q+d)$ with a fixed shift, uniform in $d$ .
The Riesel–Vaughan small-shift second-moment argument.
Chebyshev's $\log 2$ constant from Mathlib carried into the sieve moments.

Formalization scope

The Lean statement is the campaign template verbatim with $151$ in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).

Selected references

H. Riesel, R. C. Vaughan, On sums of primes, Ark. Mat. 21 (1983), 45–74.
P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
Explicit improvement of the $241$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $151$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 241 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $241$ , from the same elementary circle of ideas.

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 241,\ \textstyle\sum s = n.

This is the campaign template with the value $241$ filled in. The argument proves the stronger statement that every odd $n \ge 483$ is a sum of exactly $241$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It follows the companion $351$ entry, with every parameter pushed to the limit of the same tools. Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$ . We show $\sigma(A) \ge 1/120$ :

Sieve at a low threshold. The explicit Selberg inequality with $z = \sqrt{s}/(\log s)^2$ gives $r(s) \le \tfrac{45}{4}\,C(s)\,s/(\log s)^2$ for even $s \ge e^{130}$ , where $r(s)$ counts representations $s = p + q$ by odd primes and $C(s) = \prod_{p \mid s}\bigl(1 + p/(p-1)^2\bigr)$ .
Weighted first moment. $\sum_{e^{130} < s \le x} r(s)\,(\log s)^2/s \ge 0.439\,x$ for $x \ge e^{159}$ .
Sixteenth moment of $C$ . Expanding $C(s)^{16}$ over squarefree divisors, treating the primes up to $31$ exactly and bounding the tail in one step, gives $\sum_{s \le x,\, 2 \mid s} C(s)^{16} \le 9.44 \cdot 10^{12}\, x$ .
Hölder with exponent $16$ then gives $\#\{s \le x : r(s) > 0\} \ge x/238$ for $x \ge e^{159}$ . Below that scale, Chebyshev's bound $\pi(y) - 1 \ge 2y/(3 \log y)$ and $B \subseteq A$ suffice, so $\sigma(A) \ge 1/120$ at every scale.
Mann's theorem, $\sigma(D + E) \ge \min\{1, \sigma(D) + \sigma(E)\}$ for sets containing $0$ , gives $120A = \mathbb{Z}_{\ge 0}$ , so $240B = \mathbb{Z}_{\ge 0}$ . For odd $n \ge 3K = 723$ , write $(n - 3K)/2$ as a sum of $240$ elements of $B$ and add one more $3$ . For $483 \le n < 723$ , use $n - 2K$ threes and $3K - n$ twos. This gives $K = 241$ .

About $241$ is the floor of this method: the medium range relies on the Chebyshev constant $2/3$ , which forces the sieve threshold below $e^{4k/3}$ and so inflates the sieve coefficient.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$ , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization. Reusable components:

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ at an arbitrary threshold.
High moments $\sum_{s \le x} C(s)^{q}$ of the singular-series factor.
Mann's theorem ( $\alpha\beta$ theorem) on Schnirelmann density.

Formalization scope

The Lean statement is the campaign template verbatim with $241$ in place of the value. All the ingredients above except the moment bound and the final assembly are already proved on the platform (Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density).

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026), extending the $351$ entry. Source of the constant $241$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Dynamical Systems Functional Analysis·Captain: dbenbenn

Connes–Feldman–Weiss: an amenable equivalence relation is generated by a single transformationResearch Paper

This mission formalizes A. Connes, J. Feldman and B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450 (doi:10.1017/S014338570000136X).

Motivation

A countable group acting on a measure space partitions it into countable orbits, and much of ergodic theory studies actions only through this orbit equivalence relation. The simplest relations are those of a single transformation, the orbits of an action of $\mathbb Z$ . Connes, Feldman and Weiss characterize exactly which relations are of this kind, up to null sets: the amenable ones, those carrying an invariant mean. Since the orbit relation of any action of a countable amenable group is amenable, every such action is orbit equivalent to an action of $\mathbb Z$ . The same theorem gives the uniqueness of Cartan subalgebras in hyperfinite von Neumann algebras.

On this platform it is the missing link in the Lodha–Moore mission, which passes between Lodha and Moore's definition of a $\mu$ -amenable relation (an orbit relation of $\mathbb Z$ off a null set) and the invariant-mean definition of the Monod bundle: one direction is proved, the other (LodhaMoore.isMuAmenable_of_isAmenableRel) is this mission's goal in Lodha and Moore's language.

Timeline.

1959, 1963: Dye proves orbit equivalence for measure-preserving actions of abelian groups and groups of polynomial growth (doi:10.2307/2372852, doi:10.2307/2373108).
1976: Krieger classifies non-singular transformations up to orbit equivalence (doi:10.1007/BF01360278).
1977: Feldman and Moore set up countable Borel equivalence relations and their von Neumann algebras (doi:10.1090/S0002-9947-1977-0578656-4).
1978: Zimmer introduces amenable actions and shows that discrete subgroups act amenably on $G/P$ for $P$ amenable (doi:10.1016/0022-1236(78)90013-7).
1980: Ornstein and Weiss prove that every measure-preserving action of a countable amenable group is orbit equivalent to an action of $\mathbb Z$ (doi:10.1090/S0273-0979-1980-14702-3).
1981: Connes, Feldman and Weiss prove it for every amenable non-singular countable equivalence relation, without a group.
2004: Kechris and Miller give a detailed modern account in Topics in orbit equivalence (doi:10.1007/b99421).

Setting

$X$ is a standard Borel space with a $\sigma$ -finite measure $\mu$ . A discrete measured equivalence relation (IsDiscreteMeasured μ R) is a Borel equivalence relation $R \subseteq X \times X$ whose classes are countable and for which $\mu$ is quasi-invariant: the saturation $R(A) = \{x \mid \exists y \in A, (x, y) \in R\}$ of a null Borel set $A$ is null.

$R$ carries the measure $m = \int \nu^x\, d\mu(x)$ , $\nu^x$ the counting measure on the class of $x$ (relMeasure), and the module $\delta$ , the density of $m$ against its image under $(x, y) \mapsto (y, x)$ (module). A partial transformation of $R$ is a Borel bijection between Borel subsets of $X$ whose graph lies in $R$ (Monod.PartialTransformation).

$R$ is amenable (Monod.IsAmenableRel) when it has a left invariant mean: a positive normalized map $P$ from bounded functions on $R$ to bounded functions on $X$ with $P(f^\phi) = (Pf)^\phi$ for every partial transformation $\phi$ (Definitions 5–6). $R$ is of type I (IsTypeI) when, off a null saturated set, its quotient is a standard Borel space, and hyperfinite (IsHyperfinite) when, off a null set, it is a countable increasing union of type I equivalence relations (Definition 1). A finite subequivalence relation (IsFiniteSubrelation) is a Borel $T \subseteq R$ that is an equivalence relation with finite classes on $T^{(0)} = \{x \mid (x, x) \in T\}$ .

Formalization targets

Goal (p. 431)

For $R$ amenable there are a non-singular Borel automorphism $T$ of $X$ and a null set $N$ with

(x, y) \in R \iff \exists n \in \mathbb Z,\ y = T^n x \qquad (x, y \notin N).

Milestones

§1 (p. 434): the type I criterion; hyperfinite relations are those generated by one automorphism (Dye, external); subrelations of hyperfinite relations are hyperfinite.
§§2–3: Lemma 2 (disintegration over a finite subrelation), Feldman and Moore's Theorem 1 (external, as the proof of Lemma 3 applies it), Lemma 3 (bounded sets), Lemma 4 (local triviality).
§§5–6: Lemma 8 (the Følner condition), Lemma 9 (approximation by finite subrelations), Theorem 10 (hyperfinite if and only if amenable).
§7: Corollary 12, Corollary 13 (Vershik), and Corollary 14 with the amenability of the action it rests on (Zimmer, external).

Significance

The result. Theorem 10 turns amenability, which is usually easy to check, into hyperfiniteness, which is the structure one wants: for instance, the action of $\mathrm{SL}_2(\mathbb Z)$ on the projective line, or of any discrete group on $G/P$ with $P$ amenable, is generated by a single transformation. On this platform it closes the open direction, LodhaMoore.isMuAmenable_of_isAmenableRel, and with it Lodha and Moore's Theorem 2.1.

Formalizing it. No machine-checked proof of the theorem exists, in Mathlib or elsewhere as far as a search finds; Mathlib has no theory of countable Borel equivalence relations. A complete development builds that theory from the descriptive set theory Mathlib has.

Difficulty

The theorem is about relations without a group. The obvious route, through a countable group generating $R$ and an amenability of that group, is unavailable: the orbit relation of a nonamenable group, such as $\mathrm{SL}_2(\mathbb Z)$ acting on the projective line, can be amenable, and there is no group whose Følner sets one could use. The Følner sets of Lemma 8 have to be produced from the invariant mean on the relation itself, which needs duality between $L^1$ and $L^\infty$ and convexity arguments. Underneath, even the basic facts used in §§1–3 (that $R$ is a countable union of graphs of Borel automorphisms, that $m$ is a measure, that saturations of Borel sets are Borel) rest on the Lusin–Novikov uniformization theorem, which is not in Mathlib. It is published here as standalone theorems: a Borel set with countable sections is a countable union of Borel graphs, and a countable-to-one Borel map is injective on countably many Borel pieces covering its domain.

Formalization scope

All statements carry the hypotheses of §1: $X$ standard Borel (StandardBorelSpace), $\mu$ $\sigma$ -finite, $R$ a Borel equivalence relation with countable classes and $\mu$ quasi-invariant. Lemmas 8 and 9 take $\mu$ a probability measure, as the paper's proof of Lemma 9 does. “Up to a null set” is read as “off a $\mu$ -null Borel set of points”, which by quasi-invariance agrees with the paper's $m$ -null sets. Amenability is the published Monod definition, an invariant mean on bounded measurable functions modulo null sets; it is not trivial (the relation of $\mathrm{PSL}_2(A)$ for a countable dense subring $A$ of $\mathbb R$ is not amenable, Monod.not_isAmenableRel_mob).

The definitions are in the definition bundle ConnesFeldmanWeiss. Reusable beyond this mission: the Feldman–Moore theorem and the basic theory of countable Borel equivalence relations, both welcome as standalone theorems.

What is left out. Proposition 7 and Corollary 11 need the von Neumann algebra of a relation and its Cartan subalgebras, which Mathlib does not have. The final part of the paper (Lemma 15 to Corollary 21) treats relations with uncountable classes through transverse functions, including foliations; it is a different setting with its own definitions.

Selected references

A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
H. A. Dye, On groups of measure preserving transformations. I, Amer. J. Math. 81 (1959) 119–159. doi:10.2307/2372852
J. Feldman, C. C. Moore, Ergodic equivalence relations, cohomology, and von Neumann algebras. I, Trans. Amer. Math. Soc. 234 (1977) 289–324. doi:10.1090/S0002-9947-1977-0578656-4
R. J. Zimmer, Amenable ergodic group actions and an application to Poisson boundaries of random walks, J. Funct. Anal. 27 (1978) 350–372. doi:10.1016/0022-1236(78)90013-7
D. Ornstein, B. Weiss, Ergodic theory of amenable group actions. I: The Rohlin lemma, Bull. Amer. Math. Soc. 2 (1980) 161–164. doi:10.1090/S0273-0979-1980-14702-3
A. S. Kechris, B. D. Miller, Topics in orbit equivalence, Lecture Notes in Math. 1852, Springer, 2004. doi:10.1007/b99421

19 thms1 active userReviewed

Completed

Calculus of Variations Mathematical Physics Partial Differential Equations·Captain: shivm

Uniqueness of the Hemispheric Saddle Profile on a Magnetic Sphere (AIM 241)Open Problem

Motivation

Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at $\kappa=4$ ). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.

Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.

Setting

For anisotropy $\kappa>0$ the energy of $m:S^2\to S^2$ is $\mathcal E_\kappa(m)=\frac12\int_{S^2}|\nabla m|^2+\kappa\,(1-(m\cdot x)^2)$ . An axisymmetric field $m=(\sin h\cos\varphi,\ \sin h\sin\varphi,\ \cos h)$ with profile $h(\theta)$ is critical exactly when

h''+\cot\theta\,h'-\frac{\sin 2h}{2\sin^2\theta}-\frac{\kappa}{2}\sin(2h-2\theta)=0\qquad(0<\theta<\pi).\tag{2.6}

The hemispheric class $H_{0,2}$ adds $h(0)=0$ , $h(\pi)=2\pi$ , $h(\pi-\theta)=2\pi-h(\theta)$ .

Formalization target

For every $\kappa\ge4$ there is exactly one smooth profile in $H_{0,2}$ that solves (2.6) and induces a smooth map $S^2\to S^2$ . The statement may be proved or disproved.

Significance

Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of $\mathcal E_\kappa$ .

Difficulty

(2.6) is singular at both poles and $H_{0,2}$ is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge $\theta\le h\le 2\theta$ . Numerical evidence (shooting) finds at $\kappa=4$ , besides $h=2\theta$ , a second solution in the class with $h'(0)\approx3.899$ (similarly at $\kappa=5,8$ ), which leaves the wedge.

Formalization scope

Profiles are functions $h:\mathbb R\to\mathbb R$ ; all conditions, and the uniqueness, are imposed on $[0,\pi]$ only (values outside are unconstrained, so uniqueness on $\mathbb R$ would be trivially false). Smoothness is ContDiffOn ℝ ∞ on $[0,\pi]$ . "Induces a smooth map" means the field extended to $\mathbb R^3\setminus\{0\}$ as a function of $x/|x|$ is $C^\infty$ there; this excludes profiles with a cone singularity at a pole. The paper's $H_{0,2}$ uses piecewise $C^1$ profiles; by its Corollary 2.7 it has the same solutions.

Selected references

S. Gustafson, D. Meinert, C. Melcher, Saddle Point Configurations for Spherical Ferromagnets, preprint, 2025. arXiv:2509.05159
V. P. Kravchuk et al., Topologically stable magnetization states on a spherical shell: Curvature-stabilized skyrmions, Phys. Rev. B 94, 144402, 2016. DOI
AIM open problems list, problem 241. github.com/MColbrook/AIM

2 thms1 active userReviewed

Completed

Combinatorics Information Theory·Captain: shivm

Periodic Multidimensional Costas Arrays (Rubio–Torres Conjecture 1)Open Problem

Motivation

A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their $m$ -dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.

Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order $\le 2$ . 2023: Rubio–Torres prove the odd-order and 3D cases, give $2\times2\times4$ examples, and state Conjecture 1.

Setting

Let $[n]=\{1,\dots,n\}$ , $X=[a_1]\times\cdots\times[a_k]$ , $Y=[b_1]\times\cdots\times[b_l]$ with all sides $\ge2$ , and $\varphi:X\to Y$ a bijection; the dots are $(x,\varphi(x))\in\mathbb Z^{k+l}$ . The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over $\mathbb Z^{k+l}$ , the dots inside every translate $t+X\times Y$ have distinct difference vectors.

Formalization target

Conjecture 1: if $k\ge l\ge1$ and $\varphi$ defines a periodic Costas array, then

\prod_{i=1}^k a_i=2^k,

equivalently every $a_i=2$ . The condition $k\ge l$ is a normalization ( $\varphi^{-1}$ swaps the boxes).

Significance

A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.

Difficulty

The Rubio–Torres counting argument needs a bound that is available only when $Y$ is one-dimensional, which is why it stops at $m=3$ . Computational evidence: an exhaustive window check reports that the $2\times3\times2\times3$ array with dots $(1,1,1,1),(1,2,1,2),(1,3,2,1),(2,1,1,3),(2,2,2,3),(2,3,2,2)$ is periodic Costas, which would disprove the conjecture.

Formalization scope

A point of $\mathbb Z^{k+l}$ is a pair $(x,y)$ ; boxes are 1-based; $\varphi$ is a total function $\mathbb Z^k\to\mathbb Z^l$ whose values off $X$ are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all $t\in\mathbb Z^{k+l}$ , and $k,l\ge1$ and sides $\ge2$ are part of the definition, so no degenerate case holds vacuously.

Selected references

I. Rubio, J. Torres, Multidimensional Costas Arrays and Their Periodicity, IEEE Trans. Inf. Theory 69(8), 2023, 5032–5040. arXiv:2208.02378, DOI
J. P. Costas, A study of a class of detection waveforms having nearly ideal range-Doppler ambiguity properties, Proc. IEEE 72(8), 1984, 996–1009.
S. W. Golomb, H. Taylor, Constructions and properties of Costas arrays, Proc. IEEE 72(9), 1984, 1143–1163.

2 thms1 active userReviewed

Completed

Combinatorics·Captain: mysticflounder

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

The Schur number $S(n)$ is the largest $N$ such that $[1, N] = \{1, \dots, N\}$ can be partitioned into $n$ sumfree sets, sets with no $x, y, z$ such that $x + y = z$ ( $x = y$ allowed). Schur's argument gives $S(n) \le R_n(3) - 2$ , where the triangle Ramsey number $R_n(3)$ is the least $N$ such that every colouring of the edges of $K_N$ with $n$ colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known (Heule 2018). For six colours the published range is $536 \le S(6) \le 1836$ ; the upper bound is $R_6(3) - 2$ with $R_6(3) \le 1838$ (DS1, rev. 18).

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and $R_{n+1}(3) \le (n+1)(R_n(3) - 1) + 2$ (Theorem 6) (doi).
1961: Baumert finds $S(4) = 44$ by computer, as reported by Fredricksen and Sweet; they and Heule cite Golomb–Baumert 1965 for it.
1973: Chung proves $R_4(3) \ge 51$ (doi).
1997: Wan bounds $R_n(3)$ and, for even $n \ge 6$ , states $S_n < n!\,(e - e^{-1} + 3)/2 - n + 2$ (zbMATH 0882.05095 summary; doi). If his $S_n$ is the least $N$ that forces a monochromatic solution, this is the centred bound below, applied to his own bound on $R_{n-1}(3)$ ; if it is the largest $N$ , it is $1$ above it. His proof was not read.
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, which also lists $R_5(3) \le 307$ ).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (AAAI-18; preprint arXiv:1711.08076).
2026: a public repository of M. Tatarevic gives a computer-assisted argument for $R_4(3) \le 61$ . Its Lean development assumes that a family of 56,830 SAT instances is unsatisfiable, and the repository records solver results for them. The project of this mission's author produced LRAT certificates for all 56,830 instances and checked them; the report is in the repository's issue tracker. This mission does not depend on it.

The first target is a centred-interval bound: if $R_k(3) \le r$ , then $S(k+1) \le 2(k+1)\lfloor (r-1)/2 \rfloor + 1$ . With $R_4(3) \le 61$ the recursive bound gives $R_5(3) \le 302$ , and the centred bound gives $S(6) \le 1801$ ; with $R_5(3) \le 307$ it gives only $1837$ . The mission formalizes what a Schur colouring of $[1, 1801]$ with six colours would have to look like under $R_4(3) \le 61$ .

Setting

All numbers are natural numbers, $\mathbb{N} = \{0, 1, 2, \dots\}$ , and $[a, b] = \{a, \dots, b\}$ .

Schur colourings and covers. A colouring with $n$ colours is a map $c : \mathbb{N} \to \mathrm{Fin}\,n$ . It is a Schur colouring of $[1, N]$ (SchurColoring N c) if there are no $x, y \ge 1$ with $x + y \le N$ and $c(x) = c(y) = c(x + y)$ , the case $x = y$ included. The cover form uses SumFree S and CoveredBySumFree X n ( $X$ lies in the union of $n$ sumfree sets); for $n \ge 1$ the two bridge theorems pass between the two forms in both directions.

Triangle Ramsey property. $\mathrm{TR}(k, r)$ (TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ it is the inequality $R_k(3) \le r$ .

Neighbourhoods. The difference colouring gives a pair $\{x, y\}$ the colour $c(|x - y|)$ . For a Schur colouring of $[1, N]$ it has no monochromatic triangle on $[0, N]$ , since $(y - x) + (z - y) = z - x$ . Write

$\Gamma_i(V, v) = \{\, w \in V : w \ne v,\ c(|v - w|) = i \,\}$ (colorNbhd c V v i);
$V_m = \Gamma_{c(m+1)}([0, 2m+1], m)$ , the central neighbourhood (centralNbhd c m), which contains $2m + 1$ ;
$P_i = \Gamma_i(V_m, 2m+1)$ , the endpoint neighbourhoods (endpointNbhd c m i).

The frontier. The frontier hypotheses are $\mathrm{TR}(k, u + 1)$ , $2t = (k+1)u$ , $m = (k+2)t$ , and $c$ a Schur colouring of $[1, 2m + 1]$ with $k + 2$ colours. From the first two, $\mathrm{TR}(k + 1, 2t + 2)$ holds, and the centred bound excludes Schur colourings of $[1, 2m + 2]$ with $k + 2$ colours; $[1, 2m + 1]$ is the frontier interval. Six colours: $k = 4$ , $u = 60$ , $t = 150$ , $m = 900$ , $2m + 1 = 1801$ .

Example. For $k = 1$ , $u = 2$ , $t = 2$ , $m = 6$ (and $13 = S(3)$ ), the classes $\{1, 4, 7, 10, 13\}$ , $\{2, 3, 11, 12\}$ , $\{5, 6, 8, 9\}$ form a Schur colouring of $[1, 13]$ , with $V_6 = \{2, 5, 7, 10, 13\}$ and endpoint neighbourhoods $\{2, 10\}$ and $\{5, 7\}$ , both closed under $x \mapsto 12 - x$ .

Formalization targets

Goal: six colours under $R_4(3) \le 61$

\mathrm{TR}(4, 61) \ \text{ and } \ c \text{ a Schur colouring of } [1, 1801] \text{ with six colours} \implies (1)\text{–}(5),

where $q = c(901)$ , $V = V_{900}$ and $P_i = \Gamma_i(V, 1801)$ :

each colour occurs $150$ times in $[1, 900]$ ;
$|V| = 301$ ;
$|\Gamma_i(V, v)| = 60$ for every $v \in V$ and every colour $i \ne q$ ;
$c(901 - d) = c(901 + d)$ for every $d \in [1, 900]$ with $c(d) = q$ ;
for every colour $i \ne q$ : $|P_i| = 60$ ; $x \mapsto 1800 - x$ maps $P_i$ to itself without fixed points; and $c(|x - y|) \notin \{i, q\}$ for distinct $x, y \in P_i$ .

The goal is a structure theorem under the hypothesis $R_4(3) \le 61$ . It does not prove $S(6) \le 1800$ , and it does not assert that a Schur colouring of $[1, 1801]$ with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.

Centred-interval bound

\mathrm{TR}(k, r) \implies \Bigl[1,\ 2(k+1)\Bigl\lfloor \tfrac{r-1}{2} \Bigr\rfloor + 2\Bigr] \text{ is not covered by } k + 1 \text{ sumfree sets.}

Balanced colour classes

\mathrm{TR}(k, 2t + 2),\ m = (k+1)t,\ c \text{ a Schur colouring of } [1, 2m+1] \text{ with } k + 1 \text{ colours} \implies \bigl|\{\, d \in [1, m] : c(d) = j \,\}\bigr| = t \ \text{ for every colour } j.

Nested saturation

\text{frontier hypotheses} \implies |\Gamma_i(V_m, v)| = u \qquad (v \in V_m,\ i \ne c(m+1)).

Automorphism extension

For a colouring $\mathrm{col}$ of ordered pairs, a finite set $W$ , a point $e \notin W$ and a map $J$ with $J(W) \subseteq W$ , $J \circ J = \mathrm{id}$ on $W$ and $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$ on $W$ :

v \in W \text{ and } J(v) \text{ have equal colour degrees in } W \cup \{e\} \implies \mathrm{col}(v, e) = \mathrm{col}(J(v), e).

Forced reflection

\text{frontier hypotheses} \implies c(m + 1 - d) = c(m + 1 + d) \qquad (d \in [1, m],\ c(d) = c(m+1)).

The saturation degree is even

\text{frontier hypotheses} \implies u \text{ is even}.

Significance

The result itself. Under $R_4(3) \le 61$ , $S(6) \le 1801$ , and the goal constrains a six-colour Schur colouring of $[1, 1801]$ as listed above. In particular, each of its five endpoint neighbourhoods is a set of $30$ pairs $\{900 - d, 900 + d\}$ whose difference colouring uses at most four colours, is invariant under $x \mapsto 1800 - x$ and, like that of every subset of $[0, 1801]$ , has no monochromatic triangle. So such a colouring yields five colourings of $K_{60}$ with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give $S(6) \le 1800$ under the same hypothesis. Whether it can occur, and whether $S(6) \le 1800$ , are open.

Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. $R_4(3) \le 61$ is not formalized in the mission.

Difficulty

The centred bound counts, for one colour class, the points $h \pm a$ around the centre of the interval. At the frontier every such count is tight: each colour has $t$ elements in $[1, m]$ , and inside $V_m$ each colour other than $c(m+1)$ has degree $u$ , the largest value that $R_k(3) \le u + 1$ allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd $u$ ; at six colours $u = 60$ .

The reflection is not a property of Schur colourings in general: the colouring $\{1, 4\}$ , $\{2, 3\}$ , $\{5\}$ of $[1, 5]$ has $c(2) = c(3)$ but $c(1) \ne c(5)$ . At the frontier the theorem asserts it only for the $d$ with $c(d) = c(m+1)$ , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: $S(5) = 160$ already needed a large certified SAT computation (Heule 2018), and $[1, 1801]$ with six colours is a much larger instance.

Formalization scope

Colourings are functions ℕ → Fin n on all of $\mathbb{N}$ ; SchurColoring N c constrains only $[1, N]$ , with $x = y$ allowed. Distances are Nat.dist.
Neighbourhoods are Finsets. $V_m$ lies in range (2 * m + 2) $= [0, 2m+1]$ , so the point $0$ is a candidate member; the centre $m$ never is.
TriangleRamsey k r takes colours from any Finset of at most $k$ naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs $x < y$ of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.
Covers. CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in $X$ .
Subtraction is truncated. Under the hypotheses, none of $r - 1$ , $N - 1$ , $m + 1 - d$ , $2m - x$ (with $x \in P_i$ ), $901 - d$ and $1800 - x$ truncates.
No trivialization. The frontier theorems are vacuous for $u = 0$ , and for $k = 0$ (then $[1, 2m + 1] \supseteq [1, 5]$ , while $S(2) = 4$ ). For $k = 1$ they are not: the Schur colourings of $[1, 13]$ meet the hypotheses, and every conclusion can be checked by hand. The goal holds vacuously if $R_4(3) > 61$ or if no six-colour Schur colouring of $[1, 1801]$ exists; it is a structure theorem, not a claim that such a colouring exists.

Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every $k$ , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired $60$ -point sets exists.

Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.

Selected references

R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
S. W. Golomb, L. D. Baumert, Backtrack programming, J. ACM 12 (1965) 516–524. https://doi.org/10.1145/321296.321300
F. R. K. Chung, On the Ramsey numbers $N(3, 3, \dots, 3; 2)$ , Discrete Math. 5 (1973) 317–321. https://doi.org/10.1016/0012-365X(73)90125-8
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI Conf. Artif. Intell. 32 (2018). https://doi.org/10.1609/aaai.v32i1.12209 ; preprint arXiv:1711.08076 (2017). https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
M. Tatarevic, An improved upper bound for the Ramsey number R(3,3,3,3), GitHub repository, 2026, commit ddd7755. https://github.com/milostatarevic/r3333-upper-bound/commit/ddd7755476db3f0751181db0daec75342576cdd1
A. McKenna, $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier, Zenodo, 2026. https://doi.org/10.5281/zenodo.23156099 ; Lean code: https://github.com/mysticflounder/schur-centred-bound (release v1.0.1).

15 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 6101 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $6101$ , from the same elementary circle of ideas.

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 6101,\ \textstyle\sum s = n.

This is the campaign template with the value $6101$ filled in. The source proves the stronger statement that every odd $n \ge 12\,203$ is a sum of exactly $6101$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the first moment:

Whole-triangle count. Counting all pairs with $p + q \le x$ gives $\sum_{s \le x} r(s) \ge 2(x-2000)^2/(9(\log x)^2)$ for $x \ge 2000$ .
Weighting. Weighting $r(s)$ by $(\log s)^2/s$ cancels the varying factor in the sieve bound $r(s) \le 9\,C(s)\,s/(\log s)^2$ , giving a weighted first moment of at least $\tfrac{44}{100}x$ .
Second moment of $C$ . With $\sum_{s \le x,\, 2\mid s} C(s)^2 \le \tfrac{21}{2}x$ , Cauchy–Schwarz yields $\sigma(A) \ge 1/2200$ for $A = B + B$ , $B = \{(p-3)/2\}$ .
Schnirelmann's inequality with $m = 1525$ (the least $m$ with $(1 - 1/2200)^m < 1/2$ ) gives $K = 4m + 1 = 6101$ .

Significance

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $6101$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $6101$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 97041 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $97\,041$ , from the same elementary circle of ideas.

Setting

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 97\,041,\ \textstyle\sum s = n.

This is the campaign template with the value $97\,041$ filled in. The source proves the stronger statement that every odd $n \ge 194\,083$ is a sum of exactly $97\,041$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It is the argument behind the $100\,001$ entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give $\sigma(A) \ge 1/35\,000$ for $A = B + B$ , $B = \{(p-3)/2 : p \text{ odd prime}\}$ . The only change is to take the smallest admissible $m$ in Schnirelmann's inequality: $(1 - 1/35\,000)^{m} < 1/2$ first holds at $m = 24\,260$ (rather than the rounded $25\,000$ ), so $2mA = \mathbb{Z}_{\ge 0}$ and $K = 4m + 1 = 97\,041$ .

Significance

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $97\,041$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $97\,041$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Group Theory·Captain: dbenbenn

Moore: the Følner function of Thompson's group F grows faster than any tower of exponentialsResearch Paper

This mission formalizes J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651 (doi:10.4171/GGD/201; arXiv:0905.1118v7, whose page numbers are used): if Thompson's group $F$ has Følner sets at all, they are larger than any tower of exponentials.

Motivation

Whether Thompson's group $F$ is amenable is a long-standing open problem, the goal of the F-amenability mission on this platform. By Følner's criterion a finitely generated group is amenable exactly when it has Følner sets, finite sets almost invariant under translation by the generators, of every precision. Moore's theorem is unconditional: for every finite symmetric generating set there is a constant $C > 1$ such that every $C^{-n}$ -Følner set has at least $\exp_n(0)$ elements, a tower of $n$ exponentials. If $F$ is amenable, its Følner function therefore outgrows every tower, and $F$ would answer negatively Gromov's question whether some primitive recursive function dominates the Følner functions of all amenable finitely presented groups (Moore's Question 1.2, from Gromov 2008, p. 578).

Timeline.

1979: Geoghegan conjectures that $F$ is not amenable (Cannon–Floyd–Parry 1996, p. 227).
2001: Burillo, Cleary and Stein estimate word length in $F$ by the size of reduced tree diagrams (doi:10.1090/S0002-9947-00-02650-7).
2008: Gromov asks whether the Følner functions of amenable finitely presented groups are dominated by a primitive recursive function (doi:10.4171/ggd/48).
2013: Moore proves the tower lower bound for $F$ (doi:10.4171/GGD/201).

Setting

Thompson's group $F$ (CannonFloydParry.F, published) is the group of order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, all dyadic rationals, and all slopes powers of $2$ . Moore multiplies elements as " $f$ followed by $g$ "; that group, the opposite of the group of maps under composition, is MooreF, and it acts on the right.

A finite set $A \subseteq F$ is $\varepsilon$ -Følner with respect to a finite $\Gamma$ (IsFolnerSet Γ A ε) when $\sum_{\gamma \in \Gamma} |(A \cdot \gamma) \mathbin{\triangle} A| < \varepsilon |A|$ , where $A \cdot \gamma = \{a \gamma : a \in A\}$ . The tower function is $\exp_0(n) = n$ , $\exp_{p+1}(n) = 2^{\exp_p(n)}$ (ThompsonAmenability.towerExp, published). The Følner function $\mathrm{Føl}_{F,\Gamma}(n)$ (folnerFunction) is the least size of a $1/n$ -Følner set, and $\infty$ if there is none.

The proof works with finite rooted binary trees, recorded as the sets of addresses of their leaves (IsTree), on which $F$ acts partially by acting on the addresses (treeAct), and with weighted Følner sets and marginal sets for partial actions of a group (IsWeightedFolner, IsMarginal). These are defined in the two definitions items.

Formalization targets

Goal: Theorem 1.1

For every finite symmetric generating set $\Gamma$ of $F$ there is $C > 1$ such that, for every $n$ ,

A \text{ is } C^{-n}\text{-Følner} \implies |A| \ge \exp_n(0).

The goal is the published F-amenability milestone ThompsonAmenability.exists_const_forall_isFolner_le_card, for the product of maps by composition and left translates; a milestone states the same theorem in Moore's conventions, and another states its second sentence, that $\mathrm{Føl}_{F,\Gamma}$ is not eventually dominated by any $\exp_p$ .

Milestones

Every numbered result of §§3–5 (Lemmas 3.4, 3.5, 3.9–3.12, 3.14, 3.15, 4.1, 4.2, 5.2, 5.4, 5.5, 5.7, 5.9, 5.10, 5.12, 5.13, Remark 3.8 and Claim 5.14), the unnumbered facts about trees and tree diagrams stated in §2, and the word-length bound Moore cites from Burillo, Cleary and Stein.

Significance

The result. The theorem constrains any proof that $F$ is amenable: Følner sets of $F$ , if they exist, cannot be found by any search whose size is bounded by a tower of fixed height. If $F$ is amenable, it answers Gromov's question negatively. If $F$ is not amenable, the bound is vacuous but its method, controlling how Følner sets distribute over tree diagrams, is one of the few quantitative tools on the problem.

Formalizing it. None of the paper is formalized. The general theory of §3 (partial actions, weighted Følner sets, marginal sets) applies to any group acting partially on a set and is reusable; the partial action of $F$ on binary trees is the natural model for combinatorial arguments about $F$ .

Difficulty

The difficulty is quantitative. A Følner set is defined only by an inequality between counts, and nothing in that inequality forces its elements to be large; yet the bound must hold for every Følner set, with a single constant $C$ for all $n$ , while the height of the tower grows with $n$ . Any argument can therefore afford to lose only a constant factor in the Følner constant for each level of the tower.

Formalization scope

Lean representation and conventions.

Moore's $F$ is (CannonFloydParry.F)ᵐᵒᵖ, so products and right translates match the paper; the goal is stated for CannonFloydParry.F with left translates.
Trees are finite sets of binary sequences (List Bool). Tree diagrams, their maps on sequences, equivalence and reducedness follow Moore's §2; a tree diagram describes an element of the published $F$ through the dyadic intervals of its leaves, and Moore's sentence defining $F$ as the reduced tree diagrams is a milestone.
A partial action is an Option-valued function, and the action of $F$ is defined on all finite sets of sequences; on trees it is Moore's action.
Weighted Følner sets are finitely supported non-negative functions; sums over $S$ are finite sums over their supports.

What is left out, and deviations.

Question 1.2 (Gromov's question) and Remark 5.11 (consequences for invariant measures on trees, not used in the proof) are not formalized.
In Definition 3.1, Moore's "for which all computations involving $\cdot$ are defined" can be read two ways. It is read here as asserting that $x \cdot (gh)$ is defined whenever $x \cdot g$ and $(x \cdot g) \cdot h$ are (Exel's composition law for partial actions), which Moore's proof of Lemma 3.5 uses and the action of $F$ on trees satisfies. On the weaker reading, equality only where all three are defined, Lemmas 3.5, 3.9, 3.10 and 3.12 fail (the note on the §3 definitions links p2m theorems proving this).
Definition 3.13 is read with the joining chain staying inside the set; the literal reading makes every subset of a group acting on itself by right multiplication $\Gamma$ -connected for a symmetric generating set $\Gamma$ .
Lemmas 3.5 and 3.9 assume $g \ne e$ , where the strict inequalities fail; Claim 5.14 bounds the reduced diagram, where "a tree diagram" would be vacuous. Each is explained in the milestone's statement.
The word-length bound is cited: Burillo, Cleary and Stein prove it for elements with positive normal form, and Moore applies it to all of $F$ .

What a development needs. Tree diagrams, normal forms and generation of $F$ are published and proved on this platform (the Cannon–Floyd–Parry missions on tree diagrams and the normal form and the two presentations of $F$ ); Følner's criterion is published by Garrido's first mission. New are the combinatorics of binary trees as leaf sets, the bridge between them and the published tree diagrams, and the theory of §3. Proofs of any milestone are welcome.

Selected references

J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
J. Burillo, S. Cleary, M. I. Stein, Metrics and embeddings of generalizations of Thompson's group F, Trans. Amer. Math. Soc. 353 (2001) 1677–1689. doi:10.1090/S0002-9947-00-02650-7
R. Exel, Partial actions of groups and actions of inverse semigroups, Proc. Amer. Math. Soc. 126 (1998) 3481–3494. doi:10.1090/S0002-9939-98-04575-4
M. Gromov, Entropy and isoperimetry for linear and non-linear group actions, Groups Geom. Dyn. 2 (2008) 499–593. doi:10.4171/ggd/48

36 thms1 active userReviewed

Completed

Group Theory·Captain: burkh4rt

Local conjugacy in prosolvable groupsResearch Paper

Motivation

Two closed subgroups $H$ and $H'$ of a profinite group $G$ are locally conjugate if, for every prime $p$ , a Sylow $p$ -subgroup of $H$ is conjugate in $G$ to a Sylow $p$ -subgroup of $H'$ . Conjugate subgroups are always locally conjugate. The converse, which lets conjugacy be tested one prime at a time, fails in general. Deciding when it holds is a classical question about supplements of nilpotent normal subgroups.

1964. Glauberman: if $G = NJ$ acts on a set with $N$ transitive and $|N|$ , $|J|$ coprime, then $J$ fixes a point ([Glauberman 1964], Thm. 4).
1979. Losey and Stonehewer: in a finite solvable group, two locally conjugate supplements of a nilpotent normal subgroup $N$ are conjugate if (A) $G/N$ is nilpotent, (B) $N$ is abelian, or (C) the Sylow subgroups of $G$ have class at most two. They also exhibit $S_3$ acting on $Q_8$ inside $GL(2,3)$ , where the converse fails.
1988. Evans and Shin: for abelian $N$ , solvability of $G$ is not needed.
1995. Shin: Losey and Stonehewer's results hold for profinite $G$ and nilpotent $N$ .

Groups, local conditions, and cohomology

A profinite group is a compact Hausdorff totally disconnected topological group. Equivalently, it can be described through compatible finite quotient groups. A pronilpotent group has nilpotent finite continuous quotients. A prosupersolvable group has supersolvable finite continuous quotients; a finite group is supersolvable when it admits a normal series with cyclic factors. These properties concern all finite continuous quotients, with no uniform bound on their orders or nilpotency classes.

A subgroup $H$ supplements a normal subgroup $N$ when $NH=G$ . It complements $N$ when, in addition, $N\cap H=1$ . Two closed subgroups are locally conjugate when, for each prime $p$ , a Sylow $p$ -subgroup of one is conjugate in $G$ to a Sylow $p$ -subgroup of the other. For profinite groups, Sylow subgroups are maximal closed pro- $p$ subgroups. The conjugating element may depend on the prime. All subgroup notation in the paper carries closedness, as stipulated in §1.2.

The cohomological statements concern a profinite group $J$ acting continuously by automorphisms on a discrete group $N$ . With a left action, a continuous cocycle satisfies $f(xy)=f(x)(x\cdot f(y))$ . Two cocycles are equivalent when $g(x)=n^{-1}f(x)(x\cdot n)$ for one fixed $n\in N$ . Their quotient is the pointed set $H^1(J,N)$ , whose distinguished point is the identity cocycle. Stable classes on a subgroup compare a cocycle with its conjugates after restriction to the relevant intersections. This matters when the subgroup itself is not normal. The definitions follow §§1–1.2.

Formalization targets

The central conjugacy assertion is Theorem 1.1. For a closed normal pronilpotent subgroup $N$ of a profinite group $G$ , assume that $G$ is prosupersolvable or $G/N$ is pronilpotent. Then closed supplements $H,H'$ of $N$ satisfy

H\sim_G H'\quad\Longleftrightarrow\quad H\text{ and }H'\text{ are locally conjugate}.

Lemma 1.2 asserts, for finite nilpotent coefficients and its stated structural alternatives, a pointed bijection induced by simultaneous restriction:

H^1(J,N)\cong\prod_{p\in\pi(J)}\operatorname{inv}_J H^1(J_p,N).

The other numbered targets are Corollaries 1.3–1.4 and Propositions 2.1–2.3, 3.1–3.2, and 4.1–4.2. They retain the paper's distinctions between finite coefficients, locally finite discrete coefficients, and arbitrary closed pronilpotent subgroups. They also retain the normal-intersection condition in the semidirect-product inclusion and fixed-point results. The abelian conclusions impose no solvability assumption on the ambient profinite group.

Both counterexamples in §1 are targets. The quaternion example realizes $Q_8\rtimes S_3$ in $GL(2,3)$ , has exactly two global cohomology classes and trivial Sylow cohomology, and exhibits locally conjugate complements that are not conjugate. The Heisenberg example uses $C_3\wr S_3$ of order $162$ , with $N$ the Heisenberg group of order $27$ , $J\cong C_6$ , and $H\cong C_3\times S_3$ . Local containment holds while containment of a conjugate of $J$ fails.

The combined goal asserts all eleven numbered results and both counterexamples. Each assertion remains a separate milestone with the source's numbering or, for the unnumbered counterexamples, its section and page.

What a completed formalization provides

The conjugacy and containment theorems make precise when separate prime-wise witnesses can be replaced by one global witness. The fixed-point results similarly turn prime-wise fixed points, which can be different points, into a point fixed by the full subgroup. The counterexamples record the limits of these conclusions under weakened hypotheses. These are proved mathematical results of the preprint, rather than new conjectures.

A completed development would also provide reusable formal interfaces for continuous nonabelian first cohomology, stable classes, profinite Sylow and Hall conditions, and local subgroup relations. An earlier local Lean development supplies definitions and substantial proof material. The present draft statements are aligned to the arXiv version; their target proofs remain open in this proposal. Reusing earlier proofs requires checking their types against these interfaces and the pinned environment.

What makes the statements demanding

Local conjugators can vary with the prime, and there need not be one conjugator that works for all primes simultaneously. The quaternion example demonstrates this obstruction even in finite groups. Nonabelian cohomology is a pointed set, so the usual additive primary-decomposition language does not itself provide the needed assertion. The transition from finite groups to profinite groups also requires tracking topology, closedness, and continuity. The counterexamples and the finite-versus-profinite distinctions are part of the mathematical scope, not optional simplifications. See §§1–3.

Formalization scope and conventions

All declarations use the namespace LocalConjugacy. Profinite ambient groups use Mathlib's ProfiniteGrp; subgroups, quotient groups, normality, complements, actions, fixed points, finite Sylow subgroups, nilpotence, and solvability use Mathlib structures or predicates. Custom definitions cover the continuous nonabelian quotient and the profinite local conditions absent from the pinned library interface. Conjugation is written on the left. This changes the notation for the conjugating element, not the conjugacy or inclusion assertion.

The fixed-point targets quantify over nonempty sets with no added topology and require closed stabilizers. Propositions 2.1–2.2 allow infinite locally finite discrete coefficients. Theorem 1.1 allows arbitrary closed pronilpotent $N$ . Finite special cases cannot replace these targets. Both counterexamples include explicit isomorphisms to the concrete groups named in the paper. Contributions may reuse the existing proof development, improve the reusable interfaces, or prove the targets directly while preserving these statements.

Selected references

M. C. Burkhart, Local conjugacy in prosolvable groups, preprint, 2026. https://arxiv.org/abs/2609.37678
G. O. Losey and S. E. Stonehewer, Local conjugacy in finite soluble groups, Quart. J. Math. Oxford (2) 30 (1979), 183–190.
M. J. Evans and H. Shin, Local conjugacy in finite groups, Arch. Math. 50 (1988), 289–291.
H. Shin, A conjugacy theorem in profinite groups, Bull. Korean Math. Soc. 32 (1995), 139–144.
G. Glauberman, Fixed points in groups with operator groups, Math. Z. 84 (1964), 120–125.
L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Springer, 2010.
J.-P. Serre, Galois Cohomology, Springer, 2002.

18 thms1 active userReviewed

Completed

Category Theory Quantum Information·Captain: Bingyu Xia

Categorical Quantum Mechanics II: The Born RuleTextbook

Motivation

Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism $I \to A$ , an effect is a morphism $A \to I$ , and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.

This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.

Setting

Fix a monoidal dagger category $\mathcal{C}$ with zero morphisms. The unit object $I$ carries a commutative monoid structure $\mathrm{End}(I)$ — the scalars. For a state $a : I \to c$ and an effect $x : c \to I$ , the probability that $x$ occurs on $a$ is the scalar

\mathrm{Prob}(a,x) \;=\; a^\dagger \circ x^\dagger \circ x \circ a .

A family of effects $x : I \to \mathrm{Eff}(c)$ is complete when the induced map $\langle x \rangle : \bigoplus_i I \to c$ satisfies $\bigvee_i x_i = \mathrm{id}_c$ , and disjoint when $x_i^\dagger \circ x_j = 0$ for $i \neq j$ . Both conditions are stated for a dagger biproduct of the unit objects.

Formalization targets

Goal — the Born rule

\sum_{i} \mathrm{Prob}(a, x_i) \;=\; \mathrm{id}_I \qquad \text{for } x \text{ complete and disjoint}

This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.

Supporting results

Lemma 2.52. A family of effects is disjoint if and only if the dagger of its lift is an isometry; and complete if and only if the kernel of its lift is trivial.
Lemma 2.53. A complete and disjoint family of effects lifts to a unitary $\langle x \rangle : \bigoplus_i I \to c$ .
Lemma 2.41, Corollary 2.42. Dagger biproducts: transposing a matrix of morphisms daggers every entry, and daggers distribute over addition.

Significance

The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in $\mathbf{Hilb}$ , to the usual $\sum_i |\langle x_i | a \rangle|^2 = 1$ . Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.

The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.

Difficulty

Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.

Formalization scope

Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts (§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has no dagger-category theory at all, so the definitions are supplied from scratch as Lean Definitions and are importable independently of this mission.

Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.

Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity $x^\dagger \circ x = \mathrm{id}$ on $A$ to Lemma 2.52, whereas Lemma 2.52 only gives the identity on $\bigoplus_i I$ ; the identity on $A$ is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.

Selected references

D. Reutter and J. Vicary, Categorical Quantum Mechanics, §2.3.3 and §2.4.3.
S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, LICS 2004.
The Mathlib CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category API, on which the definitions are built.

9 thms1 active userReviewed

Completed

Functional Analysis·Captain: savarin

Sharp diagonal Hlawka constants: foundation and proved cutoff 256Research Paper

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission establishes the best possible constant for complex diagonal matrices for every real $p\ge256$ . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.

The constant comes from a simple family of three $3\times3$ diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.

This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real $p\ge90$ ; the campaign invites further improvements.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library

Established results on Prove2Me

59 thms1 active userReviewed

Completed

Machine Learning·Captain: Minghui

DARE the Extreme: Output Concentration under Delta-Parameter PruningResearch Paper

Random pruning changes more than the expected output

A fine-tuned model can be stored as a pretrained model together with its parameter changes. Pruning these delta parameters reduces the amount of task-specific information to store. The DARE procedure independently deletes each change with probability $p$ and multiplies every surviving change by $1/(1-p)$ . This preserves the expected linear-layer output, but a single pruned model can still differ substantially from that expectation.

Deng and coauthors investigate this distinction in DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025. The paper motivates changes to the rescaling rule and to fine-tuning regularization. This mission focuses on its finite-sample mathematical analysis: the relation between random pruning, coefficient energy, and output concentration. Its goal is the Kearns–Saul bound in Appendix E.1, equation (8), PDF p. 30, expressed through the coefficient statistics used in Section 3.2.

The distinction between that appendix result and the printed Theorem 3.1 matters. The mission does not assert the latter's piecewise formula. Its low-pruning branch omits the square root present in equation (8), and its high-pruning branch applies a one-sided refinement to a two-sided event. The exact target below retains the appendix's valid bound across the entire interval $0<p<1$ .

A fixed layer and a random mask

Fix one output coordinate of a linear layer, an input vector $x$ , and a delta-weight row $\Delta W$ . There are $n>0$ input coordinates. Define the deterministic influence coefficients $c_j=\Delta W_jx_j$ , their sum $S=\sum_jc_j$ , and their energy $Q=\sum_jc_j^2$ . Equivalently, the formal statements quantify over every real coefficient vector $c$ ; choosing $x_j=1$ realizes every such vector in the layer model.

The only randomness is the pruning mask. Write $\omega_j=1$ for a dropped coordinate, with mutually independent $\omega_j\sim\operatorname{Bernoulli}(p)$ . A mask has probability

w_p(\omega)=\prod_{j=1}^n\begin{cases}p,&\omega_j=1,\\1-p,&\omega_j=0.\end{cases}

Expectations and event probabilities are the finite weighted sums against $w_p$ . A surviving coordinate is rescaled by $1/q$ , where $q>0$ . The output error, original minus pruned, is

H_q(\omega)=\sum_jc_j\left(1-\frac{1-\omega_j}{q}\right).

DARE uses $q=1-p$ ; denote its error by $H$ . This is the retention-mask formulation in Section 3.2, equation (2), PDF p. 5, with $\delta_j=1-\omega_j$ . The empirical coefficient mean and variance are $\bar c=S/n$ and $\sigma^2=n^{-1}\sum_j(c_j-\bar c)^2$ . These statistics describe a fixed vector, not another source of randomness.

Formalization targets

Define the concentration coefficient with its removable singularity filled in:

\Phi(p)=\begin{cases}\frac12,&p=\frac12,\\\frac{1-2p}{\log((1-p)/p)},&p\ne\frac12.\end{cases}

For every $0<p<1$ and failure probability $0<\gamma<1$ , the goal is

\boxed{\Pr\left\{|H|\le\frac{\sqrt{\Phi(p)}}{1-p}\sqrt{n(\bar c^2+\sigma^2)}\sqrt{\log(2/\gamma)}\right\}\ge1-\gamma.}

This is Appendix E.1, equation (8), PDF p. 30, followed by the unnumbered energy identity on PDF p. 31. Zero coefficients are included: no positive-energy assumption is attached to the goal.

Four supporting milestones state the following results.

Coefficient statistics: $Q=n(\bar c^2+\sigma^2)$ for $n>0$ , as used in the final algebraic step of Appendix E.1, PDF p. 31.
Exact moments: for $0\le p\le1$ and $q>0$ , let $b_q=(1-(1-p)/q)S$ . Then $\mathbb EH_q=b_q$ , $\mathbb E(H_q-b_q)^2=p(1-p)Q/q^2$ , and $\mathbb EH_q^2=b_q^2+p(1-p)Q/q^2$ . This is a paper-derived extension of the calculations on PDF p. 29 to the general rescaling model introduced in Appendix E.2, PDF p. 31. In particular, DARE has mean zero and mean square $pQ/(1-p)$ .
Kearns–Saul exponential moment: $0<\Phi(p)\le1/2$ and, for every real $t$ ,

(1-p)e^{-tp}+pe^{t(1-p)}\le e^{\Phi(p)t^2/4}.

The analytic input is Berend–Kontorovich, Section 3, Theorem 4, equation (6), PDF pp. 3–4. The bound on $\Phi$ is also stated in the DAREx appendix on PDF p. 30. 4. Exponential output tail: for $Q>0$ and $t>0$ ,

\Pr\{|H|>t\}\le2\exp\left(-\frac{t^2(1-p)^2}{\Phi(p)Q}\right).

This is the unnumbered display immediately preceding equation (8), PDF p. 30.

What the result establishes

The target quantifies the error of a randomly selected pruned layer in terms of its actual influence coefficients. It distinguishes preserving an expectation from controlling a realization. The moment identities also expose the bias introduced by choosing a rescaling denominator different from $1-p$ .

Formalization supplies a precise probability model and checks every coefficient, sign, and exceptional case. The finite mask model and its normalization already compile locally with proofs. The five milestone and goal statements have been elaborated, but their theorem proofs remain open. Completing this mission would formalize the selected appendix result; it would not establish the paper's experimental accuracy claims, a whole-network guarantee, or an optimal rescaling rule.

Why the tail direction matters

Signed coefficients require exponential-moment control for both positive and negative arguments. The sharper estimate in Berend–Kontorovich, Lemma 5, equation (9), PDF p. 4 has a nonnegative-argument restriction. Using it for an unrestricted absolute tail loses an essential hypothesis.

For example, with $n=1$ , $c_1=1$ , $p=99/100$ , and $\gamma=1/200$ , the error is $1$ with probability $99/100$ and $-99$ with probability $1/100$ . The printed Theorem 3.1 threshold is $\sqrt{198\log400}<99$ , so its failure probability exceeds $\gamma$ . This concrete source audit is the reason for selecting equation (8), not a claim that the printed theorem has been formally disproved in Lean.

Formalization scope

The Lean model uses real coefficients indexed by Fin n and Boolean functions for masks. Nonnegative masses and normalization are proved from the product formula; concentration is never assumed in a structure field. Fixed weights and inputs are external data. Random training, dependence between masks, nonlinear activations, structural pruning, and empirical validation are outside this mission.

The main goal requires $n>0$ for the empirical statistics, $0<p<1$ for DARE rescaling, and $0<\gamma<1$ for the confidence level. The moments permit empty coefficient vectors and endpoint probabilities because they use a separate positive $q$ . The exponential-tail milestone requires $Q>0$ to avoid division by zero; the main goal includes $Q=0$ . The value $\Phi(1/2)=1/2$ is explicit. No theorem relies on Lean's total division or logarithm to supply a missing analytic hypothesis.

Selected references

Wenlong Deng, Yize Zhao, Vala Vakilian, Minghui Chen, Xiaoxiao Li, Christos Thrampoulidis. DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models. ICLR 2025. arXiv:2410.09344v2. Section 3.2, PDF p. 5, equation (2), Theorem 3.1; Appendix E.1, PDF pp. 28–31, Theorem E.1 and equations (6)–(8); Appendix E.2, PDF p. 31, initial unnumbered rescaling identity.
Daniel Berend and Aryeh Kontorovich. On the Concentration of the Missing Mass. Electronic Communications in Probability 18 (2013). arXiv:1210.3248v1. Section 3, PDF pp. 3–4, Theorem 4 and equation (6); Lemma 5 and equation (9) explain the excluded one-sided refinement.

6 thms1 active userReviewed

Completed

Group Theory·Captain: dbenbenn

Cannon–Floyd–Parry: Thurston's piecewise integral projective models of F and TTextbook

This mission formalizes §7 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: W. Thurston's interpretations of Thompson's groups $F$ and $T$ as groups of piecewise integral projective homeomorphisms of the interval and the circle.

Motivation

The notes describe their last section as follows: "In §7 we give W. Thurston's interpretations of $F$ and $T$ in terms of piecewise integral projective homeomorphisms" (p. 216). Elements of $F$ and $T$ are piecewise linear, with dyadic breakpoints and slopes powers of $2$ . Thurston's models replace the linear pieces by linear fractional maps $t \mapsto (at + b)/(ct + d)$ with integer matrices of determinant $\pm 1$ , and the dyadic intervals by the intervals of the Farey tree. The two descriptions give isomorphic groups because both are read off the same tree diagrams.

Earlier missions on this platform formalize $F$ (§1 and §4), its tree diagrams (§2), its presentations (§3) and the group $T$ (§5); this one states their projective models.

Setting

The simplex. $\Delta_n$ (Simplex n) is the standard $n$ -simplex in $\mathbb{R}^{n+1}$ , and $\rho(x) = x / \sum_i |x_i|$ (rho). A map on $U \subseteq \Delta_n$ is integral projective (IsIntegralProjective) when it is $\rho \circ A$ for some $A \in GL(n+1, \mathbb{Z})$ with $A(U)$ in the nonnegative orthant (p. 249). Subdivisions of $\Delta_n$ are Mathlib's geometric simplicial complexes (Geometry.SimplicialComplex), finite and with underlying space $\Delta_n$ ; a subdivision is rational or integral when each $n$ -simplex has rational vertices, or is the image of $\Delta_n$ under an integral projective map. lift and ind are the primitive integer lift of a rational point and the index of a rational simplex (p. 250).

PIP maps. $PIP(\Delta_n)$ (PIPSet n) is the set of homeomorphisms of $\Delta_n$ that are integral projective on each simplex of some integral subdivision. $PIP^+(\Delta_n)$ (PIPPlusSet n) consists of the orientation-preserving ones; in Lean orientation is read off the pieces, which are required to be $\rho \circ A$ with $\det A = 1$ .

The interval and the circle. On p. 251 the notes move $\Delta_1$ to $\Delta_1' = \{(t, 1)\}$ and identify it with $[0,1]$ . There a map is integral projective (IsIntegralProjective01) when it is $t \mapsto x/y$ with $(x, y) = A(t, 1)$ , $A \in GL(2, \mathbb{Z})$ and $0 \le x \le y$ . An interval $[a/b, c/d]$ is recorded by four natural numbers (FracInterval), with left part $[a/b, (a+c)/(b+d)]$ and right part $[(a+c)/(b+d), c/d]$ , and fareyNode follows a path of left and right steps from $[0,1]$ down the tree $\mathcal{T}'$ of integral subsimplices. $PIP^+$ of $[0,1]$ (PIPPlus01Set) consists of the order isomorphisms of $[0,1]$ that are integral projective on each interval of an integral partition, and RepresentsPIP reads a §2 tree diagram on $\mathcal{T}'$ instead of on the dyadic tree. $PIP^+(S^1)$ (PIPPlusCircleSet) consists of the permutations of UnitAddCircle with an order-preserving lift to $\mathbb{R}$ commuting with $x \mapsto x + 1$ that is integral projective, up to an integer, on each interval of an integral partition of $[0,1]$ , the way the published $T$ is defined through lifts.

Target

The goal is Theorem 7.3 (p. 254),

T \cong PIP^+(S^1),

together with the sentence that follows it, which names the three maps of $PIP^+(S^1)$ corresponding to $T$ 's generators $A$ , $B$ , $C$ : the goal asks for an isomorphism sending them to exactly those maps (pipA, pipB, pipC).

The milestones follow the section. For $\Delta_n$ : integral projective maps are homeomorphisms onto their images, $PIP(\Delta_n)$ is closed under inversion, two integral subdivisions have a common rational refinement (the notes cite Rourke and Sanderson), the index of a rational simplex, Theorem 7.1 (every rational subdivision refines to an integral one), $PIP(\Delta_n)$ is a group, and $PIP^+(\Delta_n)$ has index $2$ in it. For the interval: $PIP^+(\Delta_1)$ is isomorphic to its model on $[0,1]$ ; $[a/b, c/d]$ is an integral subsimplex exactly when $ad - bc = -1$ ; left and right parts are integral; $\mathcal{T}'$ is an ordered rooted binary tree; integral projective maps between integral subsimplices are unique and given by an explicit formula; they restrict to, and are glued from, maps of the left and right parts; reduced tree diagrams correspond bijectively to $PIP^+$ of $[0,1]$ ; and Theorem 7.2, $F \cong PIP^+(\Delta_1)$ .

Significance

The result. Thurston's description identifies $F$ and $T$ with groups of piecewise $PSL(2, \mathbb{Z})$ maps of the interval and the circle, the dyadic tree becoming the Farey tree. The same substitution carries each element of $F$ or $T$ to its projective model; the conjugating map is Minkowski's question mark function.

Formalizing it. Nothing on this platform or in Mathlib concerns piecewise projective groups, the Farey tree of intervals or Minkowski's function. The mission reuses the published $F$ , $T$ and the tree diagrams of §2.

Difficulty

Theorem 7.1 is the one argument in the section that is not about the interval: a descent on the index, starring a rational subdivision at a well-chosen rational point. Mathlib has geometric simplicial complexes but no subdivisions, starring or common refinements, so both Theorem 7.1 and the cited results of Rourke and Sanderson need that apparatus built. The interval half is elementary number theory of $2 \times 2$ integer matrices (the notes' proof of connectedness of $\mathcal{T}'$ is a Euclidean-algorithm descent), followed by the tree-diagram argument of §2 repeated on $\mathcal{T}'$ .

What is left out

The Farey-tree remark on p. 252 (replacing each vertex $[a/b, c/d]$ of $\mathcal{T}'$ by the mediant $(a+c)/(b+d)$ gives the Farey tree): a relabelling that no statement uses.
The remark after Theorem 7.2 that the proof of Theorem 7.2 also proves Theorem 7.3; Theorem 7.3 is stated directly.

Formalization scope

$PIP(\Delta_n)$ and $PIP^+(\Delta_n)$ are sets of homeomorphisms Simplex n ≃ₜ Simplex n. The milestones that they are groups assert a subgroup with exactly that carrier, and Theorem 7.2 asserts such a subgroup for $PIP^+(\Delta_1)$ together with an isomorphism from $F$ .
The index-2 milestone assumes $n \ge 1$ : for $n = 0$ , $\Delta_0$ is a point and $PIP^+(\Delta_0) = PIP(\Delta_0)$ .
The converse of p. 253 (two integral projective maps of the left and right parts glue to one) is stated for maps carrying endpoints to the corresponding endpoints, the orientation the section works with; maps swapping the endpoints of both parts do not glue.
Reused platform theorems, which solutions may import: the §2 tree-diagram theorems (every tree diagram represents an element of $F$ , every element has a unique reduced tree diagram, tree diagrams compose).

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §7 pp. 249–254. doi:10.5169/seals-87877
C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Ergebnisse der Mathematik und ihrer Grenzgebiete 69, Springer, 1972. doi:10.1007/978-3-642-81735-9

25 thms1 active userReviewed

Completed

Linear algebra Machine Learning Probability·Captain: Minghui

Fine-Tuning Can Distort Pretrained Features: Perfect-Feature LP-FT SeparationResearch Paper

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$ . A feature extractor is a matrix $B\in\mathbb R^{k\times d}$ , and a head is a vector $v\in\mathbb R^k$ . Together they predict $v^\top Bx$ , with effective weight vector $B^\top v$ . The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$ , with dimension $m$ .

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$ . Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$ . Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$ . The corresponding aligned head is $u=Uv_\star$ . The dimensions satisfy $1\le k\le m$ and $m+k<d$ .

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$ . See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$ . Its mean need not be zero. Define

L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$ . Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$ . Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$ , initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$ . Establish

\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.

Linear probing, from any initial head, must converge to $u$ . Fine-tuning initialized at its limit must satisfy

v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$ , including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.

9 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 100001 PrimesResearch Paper

Motivation

Goldbach's problem asks whether every integer greater than $1$ can be written as a sum of a small number of primes. The first unconditional result of this kind was obtained by Schnirelmann around 1930: there is an absolute constant $k$ such that every integer $n > 1$ is a sum of at most $k$ primes. His argument is elementary. It uses an upper-bound sieve and Chebyshev-type prime estimates, together with a notion of additive density, and it does not need the prime number theorem or complex analysis.

The constant has since been reduced by much deeper methods. A short timeline for odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes, with an ineffective threshold in the original argument.
Ramaré (1995): every even integer is a sum of at most six primes, which gives at most seven primes for every odd $n > 1$ . (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): every odd $n > 1$ is a sum of at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes (the ternary Goldbach conjecture). (arXiv:1312.7748)

This mission targets a much weaker constant than any of these, $k = 100\,001$ . It does so because the constant comes from Schnirelmann's elementary method with every estimate made explicit, and that proof is short enough to be a realistic target for a complete formalization.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset $s$ of natural numbers such that every element of $s$ is prime, the elements of $s$ sum to $n$ , and $s$ has at most $k$ elements counted with multiplicity. Repetitions are allowed and order is irrelevant.

The number $1$ is not a sum of primes, so the question concerns odd $n \ge 3$ . Even numbers are excluded from the campaign statement.

The Schnirelmann density of a set $A \subseteq \mathbb{Z}_{\ge 0}$ is

\sigma(A) = \inf_{N \ge 1} \frac{|A \cap \{1, \dots, N\}|}{N}.

This notion is the additive tool behind the elementary approach. Mathlib provides it as schnirelmannDensity.

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 100\,001,\ \textstyle\sum s = n.

This is the campaign template of Odd numbers as sums of primes with the value $100\,001$ filled in. A stronger explicit form in the source is that every odd $n \ge 200\,003$ is a sum of exactly $100\,001$ primes; the at-most form for all odd $n > 1$ follows from it immediately.

Significance

The result itself. The bound $100\,001$ is far from the best known constants; five (Tao) and three (Helfgott) are both known on paper. Its value is that it rests on an elementary argument with every constant written out. There is no "sufficiently large" threshold and no appeal to the prime number theorem, zero-density estimates, or large-scale computation.

Formalizing it. No finite bound in this problem has a machine-checked proof on this platform yet. A proof of this goal would be the campaign's first proved value. The components are reusable beyond this mission:

Explicit Chebyshev-type bounds for $\pi(y)$ .
An explicit Selberg upper-bound sieve for the number of representations of an even number as a sum of two odd primes.
An averaged bound for the associated singular-series factor.
Schnirelmann's density inequality $\sigma(D + E) \ge \sigma(D) + \sigma(E) - \sigma(D)\sigma(E)$ .

Difficulty

The only substantial step is an upper bound for

r(s) = \#\{(p, q) : p, q \text{ odd primes},\ p + q = s\}

that is sharp up to a constant factor, namely of order $s/(\log s)^2$ times an arithmetic factor depending on the prime divisors of $s$ , with an explicit constant. The trivial bound $r(s) \le \pi(s)$ is weaker by a factor of $\log s$ . That loss makes the density of sums of two primes appear to be zero, so the additive argument cannot start. Everything after the sieve bound is short and explicit.

Formalization scope

The Lean statement is the campaign template verbatim with $100\,001$ in place of the value. It uses Multiset ℕ, Nat.Prime, and Odd n ∧ 1 < n. The statement is fixed by the campaign, and it has no vacuous hypotheses: every odd $n > 1$ is covered.

Mathlib already contains schnirelmannDensity and the fact that $\sigma(A) + \sigma(B) \ge 1$ with $0 \in A \cap B$ implies $A + B = \mathbb{N}$ . It also contains the Λ² setup of the Selberg sieve (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial-coefficient bounds. Missing, and welcome as contributions:

The explicit sieve bound for $r(s)$ .
The mean-square bound for the arithmetic factor.
Schnirelmann's inequality for $\sigma(D + E)$ .
The explicit lower bound for $\pi(y)$ in the form needed here.

Selected references

P. Pollack, Not Always Buried Deep: A Second Course in Elementary Number Theory, AMS, 2009. Chapter 6, §6, "An application to the Goldbach problem", pp. 196–201. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 22 (1995), 645–706. http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997–1038. https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
An explicit elementary constant for sums of primes, unpublished note, September 2026, Theorem 1. Source of the constant $100\,001$ (with $c_1 = 1/9$ , $c_2 = 860$ , $x_0 = e^{2000}$ , $\sigma(A) \ge 1/35\,000$ , $m = 25\,000$ ).

1 thm1 active userReviewed

Completed

Linear algebra Mathematical Physics·Captain: ShapeZero

The spectrum of the octonionic two-generator flowTextbook

Motivation

This mission is pure mathematics about objects it defines itself: an octonion multiplication built from the Fano plane of the companion mission The role postulates force exactly seven points, and the matrix of the linear map

p \;\mapsto\; p\,a + b\,p

for two unit imaginary octonions $a, b$ . It is motivated by the two-generator D8 flow $\dot\psi = \psi a + b\psi$ in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b; 02_synthesis/D8_SYNTHESIS.md). The statements below do not depend on that motivation.

Result. For $a = e_1$ and $b = c\,e_1 + s\,e_2$ with $c^2 + s^2 = 1$ , the characteristic polynomial of $M = R_a + L_b$ is

X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

With $c = \cos\theta$ , $2 - 2c = 4\sin^2(\theta/2)$ , so the eigenvalues are $0, 0, \pm 2i$ and $\pm 2i\sin(\theta/2)$ (each twice), and the ratio of the two nonzero frequencies is $1/\sin(\theta/2)$ .

What this mission does NOT prove.

Only the canonical pair. It proves the result for $a = e_1$ , $b = \cos\theta\, e_1 + \sin\theta\, e_2$ . That every pair of unit imaginary octonions at angle $\theta$ gives the same spectrum follows from the classical fact that $G_2$ acts transitively on such pairs — not formalized here.
Nothing about any model. It says nothing about which angle, if any, a physical model selects, or whether the D8 flow plays a role in one.
One orientation. The octonion table uses one orientation of the Fano lines; all valid orientations give isomorphic algebras, and the spectrum is basis-independent, but only this table is formalized.

Setting

Write $e_0 = 1, e_1, \dots, e_7$ for the standard basis of $\mathbb{R}^8$ . The imaginary unit $e_u$ ( $u = 1, \dots, 7$ ) is labelled by the Fano point $u - 1$ . For each line $\{l, l+1, l+3\}$ (mod $7$ ) of the companion mission's Fano plane RolesForceSeven.fanoLine, the product is oriented cyclically along the ordered triple $(l, l+1, l+3)$ :

e_{l+1}\,e_{l+2} = e_{l+4}, \qquad e_{l+2}\,e_{l+4} = e_{l+1}, \qquad e_{l+4}\,e_{l+1} = e_{l+2}

(unit indices mod $7$ , shifted into $1, \dots, 7$ ), with the reversed products negative, $e_u^2 = -1$ , and $e_0$ the identity. This defines OctonionD8.octTable and the bilinear product OctonionD8.omul on $\mathbb{R}^8$ .

For $a, b \in \mathbb{R}^8$ , Rmat a is the matrix of $p \mapsto p\,a$ and Lmat b the matrix of $p \mapsto b\,p$ (column $j$ is the image of $e_j$ ). The flow matrix is

M = \texttt{flowMat}\;c\;s = R_{e_1} + L_{c e_1 + s e_2}.

The Fano plane is imported from the companion mission, not restated. The reordering blockEquiv and the two blocks blockA c s, blockB c s are defined explicitly for the milestones.

Formalization targets

Goal: the characteristic polynomial

c^2 + s^2 = 1 \;\Longrightarrow\; \chi_M(X) = X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

This is OctonionD8.flow_charpoly. The hypothesis $c^2 + s^2 = 1$ is the only one, and it is needed: without it the characteristic polynomial differs.

Milestones — the proof outline

The proof goes through an invariant-subspace decomposition. Reorder the basis as $(e_0, e_1, e_2, e_4 \mid e_3, e_5, e_6, e_7)$ (OctonionD8.blockEquiv).

M1 (block-diagonal form). For all real $c, s$ , in the reordered basis $M$ is block diagonal: $M = \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}$ , with explicit $4\times4$ blocks $A$ on $(e_0, e_1, e_2, e_4)$ and $B$ on $(e_3, e_5, e_6, e_7)$ (OctonionD8.blockA, OctonionD8.blockB).
M2 (block $A$ ). If $c^2 + s^2 = 1$ , then $\chi_A(X) = X^2\,(X^2 + 4)$ .
M3 (block $B$ ). If $c^2 + s^2 = 1$ , then $\chi_B(X) = \bigl(X^2 + (2 - 2c)\bigr)^2$ .

The goal follows: the characteristic polynomial is unchanged by reordering the basis, and that of a block-diagonal matrix is the product of the blocks' characteristic polynomials.

Further results (after the goal)

It is the octonions: the norm is multiplicative. For all $p, q \in \mathbb{R}^8$ , $\sum_k (pq)_k^2 = \bigl(\sum_i p_i^2\bigr)\bigl(\sum_j q_j^2\bigr)$ — the eight-square identity, which certifies that the table defines a normed (composition) algebra, the octonions, rather than some other algebra.
The flow conserves the norm. $M^{\mathsf T} = -M$ .
An annihilating polynomial. If $c^2 + s^2 = 1$ , then $M\,(M^2 + 4)\,\bigl(M^2 + (2 - 2c)\bigr) = 0$ .

Corollary: the frequencies

For $0 < \theta < \pi$ , with $c = \cos\theta$ and $s = \sin\theta$ , the roots over $\mathbb{C}$ of the characteristic polynomial, with multiplicity, are exactly

0,\ 0,\ \pm 2i,\ \pm 2i\sin(\theta/2),\ \pm 2i\sin(\theta/2),

and $0 < \sin(\theta/2) < 1$ . So the two nonzero frequencies $2$ and $2\sin(\theta/2)$ are distinct, and their ratio is $1/\sin(\theta/2)$ . Uses $2 - 2\cos\theta = 4\sin^2(\theta/2)$ .

Significance

The result itself. It gives the spectrum of the two-generator flow for the canonical pair in closed form, for every angle, from an octonion table built on the formalized Fano plane.

Formalizing it. The spectrum had been checked numerically and symbolically only.

Numerical and symbolic cross-check (independent code)

check	result
table from the companion mission's Fano lines is a normed algebra (200 random pairs)	true
eigenvalue magnitudes $\{0 \times 2,\ 2\sin(\theta/2) \times 4,\ 2 \times 2\}$ at 5°, 30°, 60°, 76.3°, 90°, 120°, 150°	max error $1.8\times10^{-15}$
symbolic characteristic polynomial (sympy, $s^2 = 1 - c^2$ )	$X^2(X^2 + 4)(X^2 + 2 - 2c)^2$

These agree with the repository's shape_zero_tests/d8_closed_form.py (frequencies $\{0, 2\sin(\theta/2), 2\}$ to $5\times10^{-11}$ ), which uses a different octonion table.

Difficulty

Moderate. The goal needs the characteristic polynomial of an $8\times8$ matrix with symbolic entries; a direct determinant expansion is expensive. The milestones take the invariant-subspace route: the block-diagonal form (M1) is an entrywise computation from the octonion table, and each $4\times4$ block's characteristic polynomial (M2, M3) is a small determinant, reduced with $c^2 + s^2 = 1$ . The further results are large but mechanical polynomial identities (the eight-square identity; the annihilating polynomial), where the risk is performance, not ideas.

Formalization scope

Vectors are Fin 8 → ℝ; matrices are Matrix (Fin 8) (Fin 8) ℝ, with column $j$ the image of the basis vector $e_j$ .
The characteristic polynomial is Mathlib's Matrix.charpoly over $\mathbb{R}$ ; the corollary maps it to $\mathbb{C}$ and uses Polynomial.roots, a multiset, so multiplicities are part of the statement.
The table is one fixed orientation of the Fano lines; $G_2$ -invariance and other orientations are out of scope.

Selected references

Wikipedia, Octonion. https://en.wikipedia.org/wiki/Octonion
Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

11 thms1 active userReviewed

Completed

Dynamical Systems Mathematical Physics·Captain: ShapeZero

Every quadratic-force oscillator is the same oscillator in different unitsTextbook

Motivation

This mission is a statement about ordinary differential equations and nothing else. It is motivated by the scaling analysis in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b), which found that the golden ratio in an on-site quadratic well is a coordinate choice. The statements below do not depend on that motivation.

Result. For any $a \neq 0$ and any two distinct real roots $r_1 \neq r_2$ , the equation

x'' = -a\,(x - r_1)(x - r_2)

becomes exactly

z'' = -(z^2 - 1)

under one fixed shift and scaling of the value and one fixed rescaling of time. So every oscillator with a quadratic restoring force and two real roots is the same oscillator, described in different units. In particular, the golden-ratio well $x'' = -(x^2 - x - 1)$ , whose roots are $\varphi$ and $-1/\varphi$ , is the normal form in disguise: its $\varphi$ is a choice of coordinates.

What this mission does NOT prove.

Nothing about any lattice or model. It concerns a single oscillator. It does not treat coupling terms, and it says nothing about which dimensionless combinations survive in a coupled system.
Not that $\varphi$ has no meaning anywhere. It shows only that $\varphi$ in this equation is a coordinate choice.
Only solutions defined on all of $\mathbb{R}$ . Some solutions of this equation escape to infinity in finite time; the theorem concerns twice continuously differentiable functions on the whole real line. The same transformation works on intervals, but that is not formalized.
Not uniqueness of the transformation. It proves one exists.

Setting

Solutions are functions $x : \mathbb{R} \to \mathbb{R}$ that are twice continuously differentiable on all of $\mathbb{R}$ (ContDiff ℝ 2 x), with $x''$ written deriv (deriv x). The transformation is

z(\tau) = \frac{x(\tau/\omega) - m}{d},

a shift by $m$ , a scaling by $d \neq 0$ of the value, and a rescaling $t = \tau/\omega$ of time with $\omega > 0$ .

Formalization targets

Goal: one transformation for every solution

Let $a \neq 0$ and $r_1 \neq r_2$ . There are real numbers $m$ , $d$ , $\omega$ with $d \neq 0$ and $\omega > 0$ , chosen once, before any solution is considered, such that for every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ :

\bigl(\forall t,\; x''(t) = -a\,(x(t) - r_1)(x(t) - r_2)\bigr) \iff \bigl(\forall \tau,\; z''(\tau) = -(z(\tau)^2 - 1)\bigr).

This is QuadraticWell.quadratic_well_equiv. Explicitly $m = (r_1 + r_2)/2$ , $d = \pm(r_1 - r_2)/2$ with the sign chosen so that $a d > 0$ , and $\omega = \sqrt{a d}$ .

Milestones

M1 (the force in shifted, scaled form). If $r_1 \neq r_2$ and $d = \pm(r_1 - r_2)/2$ (either sign), then for every real $y$ : $-a(y - r_1)(y - r_2) = -a\,d^2\bigl(((y - m)/d)^2 - 1\bigr)$ with $m = (r_1 + r_2)/2$ .
M2 (the sign can be chosen). If $a \neq 0$ and $r_1 \neq r_2$ , then $a (r_1 - r_2)/2 > 0$ or $a (r_2 - r_1)/2 > 0$ — so $\omega = \sqrt{a d}$ is real and positive for one choice of $d$ .
M3 (chain rule for the rescaling). For $x$ twice continuously differentiable, $\omega \neq 0$ and $d \neq 0$ , the second derivative of $\tau \mapsto (x(\tau/\omega) - m)/d$ at $\tau$ is $x''(\tau/\omega)/(\omega^2 d)$ .

The goal combines them: by M1 the equation reads $x'' = -a d^2 (y^2 - 1)$ with $y = (x - m)/d$ ; by M3 this becomes $z'' = -(a d/\omega^2)(z^2 - 1)$ ; and $\omega^2 = a d$ , available by M2, gives $z'' = -(z^2 - 1)$ . The converse uses $\tau = \omega t$ .

Corollary: the golden-ratio well

For every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ , $x'' = -(x^2 - x - 1)$ everywhere if and only if

z(\tau) = \frac{x(\tau/\omega) - \tfrac12}{\sqrt5/2}, \qquad \omega = \sqrt{\sqrt5/2},

satisfies $z'' = -(z^2 - 1)$ everywhere. This is the explicit instance with roots $\varphi$ and $-1/\varphi$ : $m = \tfrac12$ , $d = \sqrt5/2$ .

Significance

The result itself. It shows that the only content of a quadratic restoring force with two real roots, for a single oscillator, is the normal form $z'' = -(z^2 - 1)$ ; the roots and the stiffness are units.

Formalizing it. The equivalence had been checked numerically only.

Cross-check (independent code)

check	result
M1 identity, both signs of $d$ (sympy)	exact
golden-ratio well: $m$ , $d$ , $\omega$	$\tfrac12$ , $\sqrt5/2$ , $(\sqrt5/2)^{1/2} = 1.057371$
$z(\tau) = (x(\tau/\omega) - m)/d$ against a direct solution of $z'' = -(z^2 - 1)$ , 400 points	max difference $6.9\times10^{-13}$
a case needing the sign flip ( $a = -2$ , roots $3$ and $-1$ )	$a h = -4 < 0$ , so $d = -h$ gives $a d = 4 > 0$

These agree with the repository's shape_zero_tests/scale_invariance.py (runs at four unit choices agreeing to $1.3\times10^{-14}$ ).

Difficulty

Low–moderate. M1 and M2 are short. M3 is the only fiddly part: Mathlib's chain rule for a composition with $\tau \mapsto \tau/\omega$ , applied twice, needs the differentiability of $x$ and of $x'$ that ContDiff ℝ 2 supplies. The goal and corollary then follow by rewriting.

Formalization scope

Solutions are functions on all of $\mathbb{R}$ , twice continuously differentiable; the derivative is Mathlib's deriv.
$m$ , $d$ and $\omega$ are existentially chosen before the solution $x$ , so one transformation serves every solution.
The hypotheses of the goal are exactly $a \neq 0$ and $r_1 \neq r_2$ .

Selected references

Wikipedia, Nondimensionalization. https://en.wikipedia.org/wiki/Nondimensionalization
Wikipedia, Golden ratio. https://en.wikipedia.org/wiki/Golden_ratio
Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

5 thms1 active userReviewed

Completed

Combinatorics·Captain: mysticflounder

Eliahou–Revuelta Schur degree: L(4) = 16 and 49 ≤ L(5) ≤ 65Research Paper

Motivation

A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number $S(n)$ is the largest $N$ such that $\{1, \dots, N\}$ can be partitioned into $n$ sumfree sets; only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known. For $n \ge 4$ the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was $S(n) \le R_n(3) - 2$ , where the Ramsey number $R_n(3)$ is the least $N$ such that every $n$ -colouring of the edges of the complete graph $K_N$ has a monochromatic triangle. The Ramsey numbers satisfy $R_n(3) \le n\,(R_{n-1}(3) - 1) + 2$ for $n \ge 2$ (Greenwood–Gleason 1955); for $S(n)$ the paper knows no recursive upper bound.

Eliahou and Revuelta proposed a conjectural one. They defined a number $L(n)$ through the Schur degree of block-sum sets, proved $S(n) \le n\,L(n)$ (Theorem 5.4) and $S(n-1) + 1 \le L(n) \le R_{n-1}(3) - 1$ (Proposition 5.3), and conjectured $L(n) = S(n-1) + 1$ (Conjecture 5.6). This would give $S(n) \le n\,(S(n-1) + 1)$ (Conjecture 5.7) and $S(6) \le 966$ (Conjecture 5.8), against the range $536 \le S(6) \le 1836$ that they give. For $n = 4$ they proved $14 \le L(4) \le 16$ , conjectured $L(4) = 14$ , and left the value open.

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and the recursive bound above.
1961: Baumert computes $S(4) = 44$ (cited by Eliahou–Revuelta as reference [2]).
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, rev. 18).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (arXiv:1711.08076).
2020–2021: Eliahou and Revuelta, preprint arXiv:2006.01502 and refereed version, with the same numbering of the items used here.
2026: McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (Zenodo, doi:10.5281/zenodo.22987189), proves $L(4) = 16$ and $L(5) \ge 49$ ; its Lean library ClassicalSchur formalizes both, with $L(5) \le 65$ .

Setting

All numbers are natural numbers, except in the group $G$ below.

Sumfree sets. A set $S$ is sumfree when the sum of two of its elements, equal or distinct, is never in $S$ . A set $X$ is covered by $n$ sumfree sets when it lies in the union of $n$ sumfree sets.

Schur degree. The Schur degree $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $n$ sumfree sets cover $X$ . If there is no such $n$ , it is $\infty$ .

For example, $\operatorname{sdeg}(\{1, \dots, N\}) \le n$ holds for $N \le S(n)$ and fails for $N > S(n)$ .

Block sums. Let $A = (a_1, \dots, a_L)$ be a finite sequence of length $|A| = L$ . Its block sums are the sums of runs of consecutive entries:

a_i + a_{i+1} + \dots + a_j \qquad (1 \le i \le j \le L).

The set of these sums is $\hat A$ . The average of $A$ is the rational number $\mu(A) = (a_1 + \dots + a_L)/L$ .

The number $L(n)$ . A length $L$ has the ER property for $n$ when every sequence $A$ of $L$ positive integers with $\mu(A) \le n$ has $\operatorname{sdeg}(\hat A) \ge n$ .

For $n \ge 2$ , the inequality $\operatorname{sdeg}(\hat A) \ge n$ holds when no $n - 1$ sumfree sets cover $\hat A$ . It fails when some $n - 1$ sumfree sets cover $\hat A$ .

The number $L(n)$ is the least $L \ge 1$ with the ER property for $n$ .

The pigeonhole bound. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$ . The first values are $\rho(1) = 3$ , $\rho(2) = 6$ , $\rho(3) = 17$ and $\rho(4) = 66$ .

For $k \ge 1$ , $\rho(k)$ is an upper bound for the Ramsey number: $R_k(3) \le \rho(k)$ , with equality for $k \le 3$ .

The group $G$ . Let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$ . A set $C \subseteq G$ is sumfree in $G$ when the sum in $G$ of two of its elements, equal or distinct, is never in $C$ .

The lifted sequence. Take $m_1 \ge 1$ and $M \ge m_1$ . Write the $m_1 m_2$ numbers $u + Mj$ , with $0 \le u < m_1$ and $0 \le j < m_2$ , in increasing order:

x_0 < x_1 < \dots < x_{m_1 m_2 - 1}.

The lifted sequence is the sequence of the $m_1 m_2 - 1$ gaps between consecutive terms, $x_1 - x_0, \dots, x_{m_1 m_2 - 1} - x_{m_1 m_2 - 2}$ . Lemma 4.1 below uses it to turn a cover of $G \setminus \{0\}$ into a sequence in ℕ.

Lean names.

SumFree S: $S$ is sumfree.
CoveredBySumFree X n: $X$ is covered by $n$ sumfree sets.
sdeg X : ℕ∞: the Schur degree, with ⊤ for $\infty$ .
blockSums A and average A, for A : List ℕ: $\hat A$ and $\mu(A)$ .
ERProperty n L: the length $L$ has the ER property for $n$ .
erL n: $L(n)$ .
ramseyBound k: $\rho(k)$ .
GroupSumFree C: $C$ is sumfree in $G$ . The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.
liftPrefix m₁ M L: $x_L$ , defined for all $m_1$ and $M$ by $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$ .
liftSeq m₁ m₂ M: the lifted sequence, defined for all $m_1$ , $m_2$ and $M$ as the list of the $m_1 m_2 - 1$ differences $x_{k+1} - x_k$ .

Formalization targets

Goal

\mathrm{erL}\ 4 = 16

An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.

Theorem 4.1 of Eliahou–Revuelta, in ℕ, with $\rho(k)$ for $R_k(3)$

\rho(k) \le |A| + 1 \implies k + 1 \le \operatorname{sdeg}(\hat A) \qquad (k \in \mathbb{N},\ A \text{ a finite sequence in } \mathbb{N}).

Upper bound of Proposition 5.3, with $\rho(k)$ for $R_k(3)$

\mathrm{erL}(k+1) \le \rho(k) - 1 \qquad (k \in \mathbb{N}).

No length below 16 has the property at $n = 4$

\neg\,\mathrm{ERProperty}\ 4\ L \qquad (1 \le L \le 15).

Lemma 4.1 (McKenna 2026): lift from a group

For $m_1, m_2, q \ge 1$ , $M \ge 3m_1 - 2$ and sets $C_1, \dots, C_q$ , sumfree in $G$ , that cover $G \setminus \{0\}$ , the sequence $A =$ liftSeq m₁ m₂ M satisfies

|A| = m_1 m_2 - 1, \quad a_i > 0, \quad \operatorname{sdeg}(\hat A) \le q, \quad a_1 + \dots + a_L = x_L \ \ (L \le m_1 m_2 - 1).

Corollary 4.2 (McKenna 2026): group coverings bound $L(n)$ from below

For $n \ge 3$ , $m_1, m_2 \ge 1$ and $n - 1$ sets, sumfree in $G$ , that cover $G \setminus \{0\}$ :

m_1 m_2 \le \mathrm{erL}\ n.

Theorem 1.2 (McKenna 2026), with the Lean upper bound: bounds for $L(5)$

49 \le \mathrm{erL}\ 5 \le 65.

Significance

$L(4) = 16$ . At $n = 4$ , Conjecture 5.6 predicts $L(4) = S(3) + 1 = 14$ . So $L(4) = 16$ refutes the conjecture at $n = 4$ . Here $L(n)$ equals the upper bound $R_{n-1}(3) - 1$ of Proposition 5.3.

The two bounds of Proposition 5.3 coincide at $n = 2, 3$ , where the paper gives $L(2) = 2$ and $L(3) = 5$ . So $n = 4$ is the first case in which the conjecture says more than Proposition 5.3.

$L(5) \ge 49$ . At $n = 5$ , Conjecture 5.6 predicts $L(5) = S(4) + 1 = 45$ . So $L(5) \ge 49$ refutes the conjecture at $n = 5$ .

What remains open. Conjectures 5.7 and 5.8 remain open.

The paper derives Conjecture 5.7 at each $n$ from Conjecture 5.6 at the same $n$ , with Theorem 5.4. At $n = 4, 5$ that derivation is not available. But Conjecture 5.7 holds there by the known values: $44 \le 4 \cdot 14$ and $160 \le 5 \cdot 45$ .

Conjecture 5.8 follows from Conjecture 5.6 at $n = 6$ (that is, $L(6) = 161$ ) with Theorem 5.4. Nothing here decides that case.

With $L(4) = 16$ , Theorem 5.4 gives only $S(4) \le 64$ . This is weaker than $S(4) \le R_4(3) - 2 \le 60$ .

Status. Every target is proved and formalized.

Theorem 4.1 and Proposition 5.3 are proved in the refereed paper.
$L(4) = 16$ (Theorem 1.1), Lemma 4.1, Corollary 4.2 and $L(5) \ge 49$ (Theorem 1.2) are proved in McKenna 2026 (doi:10.5281/zenodo.22987189). Before publication, separate agents, with their own code, checked the proofs in two rounds of adversarial audit.

At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.

An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.

Literature. The literature search for McKenna 2026 found no result on $L(4)$ , $L(5)$ or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.

Open work, not targets.

The exact $L(5)$ : $49 \le L(5) \le 61$ on paper (with $R_4(3) \le 62$ ), and $49 \le L(5) \le 65$ in Lean.
The case $n = 6$ : $161 \le L(6) \le R_5(3) - 1 \le 306$ (DS1: $R_5(3) \le 307$ ). Here Conjecture 5.6 is the open step toward $S(6) \le 966$ .

Difficulty

Two kinds of bound. The two sides of an exact value of $L(n)$ are statements of different kinds.

An upper bound $L(n) \le m$ needs one length. It follows from $\operatorname{sdeg}(\hat A) \ge n$ for every sequence $A$ of positive integers of one length $L$ , with $1 \le L \le m$ and average at most $n$ .

A lower bound $L(n) \ge m$ needs every shorter length. For every $L$ with $1 \le L < m$ , it needs a sequence of $L$ positive integers, with average at most $n$ , whose block sums are covered by $n - 1$ sumfree sets.

One counterexample at length $m - 1$ is not enough. A sequence of length $L + 1$ and average at most $n$ need not contain $L$ consecutive entries of average at most $n$ . So monotonicity in $L$ does not follow directly from the definition.

The average bound. The lower bound $S(n-1) + 1$ of Proposition 5.3 comes from the constant sequence $(1, \dots, 1)$ , with $\hat A = \{1, \dots, L\}$ . Conjecture 5.6 states that at length $S(n-1) + 1$ , no sequence of average at most $n$ has $\operatorname{sdeg}(\hat A) \le n - 1$ .

Without the bound on the average, this fails. The paper gives a sequence of length 14 with $\operatorname{sdeg}(\hat A) = 3$ , found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".

The gap for $L(5)$ . The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at $n = 5$ :

$S(4) = 44$ excludes the cyclic groups of order at least 46.
Solver runs exclude the non-cyclic groups of order 50 to 60. Their unsatisfiability proofs (in the DRAT format) were checked.
$L(5) \le 61$ excludes the orders of 62 or more.

McKenna 2026 knows no sequence of length 49 with average at most 5 and $\operatorname{sdeg}(\hat A) \le 4$ ; such a sequence would give $L(5) \ge 50$ .

Formalization scope

Ambient ℕ. The paper works in an abelian group; here sets are Set ℕ and sequences List ℕ. For $X \subseteq \mathbb{N}$ the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.
sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and $\operatorname{sdeg}(\emptyset) = 1$ . Covers are Fin n → Set ℕ; the sets need not be disjoint or inside $X$ . Each lower bound on sdeg must exclude every cover.
blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires $L > 0$ .
erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every $n$ (the paper: $n \ge 2$ ). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length $\rho(k) - 1 \ge 1$ , and 0 satisfies neither the goal nor the lower bounds.
Ramsey bound. $\rho(k)$ replaces $R_k(3)$ . TriangleRamsey k N says every colouring of the pairs $x < y$ of at least $N$ naturals with at most $k$ colours has a monochromatic triangle; the tree proves it for $N = \rho(k)$ . As $\rho(4) = 66 > 62 \ge R_4(3)$ , the Lean upper bound for $L(5)$ is 65, not 61.
Lemma 4.1, Corollary 4.2. As in McKenna 2026, the sets need only cover $G \setminus \{0\}$ , and Lemma 4.1 requires $q \ge 1$ : for $q = 0$ , $m_1 = m_2 = 1$ the sequence is empty and $\operatorname{sdeg}(\emptyset) = 1$ . The prefix sums are exact: $x_L$ .
Subtraction is truncated; with $m_1, m_2 \ge 1$ and $\rho(k) \ge 2$ , none of 3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) ( $n \ge 3$ ) truncates, and the differences in liftSeq do not truncate when $M \ge m_1 \ge 1$ .
Finite checks use kernel decide; no native_decide, no external certificate.

Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives $L(5) \le 61$ in Lean; the exact $L(5)$ ; the case $n = 6$ .

Selected references

S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, Discrete Math. 344 (2021) 112332. https://doi.org/10.1016/j.disc.2021.112332
S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, preprint, arXiv:2006.01502v1, 2020. https://arxiv.org/abs/2006.01502v1
R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI-18, 2018; preprint arXiv:1711.08076, 2017. https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
A. McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49, Zenodo, 2026. https://doi.org/10.5281/zenodo.22987189 (version 1.0.1: https://doi.org/10.5281/zenodo.22987688). The Lean library ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).

16 thms1 active userReviewed

Completed

Number Theory·Captain: Yuxuan Xu

Equal Sums of Two Squares: Parametrization and Infinite Primitive FamiliesResearch Paper

Motivation

The representation function $r_{2}(n)=\#\{(a,b)\in\mathbb Z^{2}:a^{2}+b^{2}=n\}$ is one of the oldest objects in number theory. Fermat characterised the integers with $r_{2}(n)>0$ — those in which every prime congruent to $3$ modulo $4$ occurs to an even power — and Euler's proof supplied the closed form $r_{2}(n)=4\,(d_{1}(n)-d_{3}(n))$ , where $d_{j}(n)$ counts divisors congruent to $j$ modulo $4$ (sum of two squares theorem).

That description counts representations but does not relate them to one another. The integers carrying several essentially different representations,

50=1^{2}+7^{2}=5^{2}+5^{2},\qquad 65=1^{2}+8^{2}=4^{2}+7^{2},

are exactly the integers that produce quadruples $(a,b,c,d)$ with

a^{2}+b^{2}=c^{2}+d^{2}

whose two sides are not identified by swapping the two entries or changing their signs. Three reasons make this relation worth a formal development rather than a passing remark.

Energy counts. Counting solutions of the equation inside a box is the additive energy of the set of sums of two squares, the quantity controlling mean-square errors for $r_{2}$ ; it is a genuinely different problem from determining $r_{2}(n)$ for a single $n$ , and every estimate for it starts from a description of the solution set.
Composition of representations. The Brahmagupta–Fibonacci identity

(p^{2}+q^{2})(r^{2}+s^{2})=(pr+qs)^{2}+(ps-qr)^{2}=(pr-qs)^{2}+(ps+qr)^{2}

takes two representations and produces a third. Known to Brahmagupta and stated by Fibonacci in Liber Quadratorum (1225), it is the multiplicativity of the norm in the Gaussian integers, and it is the engine behind every statement below.

Geometry. Over a field, the locus $a^{2}+b^{2}=c^{2}+d^{2}$ in projective three-space is the split quadric, isomorphic to $\mathbb P^{1}\times\mathbb P^{1}$ under the Segre embedding; the four parameters introduced below are Segre coordinates in this sense. The arithmetic content of the equation is precisely the integrality that this geometry ignores.

The parametrisation targeted here is classical. Nothing in this mission claims new mathematics; the aim is a machine-checked development in which every hypothesis is explicit.

Setting

Fix integers. A solution is a quadruple $(a,b,c,d)\in\mathbb Z^{4}$ with $a^{2}+b^{2}=c^{2}+d^{2}$ . It is trivial if the multisets $\{a^{2},b^{2}\}$ and $\{c^{2},d^{2}\}$ coincide, i.e. if $(c,d)$ equals $\pm(a,b)$ or $\pm(b,a)$ ; if entries are allowed to vanish, the least value carried by a non-trivial solution is $25=0^{2}+5^{2}=3^{2}+4^{2}$ , and requiring all four entries to be positive raises that value to $50$ . A solution is primitive when the four entries have greatest common divisor $1$ , and positive when all four entries are positive and pairwise distinct — the case in which nothing about the relation is explained by signs, zeros or coincidences.

Two constructions produce solutions. The four-parameter family associates to integers $p,q,r,s$ the quadruple

a=pr+qs,\qquad b=ps-qr,\qquad c=pr-qs,\qquad d=ps+qr,

which solves the equation because both sides equal $(p^{2}+q^{2})(r^{2}+s^{2})$ by the identity above. Substituting particular parameters is unrevealing, so a genuine supply comes instead from the elementary one-parameter family

1^{2}+(n^{2}-n+1)^{2}=(2n-1)^{2}+(n^{2}-n-1)^{2},

whose four entries $1$ , $n^{2}-n+1$ , $2n-1$ , $n^{2}-n-1$ are strictly increasing — hence positive and pairwise distinct — as soon as $n\ge 4$ . The bound is sharp: at $n=3$ the two entries $2n-1$ and $n^{2}-n-1$ are equal.

In the reverse direction, rewrite the equation as $(a+c)(a-c)=(d+b)(d-b)$ and set

X=(a+c)/2,\quad Y=(a-c)/2,\qquad U=(b+d)/2,\quad V=(d-b)/2 .

The halves are integers exactly when $a$ and $c$ share a parity and so do $b$ and $d$ , and in that case the equation becomes

XY=UV .

The development is organised in the namespace TwoSquares, with node names matching the roles above (four_param_identity, explicit_family_chain, sum_sq_eq_halves, four_factor_param, complete_parametrization).

Formalization targets

Goal — completeness of the four-parameter family

For all integers $a,b,c,d$ with $a^{2}+b^{2}=c^{2}+d^{2}$ , there are integers $p,q,r,s$ with

a=pr+qs,\quad b=ps-qr,\quad c=pr-qs,\quad d=ps+qr,

possibly after interchanging $c$ and $d$ . The goal asserts only the existence of integral parameters and the necessity of at most one swap; it does not assert uniqueness of $(p,q,r,s)$ , which is false, and it says nothing about how many solutions lie in a given box.

The four-parameter identity

The identity itself, over an arbitrary commutative ring, together with the two forms of the Brahmagupta–Fibonacci identity that imply it — so that the reason it holds, rather than the expansion, is what is recorded.

An explicit infinite family

For every integer $n\ge 4$ the displayed family is a positive pairwise distinct solution; the parametrisation $n\mapsto(1,\,n^{2}-n+1,\,2n-1,\,n^{2}-n-1)$ is injective; the set of quadruples it produces is infinite; and no member is a nontrivial integer multiple of another, each member being primitive.

From the sum-of-squares equation to $XY=UV$

The equivalence of $a^{2}+b^{2}=c^{2}+d^{2}$ with $(a+c)(a-c)=(d+b)(d-b)$ ; the parity statement that matching entries share a parity after at most one swap; and the resulting existence of the half-sum variables satisfying $XY=UV$ .

Parametrizing $XY=UV$

For all integers $X,Y,U,V$ with $XY=UV$ there are integers $p,q,r,s$ with $X=pr$ , $Y=qs$ , $U=ps$ , $V=qr$ — the coordinate form of the statement that a rank-one $2\times2$ matrix factors through the integers.

Significance

The result. Taken together, the reverse chain converts the Diophantine equation $a^{2}+b^{2}=c^{2}+d^{2}$ into four free integer parameters, at the cost of one possible swap. In that form every question about the solution set becomes a question about four independent variables, which is what makes energy estimates, density statements and searches for primitive solutions tractable. The chain also isolates where integrality enters: over a field the parametrisation of $XY=UV$ is formal, so the content is carried entirely by the parity step and by divisibility over $\mathbb Z$ .

Formalizing it. None of the mathematics is new, and that is the point: the value here is a development in which each link is a reusable statement with explicit hypotheses. Three conventions make the nodes reusable rather than bespoke. The algebraic identity is proved over a general commutative ring, not over $\mathbb Z$ . The positivity and distinctness of a family are packaged as one strict chain rather than as a list of inequalities, since later arguments use the ordering, not merely the disequalities. The parity issue is isolated into a single node stating a disjunction, instead of being discharged by case splits buried inside a later proof. Conversely, the shape of the final theorem records honestly what is not claimed: parameters are not unique, and no normal form is asserted.

As difficulty, the early nodes have short proofs, while completeness requires the full chain and is the substantial part of the mission.

Difficulty

The obvious first idea is to use the Gaussian integers: $a+bi$ and $c+di$ have the same norm, so factor both and compare. It fails. Equal norm does not make two Gaussian integers associates or divisors of one another — $1+8i$ and $4+7i$ both have norm $65$ and are related by no divisibility — because uniqueness of factorisation regroups prime factors in ways that the norm alone cannot distinguish. The correct route recovers the four parameters from the product equation instead, and there the friction is entirely arithmetic:

Clearing halves. The substitution $X=(a+c)/2$ is not available for arbitrary solutions: $a^{2}+b^{2}=c^{2}+d^{2}$ forces only that the multiset of parities of $(a,b)$ matches that of $(c,d)$ , so $(a,c)$ may have different parities and no integer $X$ may exist. The example $a=1,b=0,c=0,d=1$ shows this is not vacuous, and it is why the goal carries a swap.

Factoring $XY=UV$ . Taking $p=\gcd(X,U)$ yields $X=pr$ , $U=ps$ with $\gcd(r,s)=1$ , and Euclid's lemma then forces $s\mid Y$ and $r\mid V$ . The degenerate case $X=U=0$ — where the gcd vanishes and no cancellation is possible — must be handled separately, and because the variables range over $\mathbb Z$ rather than $\mathbb N$ , every divisibility step must be tracked with signs. Working over a ring where division is available would delete both issues and with them the entire content of the statement.

Formalization scope

All nodes are stated over $\mathbb Z$ , except the Brahmagupta–Fibonacci identity and the four-parameter identity, which are proved over an arbitrary commutative ring. No node is stated over $\mathbb N$ ; transporting the prime-level statements is out of scope.
Gaussian integers are deliberately unused. Mathlib carries them, but nothing here needs them, and a development depending on them would obscure the arithmetic that actually carries the proof.
No quotient types, no permutation machinery: the possible swap of $c$ and $d$ is expressed as a disjunction, and the parity statement as a disjunction over Even.
Trivializing formalizations are excluded. Over a field the parametrisation of $XY=UV$ holds trivially (take $p=X$ , $r=1$ , $s=U/X$ ), so the quarter-ring version carries no information; likewise, a completeness statement whose hypotheses already postulate the existence of the parameters would be vacuous. Both are explicitly not what is asked for.
Expected to be reusable beyond this mission: the two forms of the Brahmagupta–Fibonacci identity; the strict-chain packaging of positivity and distinctness for a family given by polynomials; and the integer parametrisation of $XY=UV$ , which is the Segre parametrization.
Contributions are welcome for any node, and especially for the integer factoring lemma, for which several proofs are available. Explicitly out of scope: uniqueness or normal forms for $(p,q,r,s)$ , counting asymptotics for solutions in a box, the Gaussian-integer reformulation, and all $\mathbb N$ -level variants.

Selected references

Sum of two squares theorem — Fermat's characterisation and Euler's divisor formula for $r_{2}$ .
Brahmagupta–Fibonacci identity — the two-square composition identity, its history, and its interpretation through norms.
Leonardo Pisano (Fibonacci), Liber Quadratorum, 1225. English translation: L. E. Sigler, The Book of Squares, Academic Press, 1987.
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008 — Chapter XX on representations by two squares.
Segre embedding — the identification of the rank-one quadric in $\mathbb P^{3}$ with $\mathbb P^{1}\times\mathbb P^{1}$ .

13 thms1 active userReviewed

Completed

Analysis Machine Learning·Captain: Minghui

Sharp Minima Can Generalize: ReLU Rescaling and Hessian SharpnessResearch Paper

Why the geometry of a minimum needs a parameter convention

A trained neural network is used through its predictions, while its parameters are the coordinates in which training takes place. Distinct parameter vectors can describe exactly the same prediction function. A proposed explanation of generalization based on the shape of the parameter-space loss therefore needs to account for these equivalences. This mission concerns Hessian sharpness: the spectral norm of the matrix of second derivatives of the loss at a minimum. The question is whether that number is intrinsic to the predictor or can change without changing any prediction.

Dinh, Pascanu, Bengio, and Bengio establish that, for a one-hidden-layer rectified network, every sufficiently differentiable critical minimum with nonzero Hessian has equivalent parameterizations of arbitrarily large Hessian sharpness. The formalization target is their Section 4.2, Theorem 4, PDF pp. 5–6. The goal theorem and both supporting milestones now have accepted Lean proofs on Prove2Me. This public research-paper mission is complete.

The immediate historical sequence is:

2016–2017: Keskar and collaborators reported numerical evidence relating large-batch training, sharp minima, and a generalization gap. This is empirical context, not an assumption or a theorem to be proved in this mission. ICLR 2017 paper.
March 2017: Dinh and collaborators released a mathematical analysis of parameter symmetries and several flatness measures. The fixed source for this mission is their May 2017 revision, arXiv version 2, which determines the theorem numbering and PDF page citations. Version history.

Networks, losses, and reciprocal layer scaling

Fix positive integers $d$ and $h$ , the input dimension and hidden width. Let $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ be the network's weights. For an input $x\in\mathbb R^d$ , define

f_{W,v}(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_iW_{ij},0\right)v_j.

This is a bias-free network with one hidden layer, rectified activation, and a scalar linear output. Its parameter vector $\theta=(W,v)$ has $n=dh+h$ coordinates and the Euclidean norm. A function-based loss is a real-valued functional $\ell$ of the entire prediction function, giving $L(\theta)=\ell(f_\theta)$ . The Hessian targets assume $L$ is continuous. These conventions come from Sections 2–3, PDF pp. 2–4, Definition 3.

Two parameters are observationally equivalent if their predictions agree on every input. For a positive real number $\alpha$ , the layer scaling is

T_\alpha(W,v)=(\alpha W,\alpha^{-1}v).

The definition rescales the incoming and outgoing weights in opposite ways. It is the transformation in Section 3, Definition 5, PDF p. 4.

Write $DL(\theta)$ for the first Fréchet derivative and $H_L(\theta)=D(DL)(\theta)$ for the second derivative. The local differentiability condition requires $L$ to be differentiable throughout a neighborhood of $\theta$ , with $DL$ differentiable at $\theta$ . This states the regularity needed for the paper's Hessian notation explicitly, without requiring global smoothness or continuous second derivatives. A critical local minimum satisfies $DL(\theta)=0$ and has no smaller loss in some neighborhood; it may belong to a continuum of minima.

Symmetry, derivative transformation, and the goal theorem

The first milestone formalizes the scaling consequence of positive ReLU homogeneity in Theorem 1 and Definition 5, PDF p. 4:

f_{T_\alpha\theta}=f_\theta,\qquad L(T_\alpha\theta)=L(\theta),

and $T_\alpha\theta$ is a local minimum precisely when $\theta$ is. These statements hold for every parameter and every $\alpha>0$ ; the milestone itself requires no loss regularity.

The second milestone is Theorem 3, Section 4.2, PDF p. 5. At every point satisfying the stated local differentiability condition,

DL(T_\alpha\theta)[u]=DL(\theta)[T_{\alpha^{-1}}u],

H_L(T_\alpha\theta)[u,w] =H_L(\theta)[T_{\alpha^{-1}}u,T_{\alpha^{-1}}w]

for all parameter directions $u,w$ . The same regularity holds at the rescaled point. This is the coordinate-free form of the paper's gradient formula and Hessian congruence with $D_\alpha=\operatorname{diag}(\alpha^{-1}I_{dh},\alpha I_h)$ .

The goal is Theorem 4. If $\theta$ is a critical local minimum with the stated differentiability and $H_L(\theta)\ne0$ , then

\forall M>0\ \exists\alpha>0:\qquad \|H_L(T_\alpha\theta)\|_2\ge M.

For that same rescaling, predictions and loss agree with the original ones, and the transformed parameter remains a critical local minimum with the required differentiability. The subscript $2$ denotes the Euclidean spectral norm. The source statement and its interpretation are in Section 4.2, PDF pp. 5–6. The relevant displays in all three targets are unnumbered.

What the formalization establishes

The result separates prediction behavior from this particular numerical measure of parameter-space curvature. Pointwise identical predictors have identical function-based evaluation losses wherever those are defined, even though their Hessian sharpness can be made arbitrarily large under the stated conditions. This is the scope of the obstruction: it concerns the unnormalized Euclidean Hessian norm and this rescaling symmetry. It does not assert that training reaches every point on a scaling orbit or supply a numerical bound on test error. Theorem 4 and following discussion, PDF p. 6.

The completed Lean development connects an explicitly computed ReLU prediction function to its actual first and second derivatives. It provides reusable results about invariant losses, transport of local minima, and curvature under linear changes of parameters. All three published theorem statements were proved unchanged and accepted on 26 September 2026. Both milestones are complete, and the goal has no remaining open leaves.

The analytic obligations

ReLU is not differentiable at every activation boundary. The loss-level local regularity must therefore be retained rather than inferred from the network's syntax. A nonzero symmetric matrix alone is also insufficient for the sharpness claim: local minimality supplies an additional sign constraint. Finally, the second derivative is an operator on the entire parameter space; bounds for a single arbitrarily chosen scalar model do not establish the quantified network result. These are obligations of the formal proof, not hypotheses assuming the desired transformation identities.

Formalization note: scope and conventions

Parameters are represented by EuclideanSpace over the disjoint union of first-layer matrix coordinates and output-weight coordinates. This retains the sum-of-squares geometry rather than a product maximum norm. The Hessian is the derivative of the actual Fréchet derivative, represented as a continuous bilinear form. Its operator norm is the spectral norm under the Euclidean/Riesz identification. The regularity condition excludes reliance on default derivative values at nondifferentiable points.

The statement covers every positive input dimension and hidden width, arbitrary function-based losses with the specified regularity, and arbitrary qualifying minima. It imposes no separate nonzero-weight or active-neuron assumption. An input or output weight block may vanish when the loss hypotheses still hold. The nonzero-Hessian requirement is essential. Scaling by zero or a negative number is outside the claim. No probability model, random initialization, sampling measure, or training algorithm is assumed.

The mission focuses on the single-hidden-layer Hessian result. Volume flatness, the multiple-eigenvalue deep-network theorem, and other reparameterizations remain separate results in the paper. The local environment is Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio. Sharp Minima Can Generalize For Deep Nets. ICML 2017, PMLR 70:1019–1028. arXiv:1703.04933v2. Primary anchors: Section 2, PDF p. 2; Section 3, PDF pp. 3–4, Definitions 3–5 and Theorem 1; Section 4.2, PDF pp. 5–6, Theorems 3–4.
Nitish Shirish Keskar, Dheevatsa Mudigere, Jorge Nocedal, Mikhail Smelyanskiy, Ping Tak Peter Tang. On Large-Batch Training for Deep Learning: Generalization Gap and Sharp Minima. ICLR 2017. arXiv:1609.04836v2. Historical context.

4 thms1 active userReviewed

Completed

Machine Learning Probability·Captain: Minghui

Neural Tangent Kernel: The Infinite-Width Initialization LimitResearch Paper

Why an initialization kernel matters

A neural network is nonlinear in its parameters, but a small change in those parameters changes its predictions through a Jacobian. The neural tangent kernel is the Gram kernel of that Jacobian: it records which changes in predictions can be produced by common parameter updates. An initialization limit identifies a deterministic object behind this random kernel. It supplies a mathematical starting point for studying wide networks through kernel methods, before addressing the additional question of how the kernel changes during training. Jacot, Gabriel, and Hongler establish this initialization limit in Section 4.1, Theorem 1, PDF p. 5.

The requested result is already a theorem of the paper. The open work here is its formal proof in Lean, including the probability model and the order of limits. The mission is classified as OpenProblem at the request of its proposer; that label does not assert that the underlying mathematical result remains an unsolved research question.

The source appeared in 2018 and was published at NeurIPS 2018; this formalization fixes arXiv version 4, dated February 10, 2020, so that page references and conventions remain stable. Its Appendix A explicitly distinguishes the sequential limit proved there from a possible stronger simultaneous-width limit.

Networks, randomness, and the two kernels

Fix positive integers $d$ and $q$ , the input and output dimensions, a hidden-layer count $h\ge0$ , a bias scale $\beta>0$ , and a Lipschitz function $\sigma:\mathbb R\to\mathbb R$ . Write $L=h+1$ for the number of affine layers, with $n_0=d$ , $n_L=q$ , and positive hidden widths $n_1,\ldots,n_h$ . The parameters are all entries of the weight matrices and bias vectors. Every parameter is sampled independently from $\mathcal N(0,1)$ .

For an input $x$ , let $a^{(0)}(x)=x$ and define

z^{(\ell+1)}_j(x)=\frac1{\sqrt{n_\ell}} \sum_i W^{(\ell)}_{ji}a^{(\ell)}_i(x)+\beta b^{(\ell)}_j.

At each hidden layer, $a^{(\ell)}=\sigma(z^{(\ell)})$ coordinatewise. The output is $f_\theta(x)=z^{(L)}(x)$ , with no final activation. These are the conventions of Section 2, PDF pp. 2–3. Matrix storage order in Lean uses destination then source; the displayed operation is unchanged.

For output coordinates $k,k'$ , set

\Theta^{(L)}_{kk'}(\theta;x,y)=\sum_p \partial_{\theta_p}f_{\theta,k}(x)\, \partial_{\theta_p}f_{\theta,k'}(y).

The sum includes every weight and every bias, as in Section 4, PDF p. 5.

The covariance kernel starts with

\Sigma^{(1)}(x,y)=\frac{\langle x,y\rangle}{d}+\beta^2.

Given a centered Gaussian pair $(U,V)$ with covariance matrix obtained by evaluating $\Sigma^{(\ell)}$ on $(x,y)$ , define

\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma(U)\sigma(V)]+\beta^2, \qquad \dot\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma'(U)\sigma'(V)].

The deterministic limiting NTK is

\Theta_\infty^{(1)}=\Sigma^{(1)},\qquad \Theta_\infty^{(\ell+1)}(x,y)=\Theta_\infty^{(\ell)}(x,y) \dot\Sigma^{(\ell+1)}(x,y)+\Sigma^{(\ell+1)}(x,y).

These recurrences appear in Section 4.1, Proposition 1 and Theorem 1, PDF p. 5; their displays are unnumbered.

Formalization targets

The goal is Theorem 1, on every fixed finite family $X=(x_1,\ldots,x_N)$ of inputs and for every $\varepsilon>0$ :

\Pr\!\left(\exists i,j,k,k': \left|\Theta^{(L)}_{kk'}(\theta;x_i,x_j) -\Theta_\infty^{(L)}(x_i,x_j)\delta_{kk'}\right|>\varepsilon\right) \longrightarrow0.

Here $\delta_{kk'}$ is one when the output coordinates coincide and zero otherwise. The limit takes $n_1\to\infty$ first, then $n_2\to\infty$ , through $n_h\to\infty$ , precisely as specified in Appendix A, PDF p. 11, and Appendix A.1, PDF pp. 12–13.

Two supporting milestones expose the required mathematical content. First, the recursively defined $\Sigma^{(L)}$ has positive semidefinite Gram matrices on every finite input family and satisfies $\Sigma^{(L)}(x,x)\ge\beta^2$ . This is a paper-derived well-definedness obligation for the covariance in Proposition 1. Second, Proposition 1 asserts joint convergence in distribution of $(f_{\theta,k}(x_i))_{i,k}$ to the centered Gaussian vector with covariance $\Sigma^{(L)}(x_i,x_j)\delta_{kk'}$ . This expresses the paper's independent output Gaussian processes through all their finite-dimensional distributions.

What completing the mission would establish

The result connects an explicitly parameterized random finite network to a deterministic kernel computed from its activation and depth. All output correlations, bias contributions, and layer normalizations remain visible in that connection. It would provide a checked foundation on which a separate training-stability development could build.

The formal contribution is the passage from finite random Jacobians to the limiting kernel. It does not assume that the empirical NTK already equals its limit. Nor does the goal claim convergence of a training trajectory, positive definiteness on a sphere, an early-stopping guarantee, or a generalization bound; those are separate results and questions in the source.

Where the mathematical work lies

The parameter space changes with the widths. Outputs, hidden activations, and their parameter derivatives are dependent random quantities, so the limit of their products requires more than a scalar law of large numbers. The weak Gaussian limit alone also does not justify substituting an arbitrary discontinuous derivative into expectations. The Lipschitz-only hypothesis is part of the target and must be retained, including for nonsmooth activations. Remark 3, PDF p. 5 identifies almost-everywhere differentiation as the relevant convention.

Formalization scope and conventions

Lean represents parameter coordinates by a finite dependent index carrying a layer, destination neuron, and optional source neuron; the missing source denotes a bias. Initialization is the finite product of Mathlib's standard Gaussian measures. Network outputs are obtained by the displayed recursion, and NTK entries use actual Fréchet derivatives in coordinate directions. Mathlib's derivative is zero where differentiation fails; the proof must establish that the exceptional parameters are null under the stated initialization law.

Centered Gaussian laws use Mathlib's multivariateGaussian, including singular covariance. The covariance-validity milestone must justify its covariance interpretation. No invertibility, distinct-input, smooth-activation, or positive-definite-kernel assumption is added. Positive actual hidden widths are indexed as $w_i+1$ for $w_i\in\mathbb N$ , a cofinal reindexing. Depth one, constant activations, repeated or zero inputs, and empty finite families are included. The empty family is harmless because the same theorem quantifies over every nonempty family as well.

The sequential filter puts the last hidden width outermost. For two hidden widths, a probability tolerance is met by first choosing a threshold for $n_2$ , then a threshold for $n_1$ that may depend on $n_2$ . There is no uniform limit over the entire input space and no simultaneous-width assertion. The development uses Lean 4.30.0 and supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The model and statements are locally checked; the three theorem proofs remain open. Contributions to Gaussian covariance consistency, finite-dimensional distribution limits, almost-everywhere network differentiation, and the NTK limit are in scope.

Selected references

Arthur Jacot, Franck Gabriel, and Clément Hongler, Neural Tangent Kernel: Convergence and Generalization in Neural Networks, Advances in Neural Information Processing Systems 31, 2018. arXiv:1806.07572v4. Primary anchors: Section 2, PDF pp. 2–3; Section 4.1, PDF p. 5, Proposition 1, Theorem 1, Remarks 2–3; Appendix A and A.1, PDF pp. 11–13. Relevant displays have no equation numbers.

4 thms1 active userReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

APSP in O(n^2.9983) via All-Edges Exact TriangleResearch Paper

References:

Every Odd Number Greater Than 1 is the Sum of at Most 85 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Every Odd Number Greater Than 1 is the Sum of at Most 159 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Every Odd Number Greater Than 1 is the Sum of at Most 151 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Every Odd Number Greater Than 1 is the Sum of at Most 241 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Connes–Feldman–Weiss: an amenable equivalence relation is generated by a single transformationResearch Paper

Motivation

Setting

Formalization targets

Goal (p. 431)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Uniqueness of the Hemispheric Saddle Profile on a Magnetic Sphere (AIM 241)Open Problem

Motivation

Setting

Formalization target

Significance

Difficulty

Formalization scope

Selected references

Periodic Multidimensional Costas Arrays (Rubio–Torres Conjecture 1)Open Problem

Motivation

Setting

Formalization target

Significance

Difficulty

Formalization scope

Selected references

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

Setting

Formalization targets

Goal: six colours under R4(3)≤61R_4(3) \le 61R4​(3)≤61

Centred-interval bound

Balanced colour classes

Nested saturation

Automorphism extension

Forced reflection

Goal: six colours under $R_4(3) \le 61$