Motivation

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

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

Setting

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

A two-coloring is a map

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

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

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

Formalization targets

Two Color Conjecture

The goal is

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

Disconnected graphs and empty color classes are included.

Least-order counterexample structure

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

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

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

Semidegree candidate

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Weak pentagon conjecture

The root target is

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

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

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

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

Sixteen-vertex homomorphism formulation

For every finite simple graph $G$,

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.

Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.

Setting

A finite simple graph is chordal when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.

An edge partition into cliques is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$. Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.

The asymptotic notation

$$\frac{n^2}{6}+O(n)$$

means that there are constants $C>0$ and $n_0\ge1$, chosen independently of $G$ and $n$, such that every chordal $n$-vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.

Formalization targets

Erdős Problem 81

The root theorem is

$$\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \frac{n^2}{6}+Cn.$$

The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.

Leading-coefficient milestone

The supporting target records the weaker uniform statement

$$\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \left(\frac16+\varepsilon\right)n^2.$$

This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$.

Significance

The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$. It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.

Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.

Difficulty

Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$.

The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$.” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$.

Formalization scope

Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.

The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is candidate_only, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.

Selected references

• P. Erdős, E. T. Ordman, and Y. Zalcstein, Clique Partitions of Chordal Graphs, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
• P. E. Haxell and V. Rödl, Integer and Fractional Packings in Dense Graphs, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
• R. Yuster, Integer and fractional packing of families of graphs, 2003. https://arxiv.org/abs/math/0305350
• Erdős Problems, Problem 81. https://www.erdosproblems.com/81

Motivation

An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The obstacle number asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.

The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$, have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.

Setting

A finite simple graph $G$ has a $k$-obstacle drawing when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that

$$uv\in E(G) \quad\Longleftrightarrow\quad [p(u),p(v)]\text{ meets no obstacle}.$$

Graph vertices lie outside every obstacle. The ordinary obstacle number $\operatorname{obs}(G)$ is the least such $k$. The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.

The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.

Formalization targets

The two-part OPG record

The source records both

$$\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1$$

and

$$\exists k\in\mathbb N\ \forall\text{ finite planar }H, \ \operatorname{obs}(H)\le k.$$

The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.

Published first part

A milestone formalizes the stronger published statement

$$\exists\text{ finite planar }G, \qquad \operatorname{obs}(G)\le2 \quad\text{and}\quad \operatorname{obs}(G)\not\le1.$$

This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.

Universal bound

The open milestone asks for a single natural number $k$, chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.

Significance

The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.

Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.

Difficulty

A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.

Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$.

Formalization scope

All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.

The repository's fixed-placement polygonization argument and finite arrangement code are candidate_only. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.

Selected references

• L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, Graphs with Obstacle Number Greater than One, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
• J. Gimbel, P. Ossona de Mendez, and P. Valtr, Obstacle Numbers of Planar Graphs, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
• M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, Bounding and Computing Obstacle Numbers of Graphs, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
• Open Problem Garden / UnsolvedMath, OPG-37357. https://www.unsolvedmath.com/problems/OPG-37357

Motivation

An elliptic curve over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the rank. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.

Timeline.

• 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901).
• 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function.
• 1965: B. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, state the conjecture, found experimentally on the EDSAC computer.
• 1977: J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer: for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite.
• 1986: B. Gross and D. Zagier, Heegner points and derivatives of L-series: for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order.
• 1989–1990: V. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves: for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty).
• 1995–2001: A. Wiles (Ann. Math. 141), R. Taylor and A. Wiles (Ann. Math. 141), and C. Breuil, B. Conrad, F. Diamond and R. Taylor (J. Amer. Math. Soc. 14): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$.
• 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem.
• 2014: M. Bhargava, C. Skinner and W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture: the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open.

Setting

A Weierstrass equation over $\mathbb{Q}$ is

$$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$

with discriminant $\Delta$; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when $\Delta \ne 0$ (Mathlib's typeclass IsElliptic). Its rational points $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a $\mathbb{Z}$-module, $r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$ the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$.

The Hasse–Weil $L$-series is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is minimal at $p$ (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (good reduction). The local factor is

$$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$

and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there.

An $L$-function of $E$ is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, analyticOrderAt Λ 1, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$.

Formalization targets

Goal: the Birch and Swinnerton-Dyer conjecture (BSD.birch_swinnerton_dyer)

For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that

$$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$

This is Wiles' Conjecture (Birch and Swinnerton-Dyer): $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open.

Weaker target: the weak conjecture (BSD.weak_birch_swinnerton_dyer)

There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open.

Milestones: what Wiles lists as known

1. Mordell's theorem (BSD.mordell): $E(\mathbb{Q})$ is a finitely generated abelian group.
2. Convergence of the $L$-series (BSD.lSeriesSummable): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$."
3. Analytic continuation (BSD.exists_isLFunction): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.
4. Gross–Zagier–Kolyvagin (BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds."

A bridging lemma, BSD.isLFunction_unique, records that an $L$-function of $E$ is unique when it exists.

Significance

The result itself. The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions.

Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.

Difficulty

Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing.

The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.

Formalization scope

• $E$ is any WeierstrassCurve ℚ with IsElliptic ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.
• The rank is Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's finrank is $0$, a case milestone 1 excludes.
• The $L$-series is Mathlib's WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. BSD.IsLFunction constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique.
• The order of vanishing is analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$.

No trivializing formalization. The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative.

Out of scope. The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$.

Infrastructure needed and welcome contributions. Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's WeierstrassCurve.LSeries to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.

Selected references

• A. Wiles, The Birch and Swinnerton-Dyer Conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf
• B. J. Birch, H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79
• L. J. Mordell, On the rational solutions of the indeterminate equations of the third and fourth degrees, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192.
• J. Coates, A. Wiles, On the conjecture of Birch and Swinnerton-Dyer, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975
• B. H. Gross, D. B. Zagier, Heegner points and derivatives of L-series, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809
• V. A. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779
• A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• R. Taylor, A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• C. Breuil, B. Conrad, F. Diamond, R. Taylor, On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
• J. B. Tunnell, A classical Diophantine problem and modular forms of weight 3/2, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327
• M. Bhargava, C. Skinner, W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture, 2014. https://arxiv.org/abs/1407.1826
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6

Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Determining which equations force other equations separates the consequences of a single law from familiar properties that require additional assumptions. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The Equational Theories Project studies these implications systematically. Its December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $A$ with a total binary operation $\diamond:A\times A\to A$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

$$\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$

The condition E255 means

$$\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x.$$

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$, the left multiplication map is $L_y(x)=y\diamond x$. A fixer for $x$ is an element $y$ satisfying $y\diamond x=x$. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $A$ satisfying E677, the first supporting statement is

$$\forall y\in A,\quad L_y\text{ is bijective}.$$

The second supporting statement specifies any fixer:

$$\forall x,y\in A,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$

The third supporting statement is the backward recurrence

$$\forall x,y\in A,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$

These supporting statements come from ETP blueprint Lemma 13.1(i)–(iii); local direct proof files accompany their statements. The following universal fixer-existence assertion is retained as an explicit equivalent reformulation:

$$\forall x\in A,\quad\exists y\in A,\quad y\diamond x=x.$$

The mission goal is

$$\forall\text{ finite magmas }A,\quad \operatorname{E677}(A)\ \Longrightarrow\ \operatorname{E255}(A).$$

For finite E677 magmas, fixer existence is equivalent to E255: E255 supplies the fixer $(x\diamond x)\diamond x$, and Lemma 13.1(ii) converts any fixer into E255. Thus it is not presented as a strictly weaker milestone.

The active open milestone is an orbit-local producer statement. For a fixed $x$, if two elements in the forward orbit $x,L_x(x),L_x^2(x),\ldots$ have equal right products by $x$, they must be equal unless $x$ has a fixer. This isolates a genuine structural step without asserting a fixer for every element. None of the displayed statements restricts the cardinality to a tested range.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left multiplication property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left multiplication conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left multiplication map alone does not state that a fixer exists.

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

Selected references

• Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
• The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.2, chapter, accessed September 7, 2026.

What the constant is

Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:

$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$

It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.

What is being asked

For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, neither is known. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.

The goal theorem of this mission is transcendence,

$$\gamma \notin \overline{\mathbb{Q}},$$

with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.

What is actually known

Progress has come in three forms, and the milestones below formalize each.

Conditional bounds on a putative denominator. If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.

Disjunctive results. The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant

$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$

Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of $\gamma$ and $\delta$ is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.

Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.

Timeline

• 1734 — Euler introduces the constant and computes it to six decimals.
• 1790s–1800s — Mascheroni computes further digits; the constant acquires its second name.
• 1873 — Hermite proves $e$ transcendental; 1882 — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
• 1980 — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
• 1997 — Papanikolaou: the same denominator exceeds $10^{244663}$.
• 2009 — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
• 2012 — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
• 2010s — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.

Formalization notes

Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.

Egyptian fractions and the Erdős–Straus question

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

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

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

The main developments relevant here are:

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

The exact property

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

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

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

Formalization targets

The unresolved root goal is

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

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

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

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

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

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

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

What these results provide

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

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

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

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

or

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

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

The remaining difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

A unit fraction is the reciprocal $1/n$ of a positive integer. The number $1$ can be written as a sum of distinct unit fractions in infinitely many ways — $1 = \tfrac12+\tfrac13+\tfrac16$, $1 = \tfrac12+\tfrac14+\tfrac16+\tfrac1{12}$, and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?

Order the denominators increasingly and look at their consecutive differences. For $1 = \tfrac12+\tfrac13+\tfrac16$ the differences are $1$ and $3$. The question is whether a difference of at least $3$ must always occur, in every representation of $1$, no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.

Timeline. The weaker statement that some difference must be at least $2$ — equivalently, that $1$ is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number $H_n$ is not an integer for $n \ge 2$, using Bertrand's postulate. Kürschák (1918) introduced the $2$-adic argument that proves the general block statement: for $m \le n-2$, the difference $H_n - H_m$ is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference-$\ge 2$ bound. Nothing stronger appears to be known: the passage from $2$ to $3$ is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large $N$ there is a prime $p \in [N, 2N]$ with $(p+1)/2$ also prime.

Setting

Fix an integer $k \ge 2$ and integers

$$1 < n_1 < n_2 < \cdots < n_k$$

with

$$1 \;=\; \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k},$$

the sum taken in $\mathbb{Q}$. Call such a tuple a representation of length $k$. The denominators are strictly increasing, hence distinct, and all exceed $1$: the value $n_1 = 1$ is excluded because $1/1$ already exhausts the total. The gaps of the representation are the $k-1$ consecutive differences $n_{i+1} - n_i$ for $1 \le i \le k-1$, and its maximal gap is $\max_i (n_{i+1} - n_i)$.

Representations exist for every $k \ge 3$, and for $k = 1$ only the excluded $n_1 = 1$; no representation of length $2$ exists. Examples: $(2,3,6)$ with gaps $1, 3$; $(2,4,6,12)$ with gaps $2,2,6$; $(3,4,6,10,12,15)$ with gaps $1,2,4,2,3$.

Formalization targets

Goal — Erdős Problem 287

$$\text{every representation } 1 < n_1 < \cdots < n_k \ (k \ge 2) \text{ of } 1 \text{ satisfies } \max_{1 \le i < k} (n_{i+1} - n_i) \;\ge\; 3.$$

This is the open conjecture, stated with no bound on $k$ and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular $k$, or for denominators in some range, would be a different and strictly easier statement.

Milestone — the gap-two bound (Kürschák; Erdős [Er32])

$$\text{every representation satisfies } \max_{1 \le i < k}(n_{i+1} - n_i) \;\ge\; 2.$$

Equivalently: no block of two or more consecutive integers has reciprocals summing to $1$. This is closed mathematics and the natural first target.

Milestone — the classical block theorem (Kürschák)

$$\text{for } n \ge 1 \text{ and } k \ge 2, \qquad \sum_{i=0}^{k-1} \frac{1}{n+i} \notin \mathbb{Z}.$$

The gap-two bound is an immediate consequence, since a representation all of whose gaps equal $1$ is exactly a block of consecutive integers.

Milestone — sharpness

$$1 = \tfrac12+\tfrac13+\tfrac16 \text{ is a representation all of whose gaps are at most } 3.$$

So the constant $3$ in the goal is optimal and cannot be replaced by $4$.

Significance

The result itself. A positive answer would say that a representation of $1$ by unit fractions can never have all its denominators within distance $2$ of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes $p$ in $[N,2N]$ with $(p+1)/2$ prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.

Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that $H_n \notin \mathbb{Z}$ for $n \ge 2$, but not Kürschák's block version $H_n - H_m \notin \mathbb{Z}$, which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.

Difficulty

The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because $k$ is unbounded: representations of $1$ exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the $2$-adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal $2$-adic valuation, which leaves the total with negative valuation. Once gaps of size $2$ are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in $(2,4,6,12)$ — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap-$\le 2$ configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.

Formalization scope

A representation is encoded as a function $f : \mathbb{N} \to \mathbb{N}$ together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of $f$ below $k$ are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least $3$"; the subtraction is natural-number subtraction, which is harmless because $f$ is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.

The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit $f\,0 = 1$, $k = 1$; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly $3$ rather than at least $3$ would be false, as $(2,4,6,12)$ has a gap of $6$.

Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes $p$ with $(p+1)/2$ prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.

Selected references

• P. Erdős, Egy Kürschák-féle elemi számelméleti tétel általánosítása (A generalisation of an elementary number-theoretic theorem of Kürschák), Mat. és Phys. Lapok 39 (1932), 17–24.
• P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique, Geneva, 1980, p. 33. scan
• Various, Some of Paul's favorite problems, booklet for the conference "Paul Erdős and his mathematics", Budapest, July 1999, item 1.15.
• K. Conrad, The $p$-adic growth of harmonic sums, expository notes (Theorem 2 is Kürschák's block theorem, with the $2$-adic proof). pdf
• T. F. Bloom, Erdős Problem #287, erdosproblems.com/287.

Motivation

Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.

Timeline.

• 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
• 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
• 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
• 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
• 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
• 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
• 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
• 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
• 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
• 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.

Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.

Setting

Fix an integer $k$. A non-trivial $k$-term arithmetic progression is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is $k$-AP-free if it contains no such progression. Write

$$r_k(N)\;=\;\max\bigl\{\,|A| \;:\; A\subseteq\{1,\dots,N\},\ A\ \text{is}\ k\text{-AP-free}\,\bigr\}.$$

The mission takes its formal definition of $r_k$ verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length $l$ when every subset of it that is an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.

On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in how fast it goes to $0$.

Formalization targets

Goal

$$r_k(N)\;=\;o_k\!\left(\frac{N}{\log N}\right)\qquad\text{for every }k>1 .$$

This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of $r_k$.

The headline theorem in that file, erdos_142, states $r_k(N)=\Theta(f)$ with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.

A weaker open question

$$\frac{r_k(n)}{r_{k+1}(n)}\longrightarrow 0\qquad\text{for some }k\ge3 .$$

Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.

Significance

Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.

Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.

Difficulty

Every known upper bound for $r_k$ runs a density increment: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with polynomial dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.

Formalization scope

The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.

1. The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over $\mathbb N$; the file proves the two facts that make it a genuine maximum (le_r and r_le).

2. An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.

Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length-$0$ and length-$1$ progressions are trivial, so every set is free of them and $r_0(N)=r_1(N)=N$; monotonicity of $r_k$ in $k$ therefore holds only from $k\ge2$ onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over $\mathbb N$ with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is $0$ at $N=1$; this is invisible to atTop.

A trivializing formalization is ruled out by construction: one milestone asserts $r_3(N)=$ rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.

A full development needs: discrete Fourier analysis on $\mathbb Z/N\mathbb Z$, Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the $k=3$ case of a general-$k$ milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.

Selected references

• Erdős Problem #142. https://www.erdosproblems.com/142
• Erdős Problem #3. https://www.erdosproblems.com/3
• Erdős Problem #139 (Szemerédi's theorem in the $r_k$ formulation), linked from #142. https://www.erdosproblems.com/139
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of $r_k$. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean
• F. A. Behrend, On sets of integers which contain no three terms in arithmetical progression, Proc. Nat. Acad. Sci. USA 32 (1946), 331–332. https://doi.org/10.1073/pnas.32.12.331
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953), 104–109. https://doi.org/10.1112/jlms/s1-28.1.104
• R. A. Rankin, Sets of integers containing not more than a given number of terms in arithmetical progression, Proc. Roy. Soc. Edinburgh Sect. A 65 (1961), 332–344.
• E. Szemerédi, On sets of integers containing no $k$ elements in arithmetic progression, Acta Arith. 27 (1975), 199–245. https://doi.org/10.4064/aa-27-1-199-245
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001), 465–588. https://doi.org/10.1007/s00039-001-0332-9
• B. Green and T. Tao, New bounds for Szemerédi's theorem, III: A polylogarithmic bound for $r_4(N)$, Mathematika 63 (2017), 944–1040. https://arxiv.org/abs/1705.01703
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528. https://arxiv.org/abs/2007.03528
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, arXiv:2302.05537. https://arxiv.org/abs/2302.05537
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995. https://arxiv.org/abs/2402.17995

Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.