Motivation

In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic $3$-manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.

Some rational relations are forced, and for a trivial reason: a degree $n$ cover of a hyperbolic $3$-manifold has $n$ times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic $3$-manifolds have irrational volume ratio. Remarkably, not a single such pair is known.

Setting

The bundle fixes the meaning of every term. Hyperbolic $3$-space is the upper half-space $\{(x,y,z) : z > 0\}$. Its volume is Lebesgue measure with density $z^{-3}$ — the Riemannian volume of the metric $(dx^2+dy^2+dz^2)/z^2$ written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula

$$\cosh d(p,q) \;=\; 1 + \frac{|p-q|^2}{2\,p_3\,q_3}.$$

A Kleinian action is a free, properly discontinuous action by hyperbolic isometries; the quotient is a complete hyperbolic $3$-manifold, discreteness and torsion freeness being consequences rather than hypotheses. The volume of the quotient is the measure of a fundamental domain, in the sense of Mathlib's MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that are finite and positive.

Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its $\mathbb{Q}$-span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying $\mathrm{Isom}(\mathbb{H}^3)$, which is not the subject of this mission.

Formalization targets

The goal is that the volumes are not all rationally related: there are two of them, $v$ and $w$, with $v \neq q w$ for every rational $q$.

Two milestones support it. The first is that passing to a subgroup of index $n$ multiplies the volume by $n$, a fundamental domain for the subgroup being the union of $n$ translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic $3$-manifold exists at all — without which the goal would be vacuously false rather than open.

A stronger form of the question, that the $\mathbb{Q}$-span of the set of volumes is infinite dimensional, is also stated.

Significance

The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field $F$, Humbert's formula gives the covolume as $|\delta_F|^{3/2}\zeta_F(2)/4\pi^2$, so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at $2$; and Neumann and Yang showed that the Bloch invariant of a hyperbolic $3$-manifold lies in a subgroup of finite $\mathbb{Q}$-rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of $\zeta(5)$. The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.

Motivation

The smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1

Historical landmarks

• 1961: Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. Smale, Theorem A
• 1982: Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. Freedman, Theorem 1.6
• 2026: The K3 problem list continues to distinguish this established topological result from the open smooth sphere problem. Problem 4.1, pp. 191–192

Setting

Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.

The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.

For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]

Formalization targets

Main open goal

For every manifold $M$ with the preceding hypotheses, the goal is

$$M\cong_{\mathrm{Top}}S^4 \quad\Longrightarrow\quad M\cong_{\mathrm{Diff}}S^4.$$

This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.

Structural and literature milestones

The atlas formulation has the exact equivalence

$$\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.$$

The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence

$$\operatorname{Structomorph}(\mathcal G^{\infty},M,N) \simeq \operatorname{Diff}^{\infty}(M,N),$$

where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]

Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:

$$M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,$$

where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:

$$F_4\quad\Longrightarrow\quad (\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).$$

Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar

$$c:S^m\times[0,1]\longrightarrow\overline B^{m+1}, \qquad c(u,t)=(1-t/2)u.$$

The collar is a closed embedding, has image

$$\{z\in\overline B^{m+1}:\|z\|\geq1/2\},$$

and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]

Topological two-disk gluing

For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The twisted double identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is

$$X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R) \quad\cong_{\mathrm{Top}}\quad S^{m+1}.$$

This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.

Seam–interior smooth compatibility

For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]

Significance

A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.

The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.

The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.

Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.

Difficulty

A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.

Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.

Formalization scope

The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.

The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.

The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.

Selected references

• R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.

• Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.

• Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.

• Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.

• Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

An almost complex structure gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure (Introduction, p. 1). This mission records that question as an open conjecture, not as an established theorem.

Timeline

• 1957: Newlander and Nirenberg proved that an almost complex structure is integrable exactly when its Nijenhuis tensor vanishes, under the regularity assumptions in their theorem. This turns integrability into a nonlinear first-order differential condition rather than a consequence of the pointwise equation $J^2=-\mathrm{id}$ (article).
• 2014–2021: Bryant’s account of Chern’s program still calls the existence of an integrable almost complex structure on $S^6$ open, while referring to the sphere’s well-known almost complex structure (abstract).
• 2022: Granja and Milivojević state the broader closed-manifold question above and study the topology of spaces of almost complex structures on six-manifolds (SIGMA article).

Setting

Fix an integer $n\ge 3$. Let $M$ be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of real dimension $2n$. An almost complex structure on $M$ is a smooth field

$$J_x:T_xM\longrightarrow T_xM$$

of real-linear maps satisfying $J_x(J_xv)=-v$ for every $x\in M$ and $v\in T_xM$. This condition forces even real dimension, but by itself supplies no complex coordinate charts.

A complex structure of complex dimension $n$ is an atlas with values in $\mathbb C^n$ whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied $J$. It does not claim that every chosen almost complex structure is integrable.

Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: $2n\ge 6$, equivalently $n\ge 3$.

Formalization target

Main open conjecture

For every $n\ge 3$ and every closed connected smooth real $2n$-manifold $M$,

$$M\text{ admits a smooth almost complex structure} \quad\Longrightarrow\quad M\text{ admits a compatible complex atlas of complex dimension }n.$$

“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied $J$ is made.

The real six-dimensional case is essential. Since $S^6$ carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.

Significance

A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for $S^6$. A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.

The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.

Difficulty

The equation $J^2=-\mathrm{id}$ is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of $J$ does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.

The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.

Formalization scope

The namespace AlmostComplexToComplex uses Mathlib’s boundaryless Euclidean manifold model. AlmostComplexStructure n M contains a continuous real-linear map on every tangent space, the pointwise identity $J^2=-\mathrm{id}$, and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.

The main theorem assumes the real atlas is modeled on $\mathbb R^{2n}$ and concludes the existence of charts modeled on $\mathbb C^n$. Mathlib’s IsManifold condition over $\mathbb C$ at order one states complex differentiability of chart transitions. Two $C^\infty$ conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.

This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied $J$ is integrable or homotopic to the one induced by the resulting atlas. A dedicated $S^6$ milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.

Selected references

• Gustavo Granja and Aleksandar Milivojević, Topology of Almost Complex Structures on Six-Manifolds, SIGMA 18 (2022), 093, Introduction, p. 1. DOI; arXiv.
• August Newlander and Louis Nirenberg, Complex Analytic Coordinates in Almost Complex Manifolds, Annals of Mathematics 65 (1957), 391–404. DOI.
• Robert L. Bryant, S.-S. Chern’s Study of Almost-Complex Structures on the Six-Sphere, arXiv:1405.3405v2 (2021 revision), abstract. arXiv.

Motivation

A strongly regular graph with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which every vertex has exactly $k$ neighbours, every pair of adjacent vertices has exactly $\lambda$ common neighbours, and every pair of non-adjacent vertices has exactly $\mu$ common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple $(99,14,1,2)$ is the smallest such case in the family $\lambda = 1$, $\mu = 2$, and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).

Timeline of the problem and of what is known about it:

• 1969/1971 — the parameter set is raised by Norman Biggs in his Southampton lectures (Finite Groups of Automorphisms, LMS Lecture Note Series 6, p. 111).
• 1973 — Berlekamp, van Lint and Seidel construct a strongly regular graph with parameters $(243,22,1,2)$ as the coset graph of the perfect ternary Golay code, settling one of the five feasible parameter tuples in this family.
• 1975 — the existence question appears as Problem 7 (attributed to J. J. Seidel) in R. K. Guy's problem list, The Geometry of Metric and Linear Spaces, Springer LNM 490, pp. 237–238; Conway had worked on it by then.
• 1984 — H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, shows that such a graph cannot be vertex-transitive: no group of automorphisms can act transitively on its 99 vertices.
• 1988 — Brouwer and Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8, 57–61.
• 2004 — Makhnev and Minakova, On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$, Discrete Math. Appl. 14(2), and 2011 — Behbahani and Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Math. 311, 132–144: further restrictions on the possible automorphism groups.
• 2014/2017 — Conway's prize offer publicises the problem.

No graph with these parameters has been found, and no non-existence proof is known.

Setting

Fix a finite vertex set $V$ and a simple graph $g$ on $V$ (irreflexive, symmetric adjacency $\mathrm{Adj}$). For vertices $v,w$ write $N(v) = \{u : \mathrm{Adj}(v,u)\}$ for the neighbourhood of $v$ and $N(v)\cap N(w)$ for the set of common neighbours. The graph $g$ is strongly regular with parameters $(n,k,\lambda,\mu)$, written $\mathrm{IsSRGWith}\ g\ n\ k\ \lambda\ \mu$, when

• $|V| = n$;
• $|N(v)| = k$ for every vertex $v$;
• $|N(v)\cap N(w)| = \lambda$ whenever $v$ and $w$ are adjacent;
• $|N(v)\cap N(w)| = \mu$ whenever $v \neq w$ are non-adjacent.

The case $\lambda = 1$ says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case $\mu = 2$ says that every non-adjacent pair is the pair of opposite corners of exactly one $4$-cycle. Conway's problem asks for $(n,k) = (99,14)$ with these two local conditions.

Counting paths of length two from a fixed vertex gives $k(k-\lambda-1) = (n-k-1)\mu$, which for $\lambda=1$, $\mu=2$ reduces to $2n = k^2 + 2$; with $k = 14$ this yields $n = 99$. Writing $A$ for the adjacency matrix, $I$ for the identity and $J$ for the all-ones matrix, strong regularity is equivalent to the matrix identity $A^2 = kI + \lambda A + \mu(J - I - A)$, which for $(99,14,1,2)$ reads $A^2 + A = 12I + 2J$; the eigenvalues of $A$ other than $k=14$ are then $3$ and $-4$, and integrality of their multiplicities ($54$ and $44$) is one of the feasibility conditions that $(99,14,1,2)$ passes.

Formalization targets

Goal

$$\exists\ \alpha,\ \exists\ g \text{ a simple graph on } \alpha,\quad \mathrm{IsSRGWith}\ g\ 99\ 14\ 1\ 2 .$$

The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters $(99,14,1,2)$. A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.

Supporting targets

$$2n = k^2 + 2, \qquad k \text{ even}, \qquad k \in \{2,4,14,22,112,994\}$$

for every strongly regular graph with $\lambda = 1$, $\mu = 2$: the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.

$$\exists\, g,\ \mathrm{IsSRGWith}\ g\ 9\ 4\ 1\ 2, \qquad \exists\, g,\ \mathrm{IsSRGWith}\ g\ 243\ 22\ 1\ 2$$

the two members of the family that are known to exist: the $3\times 3$ rook's graph (the Paley graph on $9$ vertices) and the Berlekamp–van Lint–Seidel graph.

$$|E(g)| = 693, \qquad |\{\text{triangles of } g\}| = 231, \qquad A^2 + A = 12I + 2J, \qquad g \text{ not vertex-transitive}$$

structural consequences for a hypothetical $99$-graph, the last one being Wilbrink's theorem.

Significance

A $(99,14,1,2)$ graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth $5$ with $99$ points and $231$ lines of size $3$; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions ($\lambda=1$, $\mu=2$) constrain global structure.

Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the $99$-graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at $(9,4,1,2)$ and $(243,22,1,2)$; Wilbrink's non-vertex-transitivity; the integrality restriction on $k$); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of $k$); and the goal itself, which is open mathematics.

Difficulty

The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has $693$ edges among $\binom{99}{2} = 4851$ pairs, and no isomorph-free generation of locally linear graphs on $99$ vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at $(9,4,1,2)$ and $(243,22,1,2)$. On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by $(99,14,1,2)$, so a proof of non-existence needs an argument that does not factor through the parameters alone.

Formalization scope

All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as $3$-cliques), SimpleGraph.adjMatrix over $\mathbb{Z}$, and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains $\lambda$ only through pairs that are actually adjacent and $\mu$ only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, $K_3$) do satisfy IsSRGWith with $\lambda = 1$, $\mu = 2$; the supporting statements carry the cardinality hypotheses ($0 < n$, $1 < n$) that exclude them where needed, and the degenerate degree $k = 2$ is listed explicitly in the classification of feasible degrees.

Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the $(243,22,1,2)$ case; and decision procedures for strong regularity of an explicitly given small graph, for the $(9,4,1,2)$ case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.

Selected references

• N. Biggs, Finite Groups of Automorphisms: Course Given at the University of Southampton, October–December 1969, London Mathematical Society Lecture Note Series 6, Cambridge University Press, 1971, p. 111.
• E. R. Berlekamp, J. H. van Lint, J. J. Seidel, A strongly regular graph derived from the perfect ternary Golay code, in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25–30.
• R. K. Guy, Problems, in: The Geometry of Metric and Linear Spaces, Springer Lecture Notes in Mathematics 490, 1975, pp. 233–244 (Problem 7, J. J. Seidel, pp. 237–238). doi:10.1007/BFb0081147
• H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342–355. PDF
• A. E. Brouwer, A. Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8 (1988), 57–61. doi:10.1007/BF02122552
• A. A. Makhnev, I. M. Minakova, On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$, Discrete Mathematics and Applications 14 (2004), no. 2. doi:10.1515/156939204872374
• M. Behbahani, C. Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Mathematics 311 (2011), 132–144. doi:10.1016/j.disc.2010.10.005
• J. H. Conway, Five $1,000 Problems (Update 2017), OEIS. PDF

For every integer

$$n > 1$$

, there exists a prime p such that

$$n ^2 < p < n^2 + n$$

Motivation

A $P_3$-packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.

A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph $G$ satisfies $\lambda(G)=\lfloor |V(G)|/3\rfloor$. Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.

A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a $P_3$-factor. Candidate C02 gives an explicit proposed family $H_q$ of order $18+12q$ that has $P_3$-factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.

Setting

All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.

A $P_3$-factor is represented by a natural number $b$, together with a bijection

$$\operatorname{Fin}(b)\times\operatorname{Fin}(3)\simeq V(G),$$

such that, in every block, positions $0$ and $1$ are adjacent and positions $1$ and $2$ are adjacent. The path is not required to be induced: an ambient edge between positions $0$ and $2$ is allowed because the two selected path edges still form a copy of $P_3$.

A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching $M$ such that the relative complement $G\setminus M$ is a divisible 2-factor.

The explicit graph $H_q$ is defined on $\operatorname{Fin}(18+12q)$. Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.

Formalization targets

Main goal

For every finite simple graph $G$,

$$\bigl(G\text{ cubic}\bigr)\land \bigl(G\text{ 3-vertex-connected}\bigr)\land 3\mid |V(G)| \quad\Longrightarrow\quad G\text{ has a }P_3\text{-factor}.$$

This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.

Literature and route milestones

The mission also formalizes the $(z1)\Leftrightarrow(z8)$ part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a $P_3$-factor. Two route lemmas state that divisible 2-factors split into $P_3$-factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.

Candidate boundary milestones

The C02 milestones ask first for the complete 18-vertex statement and then for the full family:

$$\forall q\in\mathbb N,\quad H_q\text{ is cubic and 3-vertex-connected, has a }P_3\text{-factor, and has no divisible matching complement}.$$

This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every $H_q$ in the proposed family explicitly satisfies the desired $P_3$ conclusion.

Significance

A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a $P_3$-factor; the C02 family does not claim this.

Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced $P_3$-factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.

Difficulty

The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated $P_3$-factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.

The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to $G$ on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and $P_3$ must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.

The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The $H_q$ family includes $q=0$. The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.

Welcome contributions include proofs of the model lemmas, the finite $H_0$ statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.

Selected references

• A. Kelmans, Packing 3-vertex Paths In Cubic 3-connected Graphs, arXiv:0910.2766v2, 2011, Problem 1.10 (p. 3) and Theorem 3.1 (pp. 7–8). https://arxiv.org/abs/0910.2766v2
• UnsolvedMath, OPG-46613: P3-partitions of cubic 3-connected graphs. https://www.unsolvedmath.com/problems/OPG-46613
• Vibe Mathing, C01: divisible-cycle implication and a 30-vertex obstruction, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md
• Vibe Mathing, C02: an 18-vertex obstruction and an infinite family with P3-factors, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md

Motivation

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

If $|u|$ is algebraic and $u \neq 0$, is $e^{u}$ transcendental? Guy Diaz asked this in 2004 and it is still open. Note it is $e^{u}$, not $e^{|u|}$ — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that $u$ itself may be transcendental while only its modulus is constrained.

The question

Write $\bar{\mathbb{Q}}$ for the algebraic numbers in $\mathbb{C}$ and

$$\mathcal{L}=\{u\in\mathbb{C}\ :\ e^{u}\in\bar{\mathbb{Q}}^{\times}\}$$

for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of $\mathcal{L}$ has algebraic modulus. He states it as

« Soit $u \in \mathbb{C}\setminus\{0\}$ avec $|u| \in \bar{\mathbb{Q}}$ ; alors $\mathrm{e}^{u}$ est transcendant. »

The statement fits on one line and needs no machinery beyond $\exp$ and $|\cdot|$. It has been open for twenty-two years.

It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.

Why it suits a distributed platform

The mission decomposes into work that can be done now, without any open input.

Two milestones are conditional theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all Prop-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.

A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where $u$ and $\bar u$ are $\mathbb{Q}$-linearly dependent.

The remaining two milestones are classical theorems that the platform's Mathlib does not have: Hermite--Lindemann and the six exponentials theorem. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.

Only the top node needs genuinely new transcendence.

One structural remark that shapes the whole ladder: Hermite--Lindemann is a special case of the goal, not just an input to it. If $a \neq 0$ is algebraic then $|a|^{2} = a\bar a$ is algebraic, hence so is $|a|$, and the goal applied to $u := a$ gives that $e^{a}$ is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.

Timeline

1873, 1882	Hermite, then Lindemann: $e^{a}$ is transcendental for algebraic $a \neq 0$. In particular every non-zero element of $\mathcal{L}$ is itself transcendental, so a counterexample $u$ would be a transcendental number with algebraic modulus and algebraic exponential.
1934--35	Gelfond and Schneider settle Hilbert's seventh problem.
1966	Lang's Introduction to Transcendental Numbers records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The four exponentials conjecture stays open, and still is.
1966	Baker's theorem on linear forms in logarithms.
1997	Diaz studies the companion condition $\lvert\tau\rvert^{2}\in\mathbb{Q}$, assertion (4-1), p. 237.
2000	Waldschmidt's Diophantine Approximation on Linear Algebraic Groups states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with $y_1 = \lambda$, $y_2 = \lvert\lambda\rvert$ at p. 15.
2004	Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps $z \mapsto \bar z$ and $z \mapsto \lvert z\rvert$ enter a transcendence proof at all?
2026	A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched.

What is known not to work

For a candidate $u$ one has $u\bar u = |u|^{2}$ with $|u|^{2}$ algebraic, hence

$$\bar u = \frac{|u|^{2}}{u}.$$

So $\bar u$ is not independent data: complex conjugation on $\bar{\mathbb{Q}}(u)$ is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at https://github.com/carlok/diaz-modulus-lean: a ring homomorphism fixing $\bar{\mathbb{Q}}$ and carrying $u$ to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over $\bar{\mathbb{Q}} \oplus \bar{\mathbb{Q}}u \oplus \bar{\mathbb{Q}}\bar u$ separates a candidate from an ordinary complex number placed on the same circle.

The practical consequence for solvers: accumulating algebraic relations between $u$ and $\bar u$ until they collide cannot settle this. A successful attack has to introduce information that is not a rational function of $u$ over $\bar{\mathbb{Q}}$ — which is precisely Diaz's own methodological question, still open.

Mathlib gaps a solver will meet

• Hermite--Lindemann is not in Mathlib. Only the analytic half is present, in Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean — verified in all three of the platform's pinned revisions (0df444a3, c5ea0035, 777aaa61), none of which contains transcendental_exp. Hence the choice to carry it as a Prop and give it its own milestone rather than assume it. There is an open PR, leanprover-community/mathlib4#28013 (feat: Lindemann-Weierstrass Theorem, opened 2025-08-05, label awaiting-author as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.
• Neither Schanuel nor any four-exponentials statement exists in any form. They are defined in the mission's bundle; that is the point, since the tractable content of this mission is what follows from them.
• Algebra.trdeg has almost no computational API. It is cardinal-valued, with transcendence bases and lift_cardinalMk_eq_trdeg, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if $S \subseteq K(t)$ with $t$ transcendental over $K$ then $\operatorname{trdeg}_K K[S] \le 1$". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.

Sources

• G. Diaz, Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle, J. Théor. Nombres Bordeaux 16 (2004), no. 3, 535–553, doi:10.5802/jtnb.459 — the conjecture is §5.1, p. 550; the methodological question is p. 551.
• G. Diaz (1997) — the companion condition $|\tau|^{2}\in\mathbb{Q}$ is assertion (4-1), p. 237.
• M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Grundlehren der mathematischen Wissenschaften 326, Springer 2000 — pp. 15, 399, 614, and Exercise 15.16.
• S. Lang, Introduction to Transcendental Numbers, Addison-Wesley 1966, Ch. 2 (six exponentials, Schanuel's conjecture).
• A. Baker, Transcendental Number Theory, Cambridge University Press 1975, Theorem 1.4 (Hermite--Lindemann).

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

Motivation

Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.

The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.

Setting

A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.

A rainbow directed triangle is a cyclically oriented triangle

$$a\to b\to c\to a$$

whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.

A vertex $s$ is a monochromatic source when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.

The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.

Formalization targets

Root theorem

For every nonempty finite tournament $T$ with a three-coloring of its arcs,

$$T\text{ has a rainbow directed triangle} \quad\lor\quad \exists s\in V(T)\ \forall t\in V(T),\ \text{$s$ reaches $t$ monochromatically}.$$

No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.

Finite order milestone

The first milestone freezes the exact bounded claim supported by the replay package:

$$1\le |V(T)|\le 11\text{ and no rainbow directed triangle} \quad\Longrightarrow\quad T\text{ has a monochromatic source}.$$

The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.

Significance

The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.

The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.

Difficulty

The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.

The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.

Formalization scope

Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.

The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.

Selected references

• Open Problem Garden, Monochromatic reachability versus rainbow triangles, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
• B. Sands, N. Sauer, and R. Woodrow, On monochromatic paths in edge-coloured digraphs, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
• A. Georgakopoulos and P. Sprüssel, On 3-coloured tournaments, 2009. https://arxiv.org/abs/0904.1967
• A. Trygub, Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles, 2023. https://arxiv.org/abs/2304.14579

Motivation

A positive integer is perfect when it equals the sum of its proper divisors: $6 = 1 + 2 + 3$, $28 = 1 + 2 + 4 + 7 + 14$, then $496$, $8128$, and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.

The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if $2^p - 1$ is prime then $2^{p-1}(2^p - 1)$ is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.

A timeline of what is actually proved about a hypothetical odd perfect number $N$:

• Euler (published posthumously in 1849): $N = p^k m^2$ with $p$ prime, $p \equiv k \equiv 1 \pmod 4$, and $p \nmid m$. In particular $N$ is not a perfect square.
• Servais (1887), Sylvester (1888): lower bounds on the number $\omega(N)$ of distinct prime divisors; Sylvester obtained $\omega(N) \ge 5$, and $\omega(N) \ge 8$ when $3 \nmid N$.
• Touchard (1953): $N \equiv 1 \pmod{12}$ or $N \equiv 9 \pmod{36}$. Shorter proofs were later given by Satyanarayana (1959) and Holdener (2002).
• Chein (1979) and Hagis (1980), independently: $\omega(N) \ge 8$; Nielsen (2007): $\omega(N) \ge 9$; Nielsen (2015): $\omega(N) \ge 10$.
• Nielsen (2003): an upper bound in terms of $\omega$, namely $N < 2^{4^{\omega(N)}}$ — the first bound of its kind, later sharpened by Nielsen himself.
• Ochem–Rao (2012): $N > 10^{1500}$; Ochem–Rao (2014): $N$ has at least $101$ prime factors counted with multiplicity.

None of these results, alone or together, rules out an odd perfect number.

Setting

For $n \ge 1$ write $\sigma(n) = \sum_{d \mid n} d$ for the sum of all positive divisors of $n$. Then $n$ is perfect exactly when

$$\sigma(n) = 2n,$$

equivalently when the divisors of $n$ other than $n$ itself sum to $n$. The function $\sigma$ is multiplicative: $\sigma(ab) = \sigma(a)\sigma(b)$ whenever $\gcd(a,b) = 1$, and $\sigma(p^a) = 1 + p + \cdots + p^a$ for a prime power. The quantity $\sigma(n)/n$ is the abundancy index of $n$, so a perfect number is one of abundancy index exactly $2$.

Write $\omega(n)$ for the number of distinct prime divisors of $n$. In Lean, $\omega(n)$ is n.primeFactors.card, and perfection is Mathlib's Nat.Perfect n, which unfolds to ∑ i ∈ n.properDivisors, i = n ∧ 0 < n — the positivity clause is part of the definition, so $n = 0$ is not perfect.

Formalization targets

Goal

$$\forall n \in \mathbb{N}, \quad \sigma(n) = 2n \ \Longrightarrow\ 2 \mid n.$$

Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.

Milestones

The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number $N$:

$$N = p^k m^2, \quad p \text{ prime}, \quad p \equiv k \equiv 1 \ (\mathrm{mod}\ 4), \quad p \nmid m \qquad \text{(Euler)}$$ $$N \text{ is not a perfect square} \qquad \text{(Euler)}$$ $$\omega(N) \ge 3, \qquad \omega(N) \ge 5 \qquad \text{(Servais, Sylvester)}$$ $$N \equiv 1 \ (\mathrm{mod}\ 12) \quad \text{or} \quad N \equiv 9 \ (\mathrm{mod}\ 36) \qquad \text{(Touchard)}$$ $$N < 2^{4^{\omega(N)}} \qquad \text{(Nielsen)}$$

Significance

The result itself. A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be $2^{p-1}(2^p-1)$ for a Mersenne prime $2^p - 1$. A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than $1500$ decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of $\sigma$, and about the multiperfect numbers.

Formalizing it. Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (Archive/Wiedijk100Theorems/PerfectNumbers.lean, as Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect and Theorems.perfect_iff_even_and_mersenne), and the main library carries the divisor-sum API around Nat.Perfect in Mathlib/NumberTheory/Divisors.lean, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing $\sigma$-arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of $\sigma$ on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.

Difficulty

The obvious approach — take Euler's form $N = p^k m^2$ and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation $\sigma(N) = 2N$ has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing $\omega$ weakens the constraints rather than strengthening them, which is why the lower bounds on $\omega$ have advanced by one prime factor per decade at very high computational cost. The upper bound $N < 2^{4^{\omega(N)}}$ makes the search space finite for each fixed $\omega$, but astronomically so.

Formalization scope

The development is stated over ℕ with Mathlib's Nat.Perfect, so positivity is built into the hypothesis and no separate 0 < n assumption appears. Oddness is Odd n, the number of distinct prime divisors is n.primeFactors.card, and Euler's form is stated with explicit residues p % 4 = 1, k % 4 = 1, together with ¬ p ∣ m and n = p ^ k * m ^ 2. No custom definitions are introduced; everything rests on Mathlib's Nat.sigma / Nat.Perfect API.

One caution on the shape of the milestones. Each is stated conditionally, for an $n$ assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved unconditionally in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.

Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for $\sigma$ on odd numbers. Sharper published bounds — larger values of $\omega$, the improved Nielsen bound $N < 2^{4^{\omega(N)} - 2^{\omega(N)}}$, the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.

Selected references

• L. Euler, De numeris amicabilibus, Commentationes arithmeticae 2 (1849), 627–636.
• J. J. Sylvester, Sur les nombres parfaits, Comptes Rendus de l'Académie des Sciences CVI (1888), 403–405.
• J. Touchard, On prime numbers and perfect numbers, Scripta Mathematica 19 (1953), 35–39.
• J. A. Holdener, A theorem of Touchard on the form of odd perfect numbers, American Mathematical Monthly 109 (2002), 661–663.
• P. P. Nielsen, An upper bound for odd perfect numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14.
• P. P. Nielsen, Odd perfect numbers have at least nine distinct prime factors, Mathematics of Computation 76 (2007), 2109–2126.
• P. P. Nielsen, Odd perfect numbers, Diophantine equations, and upper bounds, Mathematics of Computation 84 (2015), 2549–2567.
• P. Ochem and M. Rao, Odd perfect numbers are greater than $10^{1500}$, Mathematics of Computation 81 (2012), 1869–1877.
• P. Ochem and M. Rao, On the number of prime factors of an odd perfect number, Mathematics of Computation 83 (2014), 2435–2439.
• Overview and further pointers: https://en.wikipedia.org/wiki/Perfect_number

Motivation

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.

Say $\alpha$ is $k$-collapsible if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, collapsible if it is $1$-collapsible, and eventually collapsible if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and degree $3$ is open. That one-step cubic case is this mission's goal.

Setting

Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a depressed cubic

$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$

with discriminant $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is totally real (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as

$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$

and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant

$$\tau = e^2/d^3$$

determines the problem up to scaling: the search space is one rational parameter, not two.

Formalization targets

Goal — every cubic algebraic number is collapsible

$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$

This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.

Supporting targets

The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:

1. the product criterion — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. affine invariance, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two sufficient conditions: square discriminant, and the power-family condition subsuming it;
4. three obstructions: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.

The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.

Significance

A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.

The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.

Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.

Difficulty

The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.

Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces

$$\deg f \ \ge\ \pi/\psi.$$

As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.

Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.

In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.

Formalization scope

Representation. IsSplit f says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.

Ruling out a trivialisation. Collapsible places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.

Conventions in the archimedean milestones. In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.

In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.

Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.

Selected references

• Griffin Macris, List of open problems, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
• Miles, Collapsible algebraic numbers, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.