Famous Open Problems

Motivation

Brocard's problem asks for all natural numbers $n$ such that $n! + 1$ is a perfect square. Henri Brocard raised the question in 1876 and again in 1885, and Srinivasa Ramanujan independently posed it in 1913 in the Journal of the Indian Mathematical Society. Only three solutions are known, and the problem is listed as Erdős problem #398 (erdosproblems.com/398). It is one of the simplest-looking Diophantine equations mixing a multiplicative object (the factorial) with an additive shift, and it is a standard test case for conjectures such as the abc conjecture.

Timeline

• 1876, 1885 — Brocard asks whether $n! + 1 = m^2$ has solutions other than $n = 4, 5, 7$.
• 1913 — Ramanujan poses the same question (Question 469, J. Indian Math. Soc.).
• 1993 — Overholt shows that, conditionally on (a weak form of) the abc conjecture, the equation has only finitely many solutions (Wikipedia summary).
• 2000 — Berndt and Galway report a computer search finding no solutions other than $n = 4, 5, 7$ for $n < 10^9$.
• Later searches — the search bound was extended further (Matson, to $10^{12}$; Epstein and Glickman, to $10^{15}$), again without new solutions.

No unconditional proof of finiteness is known.

Setting

For a natural number $n$, the factorial is $n! = 1 \cdot 2 \cdots n$, with $0! = 1$. A Brown number pair is a pair $(n, m)$ of natural numbers with

$$n! + 1 = m^2 .$$

The three known pairs are $(4, 5)$, $(5, 11)$ and $(7, 71)$, since $25 = 5^2$, $121 = 11^2$ and $5041 = 71^2$.

For the conditional milestone, the radical $\operatorname{rad}(N)$ of a natural number $N$ is the product of the distinct primes dividing $N$. The abc conjecture asserts: for every $\varepsilon > 0$ there is $K_\varepsilon > 0$ such that for all positive integers $a, b, c$ with $\gcd(a, b) = 1$ and $a + b = c$,

$$c < K_\varepsilon \, \operatorname{rad}(abc)^{1+\varepsilon}.$$

Formalization targets

Goal — Brocard's problem

$$\{(n, m) \in \mathbb{N}^2 : n! + 1 = m^2\} = \{(4, 5),\ (5, 11),\ (7, 71)\}.$$

This says both that the three known pairs are solutions and that there are no others.

Milestones

1. Known solutions: $4! + 1 = 5^2$, $5! + 1 = 11^2$, $7! + 1 = 71^2$.
2. Berndt–Galway search bound: if $n < 10^9$ and $n! + 1 = m^2$, then $n \in \{4, 5, 7\}$.
3. Overholt (conditional finiteness): if the abc conjecture holds, then $\{(n, m) : n! + 1 = m^2\}$ is finite.

Significance

A resolution would settle a question open since 1876 and would be one of the rare complete solutions of a factorial Diophantine equation of this kind. The conditional finiteness result is a standard illustration of how the abc conjecture controls equations of the form $n! + A = m^2$.

For the formalization, the known-solutions milestone is a finite computation. The search-bound milestone is a large verified computation; a machine-checked certificate for it would be a reusable artifact. The conditional finiteness milestone formalizes a published argument that assumes the abc conjecture as a hypothesis. The goal itself is an open problem; none of these statements is known to have a machine-checked proof on this platform at the time of drafting.

Difficulty

Congruence obstructions cannot rule out large solutions: for every modulus $M$ and every $n \ge M$ one has $n! \equiv 0 \pmod M$, so $n! + 1 \equiv 1 = 1^2 \pmod M$ is a square modulo $M$. Local arguments alone therefore cannot close the problem. The known finiteness argument depends on the abc conjecture, which is itself unproved in the standard form used here. Computer searches only give lower bounds on any further solution.

Formalization scope

• Numbers are natural numbers (ℕ); $m$ ranges over $\mathbb{N}$, so the sign of $m$ is not an issue. The factorial is Mathlib's Nat.factorial, with $0! = 1$.
• The goal is stated as an equality of sets of ordered pairs in $\mathbb{N} \times \mathbb{N}$, so it cannot be satisfied by proving only one inclusion.
• The radical is defined as the product over the prime factors of $N$ (so $\operatorname{rad}(0) = \operatorname{rad}(1) = 1$; the value at $0$ never enters since $a, b, c > 0$).
• The abc conjecture is a Prop-valued definition used as a hypothesis in the conditional milestone; it is not asserted anywhere. The exponent $1 + \varepsilon$ is a real power.
• Overholt's published result assumes only a weak form of abc; the milestone assumes the standard form, which implies the weak form, so the milestone is a consequence of the published result.
• All declarations live in the namespace Brocard.

Selected references

• H. Brocard, Question 166, Nouv. Corresp. Math. 2 (1876), 287; Nouv. Ann. Math. (3) 4 (1885), 391.
• S. Ramanujan, Question 469, J. Indian Math. Soc. 5 (1913), 59.
• M. Overholt, The Diophantine equation $n! + 1 = m^2$, Bull. London Math. Soc. 25 (1993), 104.
• B. C. Berndt and W. F. Galway, On the Brocard–Ramanujan Diophantine equation $n! + 1 = m^2$, Ramanujan J. 4 (2000), 41–42.
• Erdős problem #398: https://www.erdosproblems.com/398
• Brocard's problem, Wikipedia: https://en.wikipedia.org/wiki/Brocard%27s_problem
• Formal Conjectures (Google DeepMind): https://github.com/google-deepmind/formal-conjectures

Motivation

The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound $\pi/2+2/\pi\approx2.2074$ and the upper bound $2\sqrt{2}\approx2.828$ in 1968. Joseph Gerver constructed a shape of area approximately $2.2195$ in 1992 and described four constants $A$, $B$, $\varphi$, $\theta$ satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.

Timeline: Moser poses the problem (1966); Hammersley gives the $\pi/2+2/\pi\approx2.2074$ lower bound and the $2\sqrt{2}\approx2.828$ upper bound (1968); Gerver exhibits the $2.2195$ shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).

Setting

Work in the plane $\mathbb{R}^2$. The hallway is $(-\infty,1]\times[0,1]\cup[0,1]\times(-\infty,1]$, the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set $s$ in the horizontal side together with a continuous path $m$ of plane isometries indexed by the unit interval, starting at the identity, keeping the image of $s$ inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group $E(2)$; continuity together with $m(0)=\mathrm{id}$ forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas $\mathrm{volume}(s)$ over all moving sofas. The supremum is finite, at least $11/5$, and attained.

Gerver's shape is defined from a rotation path. For constants $A$, $B$, $\varphi$, $\theta$, let $r$ be the piecewise function with breakpoints $\varphi$, $\theta$, $\pi/2-\theta$, $\pi/2-\varphi$ from Romik's Theorem 2, let $x$ and $y$ be its cosine and sine integrals, and let $p$ be the associated translation path. The sofa for those constants is the intersection over angles in $[0,\pi/2]$ of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with $0\le\varphi\le\theta\le\pi/4$ and $0\le A$, $0\le B$. The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.

Formalization targets

Goal: optimality of Gerver's sofa

For every $A$, $B$, $\varphi$, $\theta$ satisfying ABphiThetaSpec,

$$\mathrm{sofaConstant} = \mathrm{volume}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta)).$$

The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.

Supporting targets

$$\exists!\,(A,B,\varphi,\theta),\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta).$$ $$\forall\,A,B,\varphi,\theta,\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta)\implies \exists\,m,\ \mathrm{IsMovingSofa}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta),m).$$

The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.

Significance

The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure $11/5\le\mathrm{volume}\le\infty$ proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional $Q$ on caps. Without it the exact maximum remains unknown.

Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.

Difficulty

The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional $Q$ an upper bound, and $Q$ need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle $\pi/2$ are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.

Formalization scope

Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions $r$, $x$, $y$, $p$ take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value $2.2195$ instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the $11/5$ certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.

Selected references

• Jineon Baek, Optimality of Gerver's Sofa, arXiv:2411.19826, 2024. https://arxiv.org/abs/2411.19826
• Joseph L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42 (1992), 267-283.
• Dan Romik, Differential equations and exact solutions in the moving sofa problem, Experimental Mathematics 27 (2018), 316-330. https://arxiv.org/abs/1606.08111
• Dean Cureton et al., MovingSofa: Autoformalization of Baek's solution, 2026. https://github.com/deancureton/MovingSofa
• Google DeepMind, formal-conjectures, FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjectures
• Dawid Trela, GerverSofaLean v1.1.0. https://github.com/dawidmtrela-dotcom/GerverSofaLean

Motivation

A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series $f\in\mathbb{Q}[[z]]$ is algebraic over $\mathbb{Q}[z]$, only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes $p$ may appear, but only after roughly $\omega(p)\gg p$ coefficients — already forces algebraicity.

For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz $p$-curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).

Timeline.

• 1852 — Eisenstein: algebraic power series over $\mathbb{Q}$ have bounded denominators (implication (1)⇒(2) below).
• 1970s — Grothendieck and Katz: the $p$-curvature conjecture for linear differential equations.
• 2025 — Lam and Litt formulate the conjecture for (possibly non-linear) algebraic differential equations and prove it for many equations and initial conditions of algebro-geometric interest, including Picard–Fuchs equations at initial conditions corresponding to cycle classes, and isomonodromy equations such as Painlevé VI and the Schlesinger system at initial conditions corresponding to Picard–Fuchs equations (arXiv:2501.13175).

Setting

Let $f=\sum_{k\ge0}a_kz^k\in\mathbb{Q}[[z]]$ be a formal power series with rational coefficients and write $f^{(i)}$ for its $i$-th formal derivative. Let $g\in\mathbb{Q}(z,y_0,\dots,y_{n-1})$ be a rational function in $n+1$ variables. The series $f$ solves the algebraic ODE defined by $g$ if

$$f^{(n)}(z)=g\bigl(z,f(z),f'(z),\dots,f^{(n-1)}(z)\bigr)$$

and $g$ is defined at $\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)$. Concretely, $g=p/q$ for polynomials $p,q$ with $q\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)\neq0$ and $f^{(n)}\cdot q(z,f,\dots,f^{(n-1)})=p(z,f,\dots,f^{(n-1)})$.

For $N\in\mathbb{N}$, $\mathbb{Z}[1/N]\subseteq\mathbb{Q}$ is the subring generated by $1/N$. For a function $\omega$ from the primes to $\mathbb{Z}$, the coefficients of $f$ are $\omega$-integral if for every prime $p$ the numbers $a_0,\dots,a_{\omega(p)}$ lie in $\mathbb{Z}_{(p)}$ (denominators prime to $p$); $\omega$ is superlinear if $\omega(p)/p\to\infty$.

Formalization targets

Goal: the Lam–Litt conjecture

For $f$ solving an algebraic ODE as above, the following are equivalent:

$$\text{(1) } f \text{ is algebraic over } \mathbb{Q}[z];\qquad \text{(2) } \exists N,\ \forall k,\ a_k\in\mathbb{Z}[1/N];\qquad \text{(3) } \exists\,\omega \text{ superlinear with } (a_k) \ \omega\text{-integral}.$$

Milestones

• (1)⇒(2), Eisenstein's theorem (no ODE hypothesis needed).
• (2)⇒(3), elementary (no ODE hypothesis needed).
• (3)⇒(2), open.
• (2)⇒(1), open; Litt's Problem 1.

Together the four milestones imply the goal; the last two are the open content of the conjecture.

Significance

A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz $p$-curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.

For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.

Difficulty

Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as $\sum_k\binom{2k}{k}^2z^k$. Its equation is singular at $z=0$, which the non-singularity hypothesis on $g$ excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.

Formalization scope

• Power series are PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is $z$ and variable i + 1 is $f^{(i)}$.
• The ODE hypothesis is existential: some representation $g=p/q$ with $q$ nonzero at the initial point and $f^{(n)}q(\dots)=p(\dots)$ as power series. This non-singularity requirement is essential and must not be dropped.
• Algebraicity is IsAlgebraic (Polynomial ℚ) f, i.e. over $\mathbb{Q}[z]$ (equivalently over $\mathbb{Q}(z)$).
• $\mathbb{Z}[1/N]$ is the subalgebra of $\mathbb{Q}$ generated by $1/N$; since $1/0=0$ in Lean, $N=0$ gives $\mathbb{Z}$.
• $\omega$ takes values in $\mathbb{Z}$; negative values impose no condition at that prime. Superlinearity is the limit $\omega(p)/p\to\infty$ along the primes.
• The goal is a List.TFAE of the three conditions.

Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and $p$-adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.

Selected references

• Y. H. J. Lam, D. Litt, Algebraicity and integrality of solutions to differential equations, arXiv preprint, 2025. https://arxiv.org/abs/2501.13175
• D. Litt, Problem 1, problems list. https://www.problemsilike.com/1
• G. Eisenstein, Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen, Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852.
• Formal Conjectures project, FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Hadwiger's conjecture (1943) asserts that for every integer $t\ge 0$, every graph with no $K_{t+1}$ minor is $t$-colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to $t$-colourability that matters is the presence of a complete graph $K_{t+1}$ as a minor.

Timeline.

• 1937 — Wagner shows that the case $t=4$ is equivalent to the four-colour theorem, via a clique-sum decomposition of graphs with no $K_5$ minor.
• 1943 — Hadwiger poses the conjecture and proves it for $t\le 3$ (graphs with no $K_4$ minor have a vertex of degree at most two).
• 1964 — Wagner proves that graphs with no $K_{t+1}$ minor are $2^t$-colourable.
• 1967 — Mader proves that excluding any fixed minor forces a linear number of edges, and determines the exact extremal function for $K_t$ minors when $t\le 7$.
• 1976 — Appel and Haken prove the four-colour theorem, hence the case $t=4$.
• 1982 — Duchet and Meyniel prove that every $n$-vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$.
• 1984 — Kostochka and Thomason independently show that graphs with no $K_t$ minor have average degree $O(t\sqrt{\log t})$, hence are $O(t\sqrt{\log t})$-colourable.
• 1993 — Robertson, Seymour and Thomas prove the case $t=5$ (using the four-colour theorem).
• 2023–2024 — Norin, Postle and Song, then Delcourt and Postle, improve the general bound to $O(t\log\log t)$ colours.
• (Date not recorded in the survey) Albar and Gonçalves prove that graphs with no $K_7$ minor are $8$-colourable and graphs with no $K_8$ minor are $10$-colourable.

The case $t=6$ (graphs with no $K_7$ minor are $6$-colourable) is the first open case.

Setting

All graphs are finite and simple. A minor of a graph $G$ is any graph obtained from a subgraph of $G$ by contracting edges. Equivalently, a graph $H$ on vertex set $W$ is a minor of $G$ if there are branch sets $B_w\subseteq V(G)$, $w\in W$, which are pairwise disjoint, each inducing a connected (nonempty) subgraph of $G$, and such that for every edge $w_1w_2$ of $H$ some vertex of $B_{w_1}$ is adjacent to some vertex of $B_{w_2}$. $G$ has a $K_t$ minor if the complete graph $K_t$ is a minor of $G$, i.e. $G$ contains $t$ pairwise disjoint connected vertex sets, every two joined by an edge.

A graph is $t$-colourable if its vertices can be coloured with $t$ colours so that adjacent vertices receive different colours; $\chi(G)$ is the least such $t$. Write $\mathrm{HC}(t)$ for the statement "every graph with no $K_{t+1}$ minor is $t$-colourable". A graph is $k$-degenerate if every nonempty set of vertices contains a vertex with at most $k$ neighbours inside the set. The stability number $\alpha(G)$ is the largest size of a set of pairwise non-adjacent vertices.

Formalization targets

Goal

$$\forall t\ge 0:\qquad K_{t+1}\not\preceq G\ \Longrightarrow\ \chi(G)\le t\qquad\text{for every finite graph } G.$$

Proved special cases

$$\mathrm{HC}(t)\ \text{for } t\le 3,\qquad \mathrm{HC}(4),\qquad \mathrm{HC}(5).$$

Weaker colouring bounds

• no $K_{t+1}$ minor $\Rightarrow$ $\chi(G)\le 2^t$ (Wagner);
• no $K_t$ minor $\Rightarrow$ $\chi(G)=O(t\sqrt{\log t})$ (Kostochka, Thomason) and $\chi(G)=O(t\log\log t)$ (Delcourt–Postle);
• no $K_7$ minor $\Rightarrow$ $\chi\le 8$; no $K_8$ minor $\Rightarrow$ $\chi\le 10$ (Albar–Gonçalves).

Supporting extremal and structural results

• non-null graphs with no $K_4$ minor have a vertex of degree $\le 2$;
• $k$-degenerate graphs are $(k+1)$-colourable;
• for every $H$ there is $c$ with $|E(G)|\le c|V(G)|$ whenever $H\not\preceq G$ (Mader);
• the exact edge bounds $n-1$, $2n-3$, $3n-6$ for no $K_3$, $K_4$, $K_5$ minor, and $(t-2)n-\binom{t-1}{2}$ for no $K_t$ minor, $t\le 7$ (Mader);
• every $n$-vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$ (Duchet–Meyniel);
• a graph with no $K_{t+1}$ minor has a $t$-colourable induced subgraph on at least half of its vertices.

Significance

A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of $K_t$-minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.

On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases $t\le 2$ under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases $t\le 3$, Wagner's $2^t$ bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases $t=4,5$ depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.

Difficulty

The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order $t\sqrt{\log t}$, since dense random graphs with no large clique minor have average degree of that order; closing the gap to $t$ requires using large chromatic number itself, not just density. Already for $t=4$ the statement is equivalent to the four-colour theorem, so no short proof is expected for any $t\ge 4$.

Formalization scope

Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. $\mathrm{HC}(t)$ is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case $t=0$ is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.

Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.

Selected references

• P. Seymour, Hadwiger's conjecture, in: Open Problems in Mathematics, Springer, 2016 (survey; source of the milestone numbering).
• Wikipedia, Hadwiger conjecture (graph theory). https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory)
• H. Hadwiger, Über eine Klassifikation der Streckenkomplexe, Vierteljschr. Naturforsch. Ges. Zürich 88 (1943).
• K. Wagner, Über eine Eigenschaft der ebenen Komplexe, Math. Ann. 114 (1937).
• N. Robertson, P. Seymour, R. Thomas, Hadwiger's conjecture for $K_6$-free graphs, Combinatorica 13 (1993).
• A. Kostochka, Lower bound of the Hadwiger number of graphs by their average degree, Combinatorica 4 (1984).
• A. Thomason, An extremal function for contractions of graphs, Math. Proc. Cambridge Philos. Soc. 95 (1984).
• M. Delcourt, L. Postle, Reducing linear Hadwiger's conjecture to coloring small graphs (2024).

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

Does the sharp diagonal constant work for general matrices?

For every real $p\ge256$, the optimal Hlawka constant for complex diagonal matrices is already proved in Lean. This mission asks whether that same constant works for all complex matrices, including rectangular ones. The statement is a conjecture. Accepted diagonal result

Audenaert and Kittaneh's Problem 7 asks for the best constant in the Schatten-norm setting, if one exists. Existence of some finite dimension-independent constant for every real $p>1$ is already settled by the project's Lean theorem. The task here is to establish the specified sharp candidate in the range $p\ge256$. Audenaert–Kittaneh, §8.2, proved existence result

Definitions and the goal

For a complex matrix $A$ with singular values $s_i(A)$, its Schatten norm is

$$N_p(A)=\left(\sum_i s_i(A)^p\right)^{1/p}.$$

There is no normalization by dimension. For three matrices of the same shape, define

$$\Delta_3=N_p(A)+N_p(B)+N_p(C)-N_p(A+B+C),$$ $$\Delta_2=2\bigl(N_p(A)+N_p(B)+N_p(C)\bigr) -N_p(A+B)-N_p(A+C)-N_p(B+C).$$

Formal Schatten-norm definition

The shared cyclic candidate is

$$K_p=\sup_{t\in[1/2,2]} \frac{3(t^p+2)^{1/p}-3^{1/p}|2-t|} {6(t^p+2)^{1/p}-3(2|1-t|^p+2^p)^{1/p}}.$$

The fraction is the deficit ratio for the coordinate triple $(-t,1,1),(1,-t,1),(1,1,-t)$. For $p>1$, its denominator is positive on the displayed interval and the supremum is attained. Cyclic definitions and attainment

The goal asks whether $\Delta_3\le K_p\Delta_2$ for every real $p\ge256$ and every triple of complex matrices of every finite shape. One constant for each exponent must work across all dimensions and triples. The endpoint 256, noninteger exponents, zero dimensions, singular and zero matrices, unequal norms and zero pair deficit are included.

Lean states the goal for complex-linear maps between any two finite-dimensional complex inner-product spaces, allowing different dimensions. No positivity, self-adjointness, commutativity or common diagonalization assumption is imposed.

Why the diagonal proof does not settle this

The singular values determine a matrix's own norm. However, the separate singular-value lists of three matrices do not determine the norms of their pair sums and total sum. The diagonal theorem therefore does not supply the seven matrix norms needed in this inequality. Their relative directions matter as well.

The existing existence theorem supplies a constant, but does not identify it with $K_p$. A proof here needs the exact cyclic constant. A proof only for even integer exponents or a restricted class of matrices would not settle this goal.

What a resolution would establish

If the conjectured bound holds, it is automatically optimal uniformly over all finite matrix shapes: diagonal three-dimensional examples already require at least $K_p$. Thus the missing step is that this constant works for arbitrary matrices. A counterexample would show that the diagonal constant is insufficient somewhere in the stated range. Cyclic lower bound, diagonal Schatten identity

Either outcome addresses this range of exponents; it would not settle the optimal general-matrix constant for every $1<p<256$.

The foundation mission establishes the optimal diagonal constant for every real $p\ge256$. The cutoff-90 mission has since extended the diagonal result in Lean to every real $p\ge90$. The diagonal campaign invites contributors to lower that cutoff below 90.

This mission keeps $p\ge256$ and asks whether the same optimal constant works for arbitrary complex matrices, including rectangular ones. It can be pursued independently of improvements to the diagonal cutoff.

Its three linked milestones are already-proved background: existence, the sharp diagonal result, and the diagonal norm identity. The main general-matrix goal remains open. No complete proof is supplied for it.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa and contributors, Hlawka–Schatten inequalities, Lean source repository, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Existence and diagonal libraries

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 256.
• The accepted diagonal Schatten norm identity.
• The public existence theorem for every real p > 1.

Motivation

Nguyen and Tang study the irreversible catalytic network $\mathcal A+\mathcal B\to\mathcal B+\mathcal C$, $\mathcal B+\mathcal C\to\mathcal A+\mathcal B$, a simple reaction–diffusion system with both a positive and a boundary equilibrium (catalyst used up). They settle every mass regime but one and leave it as a conjecture (AIM problem 416).

Timeline. 2021: Fellner–Morgan–Tang give global classical solutions with uniform bounds. 2026: Nguyen–Tang prove convergence for $M_1<M_2$ and $M_1\ge2M_2$ and local results in between, conjecturing global attraction there.

Setting

On a bounded connected smooth domain $\Omega\subset\mathbb R^n$ with $|\Omega|=1$ and $d_1,d_2,d_3>0$:

$$a_t-d_1\Delta a=b(c-a),\quad b_t-d_2\Delta b=b(c-a),\quad c_t-d_3\Delta c=-b(c-a),$$

with homogeneous Neumann conditions and strictly positive $C^2$ compatible initial data. The masses $M_1=\int_\Omega(a_0+c_0)$, $M_2=\int_\Omega(b_0+c_0)$ are conserved. The equilibria are the positive one $(\frac{M_1}2,\,M_2-\frac{M_1}2,\,\frac{M_1}2)$ and the boundary one $(M_1-M_2,\,0,\,M_2)$.

Formalization target

If $M_2\le M_1<2M_2$, every classical solution converges uniformly on $\Omega$ to the positive equilibrium (no rate required).

Significance

This is the last open regime of Nguyen–Tang's stability analysis. Strict positivity is essential: with $b_0\equiv0$ the solution stays away from the positive equilibrium.

Difficulty

For $M_1\ge M_2$ there is no positive lower bound on $\int_\Omega b$, so entropy dissipation can degenerate near the boundary equilibrium ($b=0$), and the local results do not exclude trajectories approaching it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\Delta$ is Mathlib's Laplacian. The domain is $\Omega=\{\varphi<0\}$ for a $C^\infty$ function $\varphi$ with $\nabla\varphi\ne0$ on $\{\varphi=0\}$; the Neumann condition is the derivative within $\overline\Omega$ in the direction $\nabla\varphi$. Solutions are continuous on $[0,\infty)\times\overline\Omega$ and $C^{1,2}$ for $t>0$, and $L^\infty$ convergence is TendstoUniformlyOn. The goal quantifies over classical solutions; their existence is proved in the literature (Fellner–Morgan–Tang; Nguyen–Tang, Theorem 2.1) but is not part of this statement.

Selected references

• T. L. Nguyen, B. Q. Tang, Stability analysis of irreversible chemical reaction-diffusion systems with boundary equilibria, Z. Angew. Math. Phys. 77, 2026, 199. DOI
• K. Fellner, J. Morgan, B. Q. Tang, Uniform-in-time bounds for quadratic reaction-diffusion systems with mass dissipation in higher dimensions, DCDS-S 14, 2021, 635–651. DOI
• AIM open problems list, problem 416. github.com/MColbrook/AIM

Motivation

A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?

This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless $\mathrm{P}=\mathrm{NP}$, d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.

Historical note

The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.

Setting

Let $X=\{x_0,\ldots,x_{n-1}\}$ be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size $n$; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function $\nu:X\to\{0,1\}$. A positive literal $x_i$ is true when $\nu(x_i)=1$; a negative literal $\neg x_i$ is true when $\nu(x_i)=0$. A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.

The input also contains one positive integer weight $c_i$ for each variable and a positive threshold $t$. The weight of an assignment is

$$w(\nu)=\sum_{i=0}^{n-1} c_i\nu(x_i).$$

The DNF is valid for this problem when every literal index is below $n$ and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least $t$.

Formalization targets

Partial result — weighted satisfiability

For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least $t$ has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.

Partial result — unary-weight falsifiability

For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.

Goal — binary-weight falsifiability

For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.

The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.

Dependency graph

Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)

Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.

Significance

A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly $t$) is a different problem and is outside this mission's scope; the goal here is specifically weight at least $t$.

Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.

Difficulty

The direct search over all $2^n$ assignments is exponential in $n$. Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.

Formalization scope

The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.

The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.

The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.

Selected references

• Albertine Amarilli, “Weighted falsifiability for unambiguous DNFs,” List of open questions in theoretical computer science, https://a3nm.net/work/research/questions/#weighted-falsifiability-for-unambiguous-dnfs.
• Mikaël Monet, “Is this problem on unambiguous DNFs hard?”, Theoretical Computer Science Stack Exchange, https://cstheory.stackexchange.com/questions/53733/is-this-problem-on-unambiguous-dnfs-hard.