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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

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.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 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.995561Formalized record

3 provers on it5 of 5 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.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 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.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 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

38 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)

See all campaigns →

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

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.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 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.995561Formalized record

3 provers on it5 of 5 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.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 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.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 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

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Number Theory Pure Mathematics·Captain: Lucas

Schinzel's Hypothesis HOpen Problem

Motivation

Almost every classical question about prime values of polynomials is a special case of one statement. Are there infinitely many twin primes? Infinitely many primes of the form $n^2+1$ ? Infinitely many Sophie Germain primes $p$ with $2p+1$ prime? Each asks whether a fixed finite list of integer polynomials takes prime values simultaneously infinitely often. Schinzel's Hypothesis H (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that factors cannot be prime infinitely often, and neither can a family whose product is always divisible by some fixed prime.

Timeline.

1837 — Dirichlet proves the degree-one, single-polynomial case: if $\gcd(a,b)=1$ and $a>0$ , then $an+b$ is prime for infinitely many $n$ .
1857 — Bunyakovsky states the single-polynomial case for arbitrary degree. It is open for every fixed polynomial of degree $\ge 2$ ; not one instance, not even $n^2+1$ , is known.
1904 — Dickson states the case of arbitrarily many linear polynomials.
1958 — Schinzel and Sierpiński state Hypothesis H in the generality used here (Acta Arith. 4 (1958), 185–208).
1962 — Bateman and Horn give the conjectural asymptotic count of such $n \le N$ , refining Hypothesis H to a quantitative form (Math. Comp. 16 (1962), 363–367).
1978 — Iwaniec proves that $n^2+1$ has at most two prime factors infinitely often; the sieve barrier that blocks "exactly one" has not been broken.
2004 — Green and Tao prove the analogous simultaneous-prime statement for systems of linear forms of finite complexity, which yields arbitrarily long arithmetic progressions of primes but does not cover Dickson's conjecture in full (the pair $n$ , $n+2$ has infinite complexity).
2013 — Zhang, and then Maynard and Tao, establish bounded gaps between primes, i.e. that some admissible pair $\{n+h_1, n+h_2\}$ is simultaneously prime infinitely often — but the method does not identify which pair.

Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.

Setting

Work in the ring $\mathbb{Z}[X]$ of polynomials with integer coefficients. Fix a finite set $\mathcal{F} \subseteq \mathbb{Z}[X]$ of polynomials $f$ , each subject to the Bunyakovsky condition:

$\deg f \ge 1$ ;
the leading coefficient of $f$ is positive;
$f$ is irreducible in $\mathbb{Z}[X]$ .

Irreducibility in $\mathbb{Z}[X]$ is strictly stronger than irreducibility in $\mathbb{Q}[X]$ : it also forces the content of $f$ to be $1$ , ruling out $2X^2+2$ .

Even an irreducible family can be blocked by congruences. The polynomial $X^2+X+2$ is irreducible with positive leading coefficient, yet $n^2+n+2$ is even for every integer $n$ , so it is prime only when it equals $2$ . The family $\mathcal{F}$ therefore also has to satisfy the Schinzel condition: for every prime $p$ there exists an integer $n$ with

p \nmid \prod_{f \in \mathcal{F}} f(n).

Equivalently, no prime is a fixed divisor of the product $\prod_{f\in\mathcal{F}} f$ . A family satisfying both conditions is called admissible.

Target

For an admissible family $\mathcal{F}$ , write

S(\mathcal{F}) \;=\; \{\, n \in \mathbb{N} \;:\; |f(n)| \text{ is prime for every } f \in \mathcal{F} \,\}.

The goal of the mission is Hypothesis H:

\mathcal{F} \text{ admissible} \;\Longrightarrow\; S(\mathcal{F}) \text{ is infinite.}

The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the Schinzel condition to the finitely many primes $p \le \sum_{f\in\mathcal F}\deg f$ ; the necessity of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the twin prime conjecture, and Landau's problem on $n^2+1$ — each stated as an implication from the goal statement, so that they can be proved before the goal itself is.

Significance

The result itself. Hypothesis H implies the twin prime conjecture, the Sophie Germain prime conjecture, Landau's conjecture that $n^2+1$ is prime infinitely often, the infinitude of primes in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts the density of such $n$ . Nothing beyond the degree-one case is known, and the conjecture is the standard yardstick against which sieve-theoretic progress on prime values of polynomials is measured.

Formalizing it. The goal is open, so the mission's deliverable is not a proof of it but a formal, audited statement of it together with a supporting environment: the admissibility predicates, the classical reductions, and machine-checked derivations of the famous corollaries from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in Mathlib, so the linear milestone is a matter of connecting that result to this mission's formulation rather than of new mathematics. The three "H implies …" milestones are provable now, unconditionally, because they are implications; they are also the sharpest available check that the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to yield twin primes.

Difficulty

The obvious first idea — sieve the values $\prod_{f} f(n)$ for $n \le N$ and count survivors — is exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can show that $\prod_f f(n)$ has few prime factors infinitely often, but they cannot distinguish "one prime factor" from "two", which is why Iwaniec's $n^2+1$ result stops at $P_2$ . The analytic input that works for degree one — the nonvanishing of Dirichlet $L$ -functions on $\Re s = 1$ — has no known analogue for a polynomial of degree $\ge 2$ , because the relevant counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are elementary or already available in Mathlib; the goal itself is not expected to be resolved here.

Formalization scope

Conventions fixed by the Lean development, and deliberately so:

The family is a finite set of polynomials, so repeated polynomials collapse, and it is allowed to be empty (the goal is then a statement about all of $\mathbb{N}$ , and true).
Primality is asserted of the absolute value $|f(n)|$ as a natural number. Since the leading coefficient is positive and $\deg f \ge 1$ , the values are eventually positive, so this is equivalent to asking for a positive prime value at all large $n$ .
The variable $n$ ranges over $\mathbb{N}$ , not $\mathbb{Z}$ , and "infinitely often" means that the set of such $n$ is infinite.
Irreducibility is irreducibility in $\mathbb{Z}[X]$ (so primitivity is included), and the degree hypothesis is $\deg f \ge 1$ in the sense of the natural-number degree.
The Schinzel condition is stated as a condition on the product over the family, quantified over all primes $p$ — not over $p$ up to a bound; milestone 2 is what reduces it to a finite check.

The statement admits no trivializing reading: the hypotheses are satisfiable (for example $\{X, X+2\}$ and $\{X^2+1\}$ are admissible, as milestones 5 and 6 require one to verify), so the goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single $n$ .

A complete development needs the admissibility predicates (supplied as the mission's definition bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations. Contributions of further conditional consequences of the goal (Sophie Germain primes, prime $k$ -tuples, cousin primes) are welcome as additions to the tree.

Selected references

A. Schinzel and W. Sierpiński, Sur certaines hypothèses concernant les nombres premiers, Acta Arithmetica 4 (1958), 185–208. DOI
P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Mathematics of Computation 16 (1962), 363–367. DOI
H. Iwaniec, Almost-primes represented by quadratic polynomials, Inventiones Mathematicae 47 (1978), 171–188. DOI
B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Annals of Mathematics 167 (2008), 481–547. arXiv:math/0404188
J. Maynard, Small gaps between primes, Annals of Mathematics 181 (2015), 383–413. arXiv:1311.4600

8 thms2 active usersReviewed

Analysis Partial Differential Equations Probability·Captain: Lucas

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$ , and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.

The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.

Setting

Fix a dimension $d$ and a scaling $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$ , and put $\|x\|_s = \max_i |x_i|^{1/s_i}$ . For $\delta > 0$ , a point $x \in \mathbb{R}^d$ and a test function $\varphi$ , the rescaled test function is

(S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right).

Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$ . For $\alpha<0$ , a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$ , $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$ , $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$ .

A regularity structure $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$ , bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$ ; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$ , and $\Gamma\mathbf{1} = \mathbf{1}$ . Elements of $T_\alpha$ are "homogeneous of order $\alpha$ ": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$ .

A model $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$ , subject to $\Gamma_{xx}=\mathrm{id}$ , $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ , $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds

|(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell.

A modelled distribution of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$

|||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty;

the space of these is $\mathcal{D}^\gamma$ , and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a sector $V$ , that is, a graded $G$ -invariant subspace vanishing in degrees below its regularity.

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

With $\alpha = \min A < 0$ and $r$ the order attached to $A$ , for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a unique distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with

\big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}).

The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.

Milestone level — the calculus around the reconstruction operator

The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$ ; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$ .

Significance

The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.

Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.

Difficulty

The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$ , and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$ : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.

Formalization scope

The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$ . The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$ ; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$ , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$ , and uniqueness simultaneously.

Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$ , the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.

Selected references

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269–504. arXiv:1303.5113, DOI:10.1007/s00222-014-0505-4
T. Lyons, Differential equations driven by rough signals, Revista Matemática Iberoamericana 14 (1998) 215–310. DOI:10.4171/RMI/240
M. Gubinelli, Controlling rough paths, Journal of Functional Analysis 216 (2004) 86–140. arXiv:math/0306433
M. Gubinelli, P. Imkeller, N. Perkowski, Paracontrolled distributions and singular PDEs, Forum of Mathematics Pi 3 (2015) e6. arXiv:1210.2684
Y. Bruned, M. Hairer, L. Zambotti, Algebraic renormalisation of regularity structures, Inventiones Mathematicae 215 (2019) 1039–1156. arXiv:1610.08468

13 thms2 active usersReviewed

Combinatorics Discrete Geometry·Captain: mysticflounder

Superlinear or exact bounds for planar distinct distancesOpen Problem

Superlinear or exact bounds for planar distinct distances

Motivation

This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?

Setting

For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.

Target

The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:

\lim_{n\to\infty} h(n)/n=\infty.

Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.

The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).

Significance and supporting results

A formally verified supporting result, an n^(1/4) additive bound for distinct distances, is

D(P)\ge n/3+c n^{1/4}

for some absolute c > 0 and all sufficiently large n. A complete Lean proof of this supporting theorem has been accepted on this platform. The n^(1/4), n^(1/5), and n^(1/6) theorem targets and their existing milestones are supporting results, not the mission's terminal goal. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.

Difficulty and research priorities

The n^(1/4) proof constructs an algebraic curve from a small distinct-distance count, proves pair separation, and constructs intrinsic curve cells to obtain the curve bound D(S) >= c d^(-4/3) |S|^(4/3) for finite samples S on noncircular, irreducible and absolutely irreducible, maximally circular curves of degree d, under |S|^2 >= T d^5 for absolute constants c,T > 0. The final calculation yields an additive n^(1/4) term. Stronger additive bounds count as intermediate progress; they must not be reported as a superlinear lower bound.

Develop an argument that excludes D(P) <= A n for every fixed A > 0. A fixed-coefficient distance-energy gap is one sufficient route.
Investigate additional structure of the Newton carriers and interactions between their factors, or another geometric or combinatorial route that can control the superlinear target.
Investigate constructions and universal lower bounds together when pursuing an exact extremal determination.
Preserve and formalize useful intermediate theorems while keeping their statements and remaining premises explicit.

Formalization scope

Configurations are finite subsets of the Euclidean plane. In the indexed formalization, a configuration is an injective map p : Fin n → ℝ²; write P = image(p) before using D(P). Both general-position hypotheses apply to the image. D(P) counts distinct positive distance values, not pairs or ordered multiplicities. The superlinear quantifier ranges over every real A > 0 and every sufficiently large general-position configuration.

The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.

Selected references

Erdős Problem 98 — extremal question and bibliography.
Proof of a fourth-root additive bound for planar distinct distances (dated 2026-09-13; revision 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), manuscript, revised 2026-09-14.
Independent audit of the fourth-root additive bound (dated 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 911a06495542d5b4b6cf9f6a41418e4baf4ecd8800b80001b3cc3748f82b0e7b; target SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), 2026-09-14.

31 thms2 active users

Number Theory·Captain: alexcarter

The Erdős–Straus Conjecture (Erdős Problem 242)Open Problem

Egyptian fractions and the Erdős–Straus question

A unit fraction is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number $4/n$ always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.

The conjecture is open. This mission adopts the exact statement maintained as Erdős Problem 242. It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.

The historical formulations vary. Erdős’s 1950 paper, pp. 193–195, discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. His 1961 problem I.32, p. 238, allows positive denominators without specifying distinctness, while the 1979 statement, problem 9, p. 70, explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by Bloom–Elsholtz, pp. 238–239.

The main developments relevant here are:

1950: Obláth’s sufficient condition using a prime divisor of $n+1$ congruent to $3$ modulo $4$ .
1965–1969: Yamamoto’s congruence analysis and Mordell’s exposition reduce the remaining prime cases to six classes modulo $840$ .
1970–1971: Vaughan bounds the density of possible exceptions; Terzi develops a stronger congruence sieve modulo $120120$ .
2013–2022: Elsholtz–Tao analyze representation counts and soluble polynomial congruences; Bloom–Elsholtz give an explicit equivalent covering formulation.
2025: Computational verification is reported through $10^{18}$ . Pomerance–Weingartner study the more general Erdős–Straus–Schinzel problem, including quantitative dependence on a variable numerator.

The exact property

For a natural number $n$ , write $\mathrm{IsErdosStraus}(n)$ for the following literal property:

\exists x,y,z\in\mathbb N,\qquad 1\le x<y<z,\qquad \frac4n=\frac1x+\frac1y+\frac1z.

Every fraction is evaluated in $\mathbb Q$ . The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is $n>2$ ; distinctness is part of the mathematical target. In particular, the prime $2$ cannot simply be imported from a formulation permitting repeated denominators. The boundary value $n=3$ is included, with denominators $1,4,12$ .

Formalization targets

The unresolved root goal is

\forall n\in\mathbb N,\quad n>2\Longrightarrow\mathrm{IsErdosStraus}(n).

The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to $4xyz=n(yz+xz+xy)$ under strict positivity. Positive scaling transports a solution for $n$ to one for $kn$ while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.

The elementary families cover $3\mid n$ , $n\equiv2\pmod3$ , $n\equiv3\pmod4$ , and $n\equiv5\pmod8$ , with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every $n>2$ outside $1\pmod{24}$ . The useful reduction is an equivalence between the root goal and its restriction to primes $p\equiv1\pmod{24}$ ; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in Bloom–Elsholtz, p. 239.

Obláth’s milestone says that $\mathrm{IsErdosStraus}(n)$ holds for $n>2$ whenever $n+1$ has a prime divisor $q\equiv3\pmod4$ . This condition is explicitly recorded in the introduction of Pomerance–Weingartner, which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.

The Mordell–Yamamoto milestone asks for a decomposition for every prime $p>2$ satisfying

p\bmod840\notin\{1,121,169,289,361,529\}.

The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. Yamamoto’s original paper, §§3–4, pp. 42–46, supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains $49$ and omits $529$ ; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.

What these results provide

The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo- $840$ milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.

Later targets include Terzi’s 1971 sieve, whose publisher abstract reports 198 residual classes modulo $120120$ , and Vaughan’s density theorem, bounding the exceptional count by $X\exp(-c(\log X)^{2/3})$ for a positive constant $c$ . Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.

Elsholtz–Tao provide counting results and a classification of polynomially soluble congruences. Bloom–Elsholtz, Theorem 1, pp. 239–240, characterize their conjecture by coverage of all primes by classes

-a/c\pmod{4acd-1}\quad(a,c,d\ge1),

-(4c^2d+1)/k\pmod{4cd}\quad(c,d,k\ge1,\ k\mid4c^2d+1).

Here division by $c$ denotes a modular inverse; division by $k$ is exact integer division. The authors are Bloom and Elsholtz, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. Pomerance–Weingartner address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator $4$ conjecture.

The remaining difficulty

Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.

The current record cites Mihnea–Bogdan (2025) for computational verification through $10^{18}$ . This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.

Formalization scope

The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing Google DeepMind transcription is a statement reference, not an imported proof.

The draft targets Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 with Lean 4.33.1. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with sorry is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo- $840$ formalization task.

Selected references

Erdős, Az … egyenlet egész számú megoldásairól, Mat. Lapok 1 (1950), 192–210; original scan.
Erdős–Graham, Old and New Problems and Results in Combinatorial Number Theory (1980), chapter IV; author’s institutional scan.
Obláth, Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$ , Mathesis 59 (1950), 308–316; bibliographic record, also cited in Pomerance–Weingartner.
Yamamoto, On the Diophantine Equation $4/n=1/x+1/y+1/z$ , Mem. Fac. Sci. Kyushu Univ. A 19 (1965), 37–47; original paper.
Mordell, Diophantine Equations, Academic Press (1969), chapter 30, pp. 287–290; publisher record.
Terzi (1971), Vaughan (1970), Elsholtz–Tao (2013), Bloom–Elsholtz (2022), Mihnea–Bogdan (2025), and Pomerance–Weingartner (2025/2026): primary sources linked at their statements above.

15 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Weak Pentagon Colorings of Triangle-Free Cubic Graphs (OPG-434)Open Problem

Motivation

The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.

Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.

Setting

Let $G$ be a finite simple triangle-free cubic graph. A five-edge coloring here is any symmetric assignment

c:E(G)\longrightarrow\{1,2,3,4,5\}.

It need not be proper or surjective. For a color $i$ , delete all edges with label $i$ while retaining every vertex. The coloring is a weak-pentagon coloring when each of the five resulting spanning graphs is bipartite.

Equivalently, each color class is an odd-cycle edge transversal: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.

A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.

Formalization targets

Weak pentagon conjecture

The root target is

\forall G\text{ finite, simple, triangle-free, and cubic}, \qquad \exists c:E(G)\to[5]\ \forall i\in[5], \quad G-c^{-1}(i)\text{ is bipartite}.

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

\bigl(\forall i,\ G-c^{-1}(i)\text{ is bipartite}\bigr) \quad\Longleftrightarrow\quad \bigl(\forall i,\ c^{-1}(i)\text{ meets every odd cycle of }G\bigr).

This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.

Sixteen-vertex homomorphism formulation

For every finite simple graph $G$ ,

G\text{ has a weak-pentagon coloring} \quad\Longleftrightarrow\quad G\longrightarrow H_{16},

where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.

Significance

The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.

Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.

Difficulty

The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.

High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.

Formalization scope

Colors are Fin 5. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.

The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are candidate_only; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.

Selected references

R. Šámal, Weak pentagon problem, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
M. DeVos and R. Šámal, High-girth cubic graphs are homomorphic to the Clebsch graph, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
P. Kolman, B. Lidický, and J.-S. Sereni, On Minimum Fair Odd Cycle Transversal, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
Open Problem Garden / UnsolvedMath, OPG-434. https://www.unsolvedmath.com/problems/OPG-434

4 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Two Acyclic Colors for Planar Orientations (OPG-169)Open Problem

Motivation

The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.

Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.

Setting

Let $G$ be a finite simple planar graph. An orientation $D$ assigns exactly one direction to every edge of $G$ , with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$ , the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$ .

A two-coloring is a map

c:V(D)\longrightarrow\{0,1\}.

It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.

Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.

Formalization targets

Two Color Conjecture

The goal is

\forall D\text{ an orientation of a finite simple planar graph}, \qquad \exists c:V(D)\to\{0,1\}, \quad D[c^{-1}(0)]\text{ and }D[c^{-1}(1)]\text{ are acyclic}.

Disconnected graphs and empty color classes are included.

Least-order counterexample structure

A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:

D\text{ least-order counterexample} \quad\Longrightarrow\quad D\text{ strongly connected and }\delta(U(D))\ge3.

The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.

Semidegree candidate

A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains candidate_only.

Significance

The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.

The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.

Difficulty

Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.

Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.

Formalization scope

A directed graph is a binary relation, coupled to a SimpleGraph by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.

The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.

Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.

Selected references

Open Problem Garden / UnsolvedMath, OPG-169: The Two Color Conjecture. https://www.unsolvedmath.com/problems/OPG-169
B. Mohar, Eigenvalues and colorings of digraphs, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
Z. Li and B. Mohar, Planar digraphs of digirth four are 2-colourable, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114

4 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: Goku

The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
2019. Aaronson surveys a decade of partial progress (retrospective).
2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree- $d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$ , carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$ . Writing $x^{\oplus i}$ for $x$ with its $i$ -th bit flipped, the influence of coordinate $i$ on $p$ is

\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$ .

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$ , all $d$ , every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$ , some coordinate $i$ satisfies

\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$ -query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$ . Without it, no such concentration is known at any rate polynomial in $1/d$ .

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$ , which yields a coordinate with influence at least $4\varepsilon/N$ . This is tight for the dictator $p(x)=x_1$ and depends on $N$ , so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$ . A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$ : a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$ . Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$ , which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level- $k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

4 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Circular (20,7)-Coloring of Triangle-Free Subcubic Planar Graphs (OPG-401)Open Problem

Motivation

Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio $20/7$ .

The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.

Setting

For integers $p\ge 2q>0$ , a $(p,q)$ -coloring of a finite simple graph $G$ is a map

\varphi:V(G)\longrightarrow \mathbb Z_p

such that the shortest cyclic distance between $\varphi(u)$ and $\varphi(v)$ is at least $q$ for every edge $uv$ . Equivalently, using representatives in $\{0,\ldots,p-1\}$ , the modular difference lies between $q$ and $p-q$ , inclusive. The circular chromatic number is the infimum of the ratios $p/q$ for which such a coloring exists.

The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.

Formalization targets

Root question

The central target is

G\text{ finite, simple, planar, triangle-free, and }\Delta(G)\le 3 \quad\Longrightarrow\quad G\text{ has a }(20,7)\text{-coloring}.

This is exactly the claim $\chi_c(G)\le 20/7$ in a form suitable for finite Lean data.

Local extension table

A reusable finite milestone freezes the local palette arithmetic. For $a\in\mathbb Z_{20}$ , let $A(a)$ be the colors at cyclic distance at least seven from $a$ . For all $a,b$ ,

|A(a)\cap A(b)|=7-d_{20}(a,b), \qquad A(a)\cap A(b)\ne\varnothing\iff d_{20}(a,b)\le6.

This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only candidate_only; the mission publishes the statement as an open formal target rather than claiming it as proved.

Significance

A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.

Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.

Difficulty

The obvious induction on vertices fails at degree two. A coloring of $G-v$ need not extend over $v$ : if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of $G-v$ has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.

A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield $(20,7)$ -colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.

Formalization scope

Lean represents colors by Fin 20 and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound $7$ and the formal upper bound $13$ . Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.

The definition bundle contains no theorem and no sorry. Draft theorem items contain exactly one := by sorry. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.

Selected references

X. Zhu, Circular chromatic number of triangle-free planar graphs with maximum degree three, open-problem page. https://www.math.nsysu.edu.tw/~zhu/open-problems/chic-k3free-planar.htm
Open Problem Garden, OPG-401. https://www.unsolvedmath.com/problems/OPG-401
X. Zhu, The fractional version of Hedetniemi's conjecture is true, European Journal of Combinatorics, 2011. https://doi.org/10.1016/j.ejc.2011.03.004
Z. Dvořák, J.-S. Sereni, and J. Volec, Subcubic triangle-free graphs have fractional chromatic number at most 14/5, Journal of the London Mathematical Society, 2014. https://arxiv.org/abs/1301.5296

3 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Six Colors for Star Edge-Coloring Subcubic Graphs (OPG-37271)Open Problem

Motivation

A star edge coloring is a proper edge coloring with an additional local restriction: no path or cycle of four edges may use only two colors. It sits between ordinary proper edge coloring and strong edge coloring. The problem is local enough to admit finite obstruction searches, but global enough that independently valid local colorings may fail to fit together.

Dvořák, Mohar, and Šámal proved in 2013 that every subcubic multigraph has a star edge coloring with seven colors and conjectured that six always suffice. The Open Problem Garden records the simple-graph version as OPG-37271. The value six would be best possible because the complete bipartite graph $K_{3,3}$ has star chromatic index six.

Subsequent work has proved the six-color bound under additional hypotheses. Lei, Shi, and Song proved it for subcubic multigraphs with maximum average degree less than $5/2$ and obtained a five-color result below $24/11$ . Casselgren, Granholm, and Raspaud proved the conjecture for cubic Halin graphs and several bipartite families. These results leave the unrestricted finite subcubic case as the target of this mission.

Setting

Let $G$ be a finite simple undirected graph. An edge coloring assigns to each unordered edge of $G$ one color from a finite palette. It is proper if two distinct edges incident with the same vertex always have different colors.

A simple path of four edges has five pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ and consecutive edges $v_0v_1,v_1v_2,v_2v_3,v_3v_4$ . It is bichromatic in a proper coloring exactly when the first and third edges have the same color and the second and fourth edges have the same color. The path need not be induced: additional chords do not remove it. A four-cycle has four pairwise distinct vertices and is bichromatic under the analogous alternating equalities, including the closing edge.

A coloring is a star edge coloring when it is proper and contains neither type of bichromatic four-edge configuration. The star chromatic index $\chi'_s(G)$ is the least palette size admitting such a coloring. A graph is subcubic when every vertex has at most three neighbors.

Formalization targets

Goal — the six-color conjecture

The main target is the exact OPG-37271 assertion for finite simple graphs:

\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 6.

In the Lean statement, this is expressed directly as the existence of a coloring by Fin 6; no separate minimization operator is needed.

Known upper bound

The first literature milestone is the established seven-color theorem:

\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 7.

Formalizing this result provides a checked baseline and infrastructure that a six-color argument can reuse.

Sharpness at $K_{3,3}$

The second literature milestone records both sides of the exact value

\chi'_s(K_{3,3})=6.

Thus the mission cannot be completed by weakening the goal to a larger universal constant.

Significance

A proof would determine the universal star chromatic-index bound for graphs of maximum degree three and would match the known lower-bound example $K_{3,3}$ . A counterexample, if one exists, would separate six from the established seven-color bound and identify the first genuinely seven-chromatic subcubic graph.

The formalization contributes a reusable definition of star edge coloring on Mathlib finite simple graphs. In particular, it fixes several conventions that are easy to blur in informal or computational work: forbidden paths have four edges rather than four vertices; they are simple but need not be induced; four-cycles are checked separately; and properness is not inferred merely from the absence of an alternating four-edge pattern. These definitions can support certified bounded searches, verified coloring certificates, and later formalizations of sparse or planar special cases.

The current research repository contains candidate-only local extension criteria and finite certificates. They may motivate future milestones, but they are not treated here as proofs of the conjecture, as admitted evidence, or as replacements for the literature milestones.

Difficulty

A direct greedy coloring argument can fail at a newly inserted edge because a color may be forbidden either by an adjacent edge or by a bichromatic four-edge path created several incidences away. Deleting a low-degree vertex and coloring the remaining graph therefore does not guarantee that the old coloring extends without recoloring. Explicit small configurations already witness failure of this zero-recoloring strategy while remaining globally six-colorable.

The known seven-color proof has one extra color available to break such interactions. Reaching six requires coordinating local recolorings or extracting stronger structure from a minimal counterexample. Finite searches can test configurations and produce certificates, but bounded verification alone cannot establish the universal quantifier over all finite graphs.

Formalization scope

The mission uses SimpleGraph with an arbitrary finite vertex type. Edges are unordered edge-set elements, and palettes are the labeled finite types Fin k. The graph need not be connected, cubic, planar, or nonempty; isolated vertices and the empty graph are included. “Subcubic” means degree at most three, not degree exactly three.

A forbidden path is represented by five pairwise distinct vertices and four consecutive adjacencies. It is not required to be induced. A forbidden cycle is represented separately by four pairwise distinct vertices and four cyclic adjacencies. Under the properness hypothesis, equality of opposite edge colors is precisely the bichromatic alternating pattern.

A complete development should supply the known seven-color theorem, certify the exact value for $K_{3,3}$ , and then address the six-color goal. Contributions formalizing faithful special cases or reusable extension lemmas are welcome, but sampled graph families and successful SAT searches remain finite evidence unless converted into a general Lean proof.

Selected references

Z. Dvořák, B. Mohar, and R. Šámal, Star chromatic index, Journal of Graph Theory 72 (2013), 313–326. arXiv:1011.3376
H. Lei, Y. Shi, and Z.-X. Song, Star chromatic index of subcubic multigraphs, Journal of Graph Theory 88 (2018), 566–576. arXiv:1701.04105
C. J. Casselgren, J. B. Granholm, and A. Raspaud, On star edge colorings of bipartite and subcubic graphs, Discrete Applied Mathematics 298 (2021), 21–33. arXiv:1912.02467
Open Problem Garden, Star chromatic index of subcubic graphs, OPG-37271. Problem page
Vibe Mathing candidate repository, OPG-37271 star chromatic index of subcubic graphs, candidate-only artifacts at commit ddc49c1978a196490702150bb75264793a658457. Repository

4 thms2 active usersReviewed

Discrete Geometry Group Theory·Captain: xuanji

230 space groupsTextbook

Motivation: classify three-dimensional periodic symmetry

A space group describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in Oliver Knill’s survey, §94, “Crystallography,” p. 41. Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.

The target is the known classification result selected by LeanEval v1, not an unsolved classification conjecture. Its authoritative specification is the declaration LeanEval.Geometry.SpaceGroupsProblem.space_groups. The accompanying benchmark manifest attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.

Setting: groups, transformations, and orientation

For a natural number $d$ , let $E(d)=\mathbb R^d$ with its Euclidean inner product. A Euclidean isometry is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the benchmark’s definitions, $G$ is discrete when, for every point $x$ and every real $\varepsilon>0$ , the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.

Such a group is crystallographic when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$ . These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called cocompact, its actual content is the existence of these independent translations, not a separately assumed compact quotient.

An affine equivalence between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An orientation-preserving affine equivalence additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The Sohncke subfamily restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the source definitions and notes.

Target: one conjunction, with all three exact counts

Write $C_{\mathrm{OP}}(d)$ for crystallographicCountOP d, $C(d)$ for crystallographicCount d, and $C_{\mathrm{OP,only}}(d)$ for crystallographicCountOPOnly d. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is

C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.

This is the exact benchmark conjunction, in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.

Significance: exact cardinalities for the underlying groups

The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in Knill, §94; the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.

The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The benchmark source currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.

Difficulty: a catalog is not a completeness theorem

A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the source’s cardinality assertion. The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.

Formalization scope: preserve the benchmark model

The Lean representation is EuclideanSpace ℝ (Fin d), with affine isometries and affine equivalences from Mathlib. The three source counting functions use Set.encard in the extended natural numbers $\mathbb N\cup\{\infty\}$ . More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.

One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$ . Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.

Selected references

LeanEval contributors; problem submitted by Kim Morrison. LeanEval v1: 230 space groups, statement revision 1, 2026, repository commit 296b7491ec989d21bcf8636a9a69231a1e5d1d25. Exact Lean source; manifest with historical bibliography.
Oliver Knill. Some Fundamental Theorems in Mathematics, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. Full text. This provides background for the three counts; the exact formal conventions are those of LeanEval above.

17 thms2 active usersReviewed

Functional Analysis Pure Mathematics·Captain: ShouqiaoWang

Zhang–Si–Si: Corrected Resonant Almost-Periodic Poincaré–Treshchev PersistenceResearch Paper

Motivation

The classical persistence problem asks which invariant tori of an integrable Hamiltonian survive a small perturbation. A resonance makes some internal angular frequencies vanish, and an almost-periodic perturbation introduces infinitely many additional forcing frequencies. Zhang, Si, and Si state a Poincaré–Treshchev persistence theorem for this combined regime: most lower-dimensional resonant tori associated with nondegenerate relative equilibria persist as infinite-dimensional invariant tori in Theorem 2.7. The formal mission targets that headline result in corrected form. It retains the paper’s nonresonance, spatial-shell, and averaged-critical-point hypotheses, while making explicit the full frequency twist and reduced-frequency parameter chart used later in the paper but absent from the printed theorem statement.

Setting

Let $n,m>0$ and $d=n+m$ . The internal variables are $x\in\mathbb T^d$ and $y\in G\subset\mathbb R^d$ , where $G$ is bounded and closed. The external forcing angles and their conjugate actions are $\theta\in\mathbb T^{\mathbb Z}$ and $J\in\ell^1(\mathbb Z;\mathbb R)$ . The suspended Hamiltonian is

\mathcal H_\epsilon(\theta,J,x,y)= \sum_{j\in\mathbb Z}\omega_jJ_j+N(y)+\epsilon P(\theta,x,y,\epsilon).

Here $N$ is real analytic near $G$ . A primitive rank- $m$ resonance lattice is represented by an integer matrix $K_0=(K_1,K_2)$ with $\det K_0=1$ , where the last $m$ columns generate the lattice. The adapted angles are $(\psi,\phi)=K_0^{\mathsf T}x$ , with $\psi\in\mathbb T^n$ and $\phi\in\mathbb T^m$ . Writing $\nabla N$ for the actual derivative of $N$ , define

O(g,G)=\{y\in G:K_2^{\mathsf T}\nabla N(y)=0\}, \qquad \Omega(y)=K_1^{\mathsf T}\nabla N(y).

The averaged potential $h_0(\phi,y)$ is the zero external and zero $\psi$ Fourier coefficient of $P$ at $\epsilon=0$ . A pair $(\phi,y)$ is associated and nondegenerate when

\nabla_\phi h_0(\phi,y)=0, \qquad \det D_\phi^2h_0(\phi,y)\ne0.

Let $O_0$ be the subset of $O(g,G)$ admitting such a $\phi$ , let $\Omega_0=\Omega(O_0)$ , and trim in reduced-frequency coordinates:

\Omega_\xi=\{\eta\in\Omega_0:\operatorname{dist}(\eta,\partial\Omega_0)\ge\xi\}, \qquad O_\xi=O_0\cap\Omega^{-1}(\Omega_\xi).

The perturbation has the paper’s spatial-shell Fourier expansion over finite shells $A$ in a spatial structure $\mathcal S$ . With $[A]=1+\sum_{j\in A}\log^{\varrho}(1+|j|)$ for $\varrho>2$ , each shell has a uniform analytic Fourier bound $B_A$ , and $\sum_AB_Ae^{s[A]}<\infty$ for some $s>0$ . Every nonzero admissible finite external mode $k$ satisfies

|\langle k,\omega\rangle|\ge \frac{\gamma}{\Delta([[k]])\Delta(|k|_1)},

where $\gamma>0$ , $[[k]]$ is the minimum shell weight containing its support, and $\Delta$ is a nondecreasing approximation function with $\Delta(0)=1$ , $\log\Delta(t)/t\downarrow0$ , and $\int_0^\infty\log\Delta(t)t^{-2}\,dt<\infty$ .

Target

Assume that $O_0$ is nonempty. On every sufficiently small trim $O_\xi$ , require compactness and positive $n$ -dimensional measure in the $\Omega$ chart, injectivity of $D(\nabla N)(y)$ , an analytic lower-Lipschitz diffeomorphism $\Omega:O_\xi\to\Omega_\xi$ , and nondegeneracy of every averaged critical point retained by the conclusion. Then, for every $0<\xi\le\xi_*$ , there are $0<\epsilon_0\le1$ , a rate $c(\epsilon)\to0$ as $\epsilon\downarrow0$ , and closed measurable nonempty sets $\Lambda_\epsilon\subset O_\xi$ for $0<\epsilon\le\epsilon_0$ such that

\operatorname{vol}_n\bigl(\Omega(O_\xi\setminus\Lambda_\epsilon)\bigr) \longrightarrow0\qquad(\epsilon\downarrow0).

For every $y\in\Lambda_\epsilon$ and every associated nondegenerate $\phi$ , construct a topological embedding

\iota_{\epsilon,y,\phi}:\mathbb T^{\mathbb Z}\times\mathbb T^n \longrightarrow (\mathbb T^{\mathbb Z}\times\ell^1)\times (\mathbb T^d\times\mathbb R^d)

that is analytic almost periodic with the same shell structure, is the image of the standard resonant torus under a local canonical transformation, is $c(\epsilon)$ -close to that torus, and is invariant under $\mathcal H_\epsilon$ with rotation vector $(\omega,\Omega(y))$ .

Significance

The result combines three features that are usually separated: a positive-rank internal resonance, an infinite external frequency vector, and persistence for an asymptotically full-measure parameter set. It identifies the surviving object in the full suspended phase, including the external actions, rather than only in the finite internal fibre. The paper contains a proof of its printed theorem; the mission’s open work is a Lean proof of the corrected target. The correction exposes the parameter twist and chart assumptions on which the reduction and measure assertion depend, so a completed formalization would distinguish the theorem’s stated content from hypotheses needed to make that content mathematically controlled.

Difficulty

Finite-dimensional Diophantine notation does not control infinitely many external modes: admissibility, support weights, and the decay of $\Delta$ must interact without leaving an empty mode class. Resonance also removes $m$ internal frequencies and replaces the original parameter set by a lower-dimensional surface. Its ambient Euclidean boundary is therefore unsuitable for a positive trim, and ordinary ambient volume is unsuitable for the majority statement. Finally, persistence must be expressed simultaneously as an invariant solution of the actual Hamilton equations, an analytic almost-periodic embedding, and a canonical equivalence in the suspended phase; any one of these conditions alone admits objects that do not express the theorem.

Formalization scope

The Lean representation uses finitely supported integer external modes, a covering spatial structure, the literal shell-indexed norm, complex-neighborhood coefficient analyticity, and a separate absolute-summability guard for every infinite Fourier sum. Unit modes are provably admissible. The averaged potential, its gradient and Hessian, the internal frequency $\nabla N$ , the resonant set, and the reduced-frequency map are transparent definitions. Nonemptiness of $O_0$ , positive volume of every allowed $\Omega_\xi$ , and nonempty $\Lambda_\epsilon$ rule out empty-set and zero-measure trivializations.

The formal target strengthens the printed assumptions only where the source’s reduction requires missing control: $D(\nabla N)$ is injective on the retained trim, and $\Omega$ is an analytic diffeomorphism there with a uniform lower Lipschitz bound. The boundary distance and excluded volume are both taken in the $n$ -dimensional reduced-frequency chart. The word “Cantor” is represented by closedness, measurability, nonemptiness, and asymptotically full measure; perfectness and total disconnectedness are not additional targets.

The torus lives in a genuine $\ell^1$ external-action space. Its action component has one weighted- $\ell^1$ -valued shell expansion, and the Hamiltonian pairing and external action velocity carry convergence guards. A local conjugacy is a homeomorphism between open neighborhoods, fixes $\theta$ , is differentiable along all $\ell^1$ action directions and finitely supported external-angle directions, and preserves $\sum_jd\theta_j\wedge dJ_j+\sum_i dx_i\wedge dy_i$ on those cylinder directions. Reusable contributions include spatial-shell Fourier classes, approximation functions, reduced-manifold measure interfaces, weighted infinite canonical forms, and coordinatewise Hamiltonian invariance.

Selected references

Yuan Zhang, Wen Si, and Jianguo Si, Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations, Discrete and Continuous Dynamical Systems 52 (2026), 32–69. DOI: 10.3934/dcds.2026043. Main result: Theorem 2.7, journal p. 39 (PDF p. 8); spatial and nonresonance definitions: Definitions 2.2–2.4 and equations (5)–(7), journal pp. 35–38 (PDF pp. 4–7); reduction exposing the additional twist and parameter-change requirements: Lemma 3.2, journal pp. 41–43 (PDF pp. 10–12).

3 thms2 active usersReviewed

Quantum Information·Captain: Goku

Universal recovery map for approximate Markov chainsResearch Paper

Motivation

A central question in quantum information theory is to determine how well lost information can be reconstructed. Crucially, the corresponding recovery operation should perform well without knowing the information to be reconstructed. In this work, we show that the quantum conditional mutual information measures the performance of such recovery operations. More precisely, we prove that the conditional mutual information $I(A:C|B)$ of a tripartite quantum state $ρ_{ABC}$ can be bounded from below by its distance to the closest recovered state $\mathcal{R}_{B \to BC}(ρ_{AB})$ , where the $C$ -part is reconstructed from the $B$ -part only and the recovery map $\mathcal{R}_{B \to BC}$ merely depends on $ρ_{BC}$ . One particular application of this result implies the equivalence between two different approaches to define topological order in quantum systems.

This mission is the statement-level formalization of Universal recovery map for approximate Markov chains (arXiv:1504.07251v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Commuting rotations give a state-dependent linear recovery bound (Lemma 6.1, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

21 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 2.1: universal recovery for separable systems: Extended CMI and a coordinate-to-bounded-operator realization compatible with recovery, tensor action and marginals (hard)
Remark 2.2: measured-relative-entropy strengthening: Extended CMI and realized finite-channel amplification on arbitrary separable ancillas (hard)
Remark 2.3: the universal map recovers its prescribed marginal: Universal-validity predicate built from realized coordinate recovery and extended CMI (hard)
Corollary 2.4: linear bound and unital recovery structure: Realized separable recovery, extended CMI and the supported finite unital structure (hard)
Remark 2.5: commuting-unitary mixture for the linear bound: Realized universal recovery and an integrable probability mixture of supported rotated transpose maps (hard)
Remark 2.5: semidefinite optimization and efficiency claim: Remark 2.5: semidefinite optimization and efficiency claim (source-ambiguity)
Remark 2.5: generic replacement by imaginary powers: Remark 2.5: generic replacement by imaginary powers (source-ambiguity)
Example 2.6: product marginal and unique transpose recovery: Realization-compatible product recovery, extended CMI and universal supported uniqueness (hard)
§3, eq.(15): topological-order application: §3, eq.(15): topological-order application (source-ambiguity)
Proposition 4.1: pointwise-to-universal minimax principle: Proposition 4.1: pointwise-to-universal minimax principle (source-ambiguity)
Lemma 4.2: measured-entropy slack properties: Realization-compatible CMI, measured entropy, flagged mixtures and slack topology (hard)
Lemma 5.1: uniform comparison under normalized BC compression: Realized local tensor projections, positive-trace joint compression and extended-CMI slack (hard)
Lemma 5.2: compression of approximately marginal-preserving channels: Realized input/output channel compression and fixed-marginal slack infima (hard)
Lemma 5.3: trace retained by a compressed channel: Realized channel action compatible with arbitrary local projections and marginals (hard)
Lemma 6.2: linear fidelity slack properties: Realized flagged tensor action, CMI and trace-norm topology for arbitrary separable ancillas (hard)
§7: conditional universal relative-entropy improvement: Realization-compatible global extension family and relative-entropy recovery slack (hard)
Lemma C.4: fidelity continuous in a finite-dimensional recovery map: Operator realization of coordinate amplification and its root fidelity on arbitrary separable ancillas (hard)
Lemma C.5: continuity of a channel tensored with identity: Cross-system operator realization of coordinate amplification and compatible trace-norm topology (hard)
Lemma E.1: fidelity with a projected positive operator: Realized tensor-local projections and normalization compatible with local root fidelity (hard)
Lemma E.3: fixed-marginal finite-support approximations: Arbitrary bounded local projections acting on coordinate states with exact-marginal support slices (hard)
Appendix F: additional fourth-root counterexample claim: Full-scope separable-system transpose recovery and fidelity comparison, compatible with the accepted coordinate tensor model (hard)

Selected references

Universal recovery map for approximate Markov chains, arXiv:1504.07251v3, https://arxiv.org/abs/1504.07251v3

20 thms1 active userReviewed

Quantum Information·Captain: Goku

General bounds for sender-receiver capacities in multipoint quantum communicationsResearch Paper

Motivation

We investigate the maximum rates for transmitting quantum information, distilling entanglement, and distributing secret keys between a sender and a receiver in a multipoint communication scenario, with the assistance of unlimited two-way classical communication involving all parties. First we consider the case where a sender communicates with an arbitrary number of receivers, so called quantum broadcast channel. Here we also provide a simple analysis in the bosonic setting where we consider quantum broadcasting through a sequence of beamsplitters. Then, we consider the opposite case where an arbitrary number of senders communicate with a single receiver, so called quantum multiple-access channel. Finally, we study the general case of all-in-all quantum communication where an arbitrary number of senders communicate with an arbitrary number of receivers. Since our bounds are formulated for quantum systems of arbitrary dimension, they can be applied to many different physical scenarios involving multipoint quantum communication.

This mission is the statement-level formalization of General bounds for sender-receiver capacities in multipoint quantum communications (arXiv:1603.07262v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Broadcast Choi teleportation simulation (§III, Eq.(28) and Fig.3: broadcast Choi teleportation simulation, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

16 results of the paper are not stated yet, because the library lacks an interface they need:

§V, Eq.(68): finite-dimensional sender-receiver REE upper bound: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
§§III–V, unnumbered: operational task hierarchy with helpers: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use (hard)
§III, Eqs.(29)–(30): actual broadcast output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
§III, Eqs.(31)–(34): broadcast output REE and regularized converse: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal; regularized Choi REE and the supremum of existing limiting actual-output REE rates (hard)
§III, Eqs.(35)–(36): broadcast single-copy capacity bound: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
§III.A, Eqs.(38)–(40): bosonic broadcast simulation and fixed-n stretching: Normal bosonic channels and finite-energy teleportation instruments on arbitrary references, TMSV resources, trace-norm output semantics, and fixed-n hybrid energy bounds; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
§III.A, Eqs.(41)–(43), and §§IV–V: asymptotic-REE capacity extensions: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
§III.B, Eqs.(44)–(45): cascade factorization and separable comparators: The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
§III.B, Eq.(46): asymptotic Choi-family bottleneck: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
§III.B, Eq.(49): thermal-loss broadcast numeric bottleneck: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
§III.B, Eq.(50): vacuum-loss broadcast bottleneck: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; the vacuum specialization of The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
§III.B, Eq.(51): arbitrary Gaussian-unitary cascade flux bottleneck: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
§IV, Eqs.(55)–(56): actual multiple-access output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
§IV, Eq.(57): multiple-access output REE: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
§IV, Eqs.(58)–(60): multiple-access regularized and single-copy bounds: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal; the supremum over existing output-REE limits and regularized resource REE (hard)
§V, Eqs.(64)–(65): actual interference output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)

Selected references

General bounds for sender-receiver capacities in multipoint quantum communications, arXiv:1603.07262v2, https://arxiv.org/abs/1603.07262v2

8 thms1 active userReviewed

Quantum Information·Captain: Goku

Unconstrained distillation capacities of a pure-loss bosonic broadcast channelResearch Paper

Motivation

Bosonic channels are important in practice as they form a simple model for free-space or fiber-optic communication. Here we consider a single-sender two-receiver pure-loss bosonic broadcast channel and determine the unconstrained capacity region for the distillation of bipartite entanglement and secret key between the sender and each receiver, whenever they are allowed arbitrary public classical communication. We show how the state merging protocol leads to achievable rates in this setting, giving an inner bound on the capacity region. We also evaluate an outer bound on the region by using the relative entropy of entanglement and a `reduction by teleportation' technique. The outer bounds match the inner bounds in the infinite-energy limit, thereby establishing the unconstrained capacity region for such channels. Our result could provide a useful benchmark for implementing a broadcasting of entanglement and secret key through such channels. An important open question relevant to practice is to determine the capacity region in both this setting and the single-sender single-receiver case when there is an energy constraint on the transmitter.

This mission is the statement-level formalization of Unconstrained distillation capacities of a pure-loss bosonic broadcast channel (arXiv:1601.05563v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Actual TMSV broadcast conditional entropies and their unconstrained limits (Appendix after (29); Section III.A, (12)-(13), p.3, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

6 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 1, (4)-(6): Unrestricted bosonic joint entanglement/private-state operational capacity region (hard)
Theorem 2, (27): Arbitrary-m unrestricted joint Bell/private distillation region and its cut theorem (hard)
Section III.A, (8)-(10); Appendix (28)-(29): Bosonic reverse state-merging distillation protocols for finite-energy TMSV resources (hard)
Remark 3: Sequential reverse-merging execution and absence of entanglement borrowing at every stage (hard)
Section III.B displacement covariance and teleportation reduction: Normalized continuous-variable teleportation instruments and actual adaptive broadcast-output reduction (hard)
Section III.B, (17)-(20); Appendix (31): Energy limit and ordered operational interpretation in (17)-(20)/(31) (source-ambiguity)

Selected references

Unconstrained distillation capacities of a pure-loss bosonic broadcast channel, arXiv:1601.05563v3, https://arxiv.org/abs/1601.05563v3

6 thms1 active userReviewed

Quantum Information·Captain: Goku

Capacities of repeater-assisted quantum communicationsResearch Paper

Motivation

We consider quantum and private communications assisted by repeaters, from the basic scenario of a single repeater chain to the general case of an arbitrarily-complex quantum network, where systems may be routed through single or multiple paths. In this context, we investigate the ultimate rates at which two end-parties may transmit quantum information, distribute entanglement, or generate secret keys. These end-to-end capacities are defined by optimizing over the most general adaptive protocols that are allowed by quantum mechanics. Combining techniques from quantum information and classical network theory, we derive single-letter upper bounds for the end-to-end capacities in repeater chains and quantum networks connected by arbitrary quantum channels, establishing exact formulas under basic decoherence models, including bosonic lossy channels, quantum-limited amplifiers, dephasing and erasure channels. For the converse part, we adopt a teleportation-inspired simulation of a quantum network which leads to upper bounds in terms of the relative entropy of entanglement. For the lower bounds we combine point-to-point quantum protocols with classical network algorithms. Depending on the type of routing (single or multiple), optimal strategies corresponds to finding the widest path or the maximum flow in the quantum network. Our theory can also be extended to simultaneous quantum communication between multiple senders and receivers.

This mission is the statement-level formalization of Capacities of repeater-assisted quantum communications (arXiv:1601.00966v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Widest path: equality with the minimum maximum-edge cut (Proposition 12, Eq.(131), PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

56 results of the paper are not stated yet, because the library lacks an interface they need:

Main result: loss-chain capacity, Eqs.(6),(74): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Theorem 1 (Weak converse): Adaptive point-to-point protocol; Normal-state REE in bits; Operational channel capacity; Asymptotic output-REE supremum (source-ambiguity)
Lemma 3 (Tele-covariance and simulability): Teleportation covariance; Normalized Choi state; Finite teleportation LOCC; TMSV state; Bosonic teleportation instrument; Pointwise referenced simulation (hard)
Lemma 6 (Chain stretching): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
Theorem 7 (Single-letter REE bound), full statement: Chain capacity; Cut resource REE; Normalized and asymptotic Choi resources; One-way distillable entanglement; Entanglement swapping (source-ambiguity)
Theorem 7, finite-resource branch including Eq.(72): Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Lemma 8 (Network stretching): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
Lemma 9 (Network stretching with cuts): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
Theorem 10 (Converse for single-path capacity): Sequential capacity; Resource representation; Single-edge REE cut value (source-ambiguity)
Theorem 11 (Lower bound): Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
Corollary 13 (Single-path capacities): Distillable network; Single-path capacity; REE cut; Widest path; Routing complexity; One-way protocol (source-ambiguity)
Theorem 14 (Converse for multi-path capacity), full statement: Flooding capacity; Resource representation; Multi-edge REE flow (source-ambiguity)
Theorem 14, exact normal-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Theorem 15 (Lower bound): Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
Corollary 16 (Multi-path capacities), full statement: Distillable network; Multi-edge REE; Operational capacity; Maximum flow; One-way teleportation protocol (source-ambiguity)
Corollary 16, operational min-cut equality and achieving strategy: Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
Theorem 17 (Multi-unicast with single paths): Multiple-unicast sequential protocols; Independent pair targets; Capacity region; Subset cut constraints; Single-edge REE flow (source-ambiguity)
Corollary 18: Multiple-unicast region; Distillable edge capacities; Subset endpoint cuts; Maximum-edge cut capacity (source-ambiguity)
Theorem 19 (Multi-unicast with multipaths), full statement: Multiple-unicast flooding protocol; Independent pair targets; Capacity region; Subset cut inequalities; Multi-edge REE flow (source-ambiguity)
Theorem 19, exact-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Corollary 20: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
Theorem 21 (Quantum multicast), full statement: Independent-message multicast protocol; Distinct target factors; Capacity region; Symmetric multicast capacity; Receiver subset cuts; REE sums (source-ambiguity)
Theorem 21, exact-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Corollary 22: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
Theorem 23 (Network coding for QKD): Common-key multicast capacity; Unicast flooding key capacity; Distillable link protocols; Classical linear network coding; Shared undirected-edge resource budget (source-ambiguity)
Theorem 24 (Quantum multiple-multicast), full statement: Multiple-multicast flooding protocol; Independent pair targets; Symmetric-per-sender rate region; Sender subset cuts with a receiver on opposite side; REE and operational cut sums (source-ambiguity)
Theorem 24, exact-resource and operational distillable clauses: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Task equivalences for chains and networks: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
Chain weak converse, Eq.(60): Chain protocol; Output REE; Protocol-family limit and supremum (source-ambiguity)
Amplifier-chain capacity, Eq.(75): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Qubit dephasing-chain capacity, Eq.(76): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Qubit erasure-chain capacity, Eq.(77): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Qudit and hybrid distillable-chain extension: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
One-bit threshold and optical distance rule: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Optimal equidistant placement, Eqs.(78)–(79): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Repeater-dominant asymptotic scaling, Eq.(80): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Loss-dominant scaling, Eq.(81): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Multiband chain bound and equality, Eqs.(86)–(87): Independent band tensor-product channel; Band resource representation; Multiband chain capacity; REE sums; Distillable band capacities (source-ambiguity)
Multiband chain finite-resource bound and operational bottleneck equality: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
Multiband lossy-chain capacity, Eq.(88): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Multiband high-loss scaling, Eq.(89): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Network peeling error and fixed-protocol convergence, Eqs.(104)–(106): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
Optimized average-cut bound, Eqs.(121)–(122): Sequential protocols; Actual edge-use frequencies; Optimal-use vector; Protocol-dependent cut REE sum (source-ambiguity)
Loss-network single-path formula, Eqs.(138)–(140): Pure-loss channel; Sequential network capacity; Cut and path transmissivity extrema (source-ambiguity)
Amplifier-network single-path formula, Eq.(143): Quantum-limited amplifiers; Sequential capacity; Cut and route gains (source-ambiguity)
Dephasing-network single-path formula, Eqs.(146)–(147): Qubit dephasing; Sequential capacity; Binary entropy; Cut/path error parameters (source-ambiguity)
Erasure-network single-path formula, Eq.(149): Qubit pure-flag erasure; Sequential capacity; Cut/path erasure parameters (source-ambiguity)
Teleportation-covariant multipath sandwich, Eqs.(164)–(165): Teleportation covariance; Operational edge and flooding capacities; Normalized Choi REE; Cut sums (source-ambiguity)
Loss-network multipath capacity, Eq.(171): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Multiband loss-network multipath formulas, Eqs.(172)–(174): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Amplifier-network multipath formula, Eq.(175): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Dephasing-network multipath formula, Eq.(176): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Erasure-network multipath formula, Eq.(177) and qudit extension: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Symmetric diamond routing comparison, Eq.(21): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
Common-key versus independent-key multicast: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
Independent pair-rate bounds, Eqs.(250)–(253): Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)

Selected references

Capacities of repeater-assisted quantum communications, arXiv:1601.00966v4, https://arxiv.org/abs/1601.00966v4

2 thms1 active userReviewed

Quantum Information·Captain: Goku

Sending quantum entanglement through noisy channelsResearch Paper

Motivation

This paper addresses some general questions of quantum information theory arising from the transmission of quantum entanglement through (possibly noisy) quantum channels. A pure entangled state is prepared of a pair of systems $R$ and $Q$ , after which $Q$ is subjected to a dynamical evolution given by the superoperator $\superop^{Q}$ . Two interesting quantities can be defined for this process: the entanglement fidelity $F_{e}$ and the entropy production $S_{e}$ . It turns out that neither of these quantities depends in any way on the system $R$ , but only on the initial state and dynamical evolution of $Q$ . $F_{e}$ and $S_{e}$ are related to various other fidelities and entropies, and are connected by an inequality reminiscent of the Fano inequality of classical information theory. Some insight can be gained from these techniques into the security of quantum cryptographic protocols and the nature of quantum error-correcting codes.

This mission is the statement-level formalization of Sending quantum entanglement through noisy channels (arXiv:quant-ph/9604023v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6.2, equations (24)–(25): quantum Fano inequality (§6.2, equations (24)–(25): quantum Fano inequality, PDF p. 27). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

§7, concluding recovery claim: A specified metric, input/uniformity domain, and quantitative recovery claim for low entropy production implying nearly unitary dynamics. (source-ambiguity)

Selected references

Sending quantum entanglement through noisy channels, arXiv:quant-ph/9604023v1, https://arxiv.org/abs/quant-ph/9604023v1

38 thms1 active userReviewed

Quantum Information·Captain: Goku

Multiparty Quantum Mutual Information: An alternative definitionResearch Paper

Motivation

Mutual information is the reciprocal information that is common to or shared by two or more parties. Quantum mutual information for bipartite quantum systems is non-negative, and bears the interpretation of total correlation between the two subsystems. This may, however, no longer be true for three or more party quantum systems. In this paper, we propose an alternative definition of multipartite information taking into account the shared information between two and more parties. It is non-negative, observes monotonicity under partial trace as well as completely positive maps, and equals multipartite information measure in literature for pure states. We then define multiparty quantum discord, and give some examples. Interestingly, we observe that quantum discord increases when measurement is performed on a large number of subsystems. Consequently, the symmetric quantum discord, which involves measurement on all parties, reveals the maximal quantumness. This raises question on the interpretation of measured mutual information as classical correlation.

This mission is the statement-level formalization of Multiparty Quantum Mutual Information: An alternative definition (arXiv:1504.07176v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Alternative multipartite information is nonnegative (Theorem 1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

6 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 3: Locality and trace normalization of the claimed operation (source-ambiguity)
Equation (11), final equality: Replica-space identification and valid support containment for equation (11) (source-ambiguity)
Equation (12), final equality: Replica-space identification and matching marginals in equation (12) (source-ambiguity)
Equation (13), last line: General tensor-power representation of complementary marginal entropy sum (source-ambiguity)
Equation (14), numerical n=3,4 claim and saturation: A valid domain and a specified pair-index set for the numerical bound (source-ambiguity)
Figure 2(c) caption: Normalized noisy three-qutrit family in Figure 2(c) (source-ambiguity)

Selected references

Multiparty Quantum Mutual Information: An alternative definition, arXiv:1504.07176v2, https://arxiv.org/abs/1504.07176v2

15 thms1 active userReviewed

Quantum Information·Captain: Goku

Concentrating Partial Entanglement by Local OperationsResearch Paper

Motivation

If two separated observers are supplied with entanglement, in the form of $n$ pairs of particles in identical partly-entangled pure states, one member of each pair being given to each observer; they can, by local actions of each observer, concentrate this entanglement into a smaller number of maximally-entangled pairs of particles, for example Einstein-Podolsky-Rosen singlets, similarly shared between the two observers. The concentration process asymptotically conserves {\em entropy of entanglement}---the von Neumann entropy of the partial density matrix seen by either observer---with the yield of singlets approaching, for large $n$ , the base-2 entropy of entanglement of the initial partly-entangled pure state. Conversely, any pure or mixed entangled state of two systems can be produced by two classically-communicating separated observers, drawing on a supply of singlets as their sole source of entanglement.

This mission is the statement-level formalization of Concentrating Partial Entanglement by Local Operations (arXiv:quant-ph/9511030v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entropy-efficient exact singlet concentration (Abstract, §I: asymptotically efficient concentration of pure entanglement, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

§III, Eqs.(7),(9): batching reaches near powers of two: An IID binomial type-history process, positive-time near-power hitting/stopping events, and its physically counted stopped-batch singlet-efficiency functional. (hard)
§IV: two-sided QDC is not entanglement concentration: A complete largest-eigenvalue compressed two-sided state with rounded/capped dimension, fixed spectral tie order, positive-success normalization, and same-dimension Bell/Haar teleportation fidelity. (hard)
§IV: growth of Schmidt-coefficient variance: The probability distribution and scaling underlying the asserted Schmidt-coefficient variance. (source-ambiguity)
§IV footnote 1: majority-up encoding and marginal spectra: The input ensemble determining the majority-up marginal density matrices. (source-ambiguity)
§IV: quantum compression followed by concentration and teleportation: A typed source-averaged compression/concentration/teleportation composition with a deterministic compressed-qubit requirement, heralded concentration supply, and separated classical-message accounting. (hard)

Selected references

Concentrating Partial Entanglement by Local Operations, arXiv:quant-ph/9511030v1, https://arxiv.org/abs/quant-ph/9511030v1

24 thms1 active userReviewed

Quantum Information·Captain: Goku

Compression of sources of probability distributions and density operatorsResearch Paper

Motivation

We study the problem of efficient compression of a stochastic source of probability distributions. It can be viewed as a generalization of Shannon's source coding problem. It has relation to the theory of common randomness, as well as to channel coding and rate--distortion theory: in the first two subjects ``inverses'' to established coding theorems can be derived, yielding a new approach to proving converse theorems, in the third we find a new proof of Shannon's rate--distortion theorem. After reviewing the known lower bound for the optimal compression rate, we present a number of approaches to achieve it by code constructions. Our main results are: a better understanding of the known lower bounds on the compression rate by means of a strong version of this statement, a review of a construction achieving the lower bound by using common randomness which we complement by showing the optimal use of the latter within a class of protocols. Then we review another approach, not dependent on common randomness, to minimizing the compression rate, providing some insight into its combinatorial structure, and suggesting an algorithm to optimize it. The second part of the paper is concerned with the generalization of the problem to quantum information theory: the compression of mixed quantum states. Here, after reviewing the known lower bound we contribute a strong version of it, and discuss the relation of the problem to other issues in quantum information theory.

This mission is the statement-level formalization of Compression of sources of probability distributions and density operators (arXiv:quant-ph/0208131v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Common-randomness compression with typical-word guarantees (Theorem 9, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

Question 4: Unconditional no-shared-randomness block-error achievability at mutual information. (source-ambiguity)
Question 4': Ordinary block-error compression with simultaneous typical-word fidelity at mutual information. (source-ambiguity)
Section VI.C: A source-pinned multi-constraint rate-distortion formula with precise feasible set and boundary approximation convention. (source-ambiguity)
Conjecture 23: Proved quantum visible compression with the stated communication and randomness rates. (source-ambiguity)
Question 24: Unconditional quantum fixed-error compression equality at Holevo information. (source-ambiguity)

Selected references

Compression of sources of probability distributions and density operators, arXiv:quant-ph/0208131v1, https://arxiv.org/abs/quant-ph/0208131v1

24 thms1 active userReviewed

Quantum Information·Captain: Goku

Quantum Channel Capacity of Very Noisy ChannelsResearch Paper

Motivation

We present a family of additive quantum error-correcting codes whose capacities exceeds that of quantum random coding (hashing) for very noisy channels. These codes provide non-zero capacity in a depolarizing channel for fidelity parameters $f$ when $f> .80944$ . Random coding has non-zero capacity only for $f>.81071$ ; by analogy to the classical Shannon coding limit, this value had previously been conjectured to be a lower bound. We use the method introduced by Shor and Smolin of concatenating a non-random (cat) code within a random code to obtain good codes. The cat code with block size five is shown to be optimal for single concatenation. The best known multiple-concatenated code we found has a block size of 25. We derive a general relation between the capacity attainable by these concatenation schemes and the coherent information of the inner code states.

This mission is the statement-level formalization of Quantum Channel Capacity of Very Noisy Channels (arXiv:quant-ph/9706061v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Five-in-five cat concatenation strictly improves hashing (Abstract and Section V.B: five-in-five concatenation improves the hashing threshold, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

Section V.A, Eqs. (40)-(41): two claimed asymptotic contributions: The central-syndrome partial contribution, its index window, the constant c, and the intended asymptotic equivalence including polynomial prefactors. (source-ambiguity)
Numerical reports: Table I, five-in-five, and note [36]: Certified precision or a rounding convention for Table I, the five-in-five threshold, and reference note [36]. (source-ambiguity)
Section VI: limited Monte-Carlo search observation: A specified Monte-Carlo search experiment: sampled code set, fidelity range, sampling distribution, transcript, and stopping rule. (source-ambiguity)
Section VI: proposed extension to generalized depolarizing channels: A precise generalized-channel or k>1 extension, with modified weight polynomials and operational statement. (source-ambiguity)
Reference note [20]: typical hashing distance heuristic: A probability model and limit quantifiers for “typical,” an asymptotic error statement, and an exact meaning of coefficient .8. (source-ambiguity)

Selected references

Quantum Channel Capacity of Very Noisy Channels, arXiv:quant-ph/9706061v3, https://arxiv.org/abs/quant-ph/9706061v3

12 thms1 active userReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Schinzel's Hypothesis HOpen Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Setting

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for γ>0\gamma>0γ>0

Milestone level — the calculus around the reconstruction operator

Significance

Difficulty

Formalization scope

Selected references

Superlinear or exact bounds for planar distinct distancesOpen Problem

Superlinear or exact bounds for planar distinct distances

Motivation

Setting

Target

Significance and supporting results

Difficulty and research priorities

Formalization scope

Selected references

The Erdős–Straus Conjecture (Erdős Problem 242)Open Problem

Egyptian fractions and the Erdős–Straus question

The exact property

Formalization targets

What these results provide

The remaining difficulty

Formalization scope

Selected references

Weak Pentagon Colorings of Triangle-Free Cubic Graphs (OPG-434)Open Problem

Motivation

Setting

Formalization targets

Weak pentagon conjecture

Odd-cycle equivalence

Sixteen-vertex homomorphism formulation

Significance

Difficulty

Formalization scope

Selected references

Two Acyclic Colors for Planar Orientations (OPG-169)Open Problem

Motivation

Setting

Formalization targets

Two Color Conjecture

Least-order counterexample structure

Semidegree candidate

Significance

Difficulty

Formalization scope

Selected references

The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Circular (20,7)-Coloring of Triangle-Free Subcubic Planar Graphs (OPG-401)Open Problem

Motivation

Setting

Formalization targets

Root question

Local extension table

Significance

Difficulty

Formalization scope

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

Sharpness at $K_{3,3}$