All missions

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:

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

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

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

or

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

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

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

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

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$,

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

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

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

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:

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

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

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

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

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

Setting

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

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

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

Target

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

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

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

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$,

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

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:

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:

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

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

Motivation: classify three-dimensional periodic symmetry

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

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

Setting: groups, transformations, and orientation

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

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

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

Target: one conjunction, with all three exact counts

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

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

Significance: exact cardinalities for the underlying groups

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

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

Difficulty: a catalog is not a completeness theorem

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

Formalization scope: preserve the benchmark model

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

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

Selected references

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

Motivation

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

Setting

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

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

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

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

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

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

Target

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.

Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.

That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.

In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.

In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from $5,000 in 1997 to$1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.

Motivation

Erdős Problem 624 (erdosproblems.com/624) is a problem of Erdős and Hajnal about how few elements of a set can be enough to "see" the whole set through a function on its subsets. For a finite set $X$ with $|X| = n$, let $H(n)$ be the least $m$ for which some map $f : \mathcal P(X) \to X$ has the following property: for every $Y \subseteq X$ with $|Y| \ge m$,

The problem asks to prove that $H(n) - \log_2 n \to \infty$.

The question belongs to extremal set theory. It asks whether the trivial counting bound $2^{|Y|} \ge n$ can be beaten by an unbounded additive amount.

Timeline.

• Erdős and Hajnal (1968) proved $\log_2 n \le H(n) < \log_2 n + (3+o(1))\log_2\log_2 n$ ([ErHa68], as reported on erdosproblems.com/624).
• Erdős remarked that even $H(2^k) \ge k+1$ was open. Alon gave a short pigeonhole proof of it. Alon also proved, for large $k$ and $|X| = 2^k$, that every $f$ has a $k$-set $Y$ with $|f[\mathcal P(Y)]| < (1-c)2^k$ for an absolute constant $c > 0$. Both are personal communications recorded on erdosproblems.com/624.
• The problem remains open.

Setting

• $\mathrm{Fin}\,n$ stands for an $n$-element set.
• ExistsEventuallySurjective $n\ m$ holds if some $f : \mathcal P(\mathrm{Fin}\,n) \to \mathrm{Fin}\,n$ satisfies $Y.\mathrm{powerset}.\mathrm{image}\ f = \mathrm{univ}$ whenever $|Y| \ge m$.
• $H(n)$ is the infimum of such $m$ for $n > 0$, and $H(0) = 0$.
• Both definitions are copied verbatim from Google DeepMind's Formal Conjectures file ErdosProblems/624.lean and published here as the definition Erdos624_defs.

Much of the supporting development works in a two-map (PAIR) reformulation:

• $|U| = |C| = n = 2^k$, with two arbitrary maps $g_0, g_1 : \mathcal P(U) \to C$.
• $L(A) = \{g_0(A), g_1(A)\}$, $J(Y) = \bigcup_{A \subseteq Y} L(A)$ and $D(Y) = n - |J(Y)|$.
• A colour $u \notin J(Y)$ is a common hole of $Y$.

More generally, the $r$-track version allows $r$ maps $g_1, \dots, g_r$.

Formalization targets

Goal (open)

stated as Erdos624.erdos_624 exactly as in Formal Conjectures.

Sufficient condition (open): bounded-track resilience

For every fixed $r$ there is $K$ such that for all $k \ge K$ and all $g_1, \dots, g_r : \mathcal P(\mathrm{Fin}\,2^k) \to \mathrm{Fin}\,2^k$, some $k$-set $Y$ and colour $u$ satisfy $g_i(A) \ne u$ for all $i$ and all $A \subseteq Y$.

The implication "bounded-track resilience $\Rightarrow$ Erdős 624" is proved in Lean (erdos_624_of_bounded_track_resilience). Whether the hypothesis is true is open.

Two-track case (open): PAIR

For all sufficiently large $k$, every pair $g_0, g_1 : \mathcal P(\mathrm{Fin}\,2^k) \to \mathrm{Fin}\,2^k$ has a $k$-set $Y$ with $D(Y) > 0$.

This is the $r = 2$ case of the condition above. On its own it does not imply Erdős 624, and it is false at $k = 3$ (pair_common_hole_false_k3).

Significance

A proof of the goal would settle a 1968 question of Erdős and Hajnal. It would show that the information-theoretic bound $|Y| \ge \log_2 n$ is never tight up to bounded error.

The present mission collects machine-checked partial and structural results obtained while attacking the PAIR case:

• a uniform, explicit-constant version of Alon's theorem ("robust Alon": a random $k$-set misses at least $n/32$ points on average), plus conditioned versions on stars of $k$-sets through a small core;
• monotonicity of $H$, and a track-amplification lemma reducing the goal to bounded-track resilience;
• obstructions for structured maps (monoid factorisations, one structured map);
• a rank-deficiency lemma for $\mathbb F_2$ labellings;
• packing lemmas for proper holes;
• the "top-layer-free resilience" theorem for covering pairs;
• minimal-envelope linear algebra over $\mathbb F_2$: extension of holes, $r \le k-1$ under coverage, critical-rank rigidity and circuit identification;
• arithmetic and lower-bound ingredients of a local counterexample construction.

Status, stated plainly: none of these results proves PAIR, the "Step 17" target of the underlying analysis, or Erdős 624. All of them are partial or structural. Some theorems are pure arithmetic consequences of an unproved packing statement (P), which enters only as a numeric hypothesis. In particular, the rank-rich exclusion ($k \ge 157$) is conditional on (P), and (P) is neither claimed nor formalized here.

Every linked theorem has an accepted, sorry-free Lean proof on this platform using only the standard axioms (propext, Classical.choice, Quot.sound).

Difficulty

Alon's pigeonhole argument gives a missed colour for a single map. For two or more maps the missed sets of different maps can be disjoint: pair_common_hole_false_k3 shows exactly this at $k = 3$, where each map misses half the colours on every 3-set yet no colour is missed by both. The underlying analysis also shows that separately convexified (fractional) relaxations of the fibre constraints admit fractional "covering pairs", so integrality or genuinely joint information across colours must enter any proof. The holes produced on small sets for different colours do not obviously combine, because the union of two holes can contain a new witness.

Formalization scope

• Conventions:
  • Lean 4 with Mathlib (rev 0df444a).
  • $H$ is defined on $\mathrm{Fin}\,n$ exactly as in Formal Conjectures.
  • Supporting theorems use Finset with arbitrary finite types $U, C$ and two maps $g_0, g_1$, or list maps $L : \mathcal P(U) \to \mathcal P(C)$.
  • Statements inline their own objects instead of introducing custom definitions where possible.
  • Natural-number subtraction is used only where it is harmless; each such statement notes it.
• No trivialisation: the goal is the Formal Conjectures statement, with no extra hypotheses.
• Welcome contributions:
  • proofs or disproofs of the two open targets;
  • new structural results on covering pairs;
  • independent re-proofs of the linked lemmas.

Credit

Mathematics derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; hand-checked and Lean formalization by Grok Bot.

Selected references

• [ErHa68] P. Erdős and A. Hajnal (1968) and [Er99] P. Erdős (1999), as cited, with the Erdős–Hajnal bounds and Alon's results, on the problem page https://www.erdosproblems.com/624
• Google DeepMind, Formal Conjectures, FormalConjectures/ErdosProblems/624.lean, https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/624.lean

Motivation

We investigate Gaussian quantum states in view of their exceptional role within the space of all continuous variables states. A general method for deriving extremality results is provided and applied to entanglement measures, secret key distillation and the classical capacity of Bosonic quantum channels. We prove that for every given covariance matrix the distillable secret key rate and the entanglement, if measured appropriately, are minimized by Gaussian states. This result leads to a clearer picture of the validity of frequently made Gaussian approximations. Moreover, it implies that Gaussian encodings are optimal for the transmission of classical information through Bosonic channels, if the capacity is additive.

This mission is the statement-level formalization of Extremality of Gaussian quantum states (arXiv:quant-ph/0509154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1, (2): general Gaussian extremality (original seed) (Lemma 1, (2): general Gaussian extremality (original seed), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered application (i): distillable-entanglement minimum: Operational extended LOCC conversion rate for full oscillator inputs and one arbitrary fixed multipartite normalized target (hard)
• Unnumbered sufficient covariance distillability criterion: Positive computed full-oscillator bipartite LOCC distillation rate (hard)
• Proposition 2: collective-attack distillable secret key: Computed collective-attack multipartite secret-bit rate on full oscillator densities (hard)
• Proposition 3: optimal Gaussian average encoding under additivity: Full-mode E_F convex roof, its global strong-superadditivity hypothesis, and constrained regularized capacity linked to the same Gaussian dilation (hard)
• Unnumbered single-mode coherent Gaussian ensemble: Restrictions on the fixed channel/dilation making inverse images of optimal joint Gaussian-roof components coherent input states (source-ambiguity)
• Introduction: distillable-randomness claim: Source-selected operational randomness resource, communication restrictions and unit (source-ambiguity)
• Conclusion: claimed translation to Fermionic systems: Source-selected CAR covariance, parity, local tensor and operational resource conventions (source-ambiguity)

Selected references

• Extremality of Gaussian quantum states, arXiv:quant-ph/0509154v1, https://arxiv.org/abs/quant-ph/0509154v1

Motivation

Additivity of the Holevo capacity is proved for product channels, under the condition that one of the channels is in a certain class of unital qubit channels, with the other completely arbitrary. This qubit class includes the depolarizing channel. As a byproduct this proves that the Holevo bound is the ultimate information capacity of such qubit channels (assuming no prior entanglement between sender and receiver). Additivity of minimal entropy and multiplicativity of p-norms are also proved under the same assumptions.

This mission is the statement-level formalization of Additivity for a class of unital qubit channels (arXiv:quant-ph/0103156v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unital qubit channels: norm multiplicativity and entropy and Holevo additivity (Theorem 1, equations (5)–(7), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Additivity for a class of unital qubit channels, arXiv:quant-ph/0103156v2, https://arxiv.org/abs/quant-ph/0103156v2

Motivation

We study the symmetric-side-channel-assisted private capacity of a quantum channel, for which we provide a single-letter formula. This capacity is additive, convex, and, for degradable channels, equal to the unassisted private capacity. While a channel's (unassisted) capacity for for private classical communication may be strictly larger than its quantum capacity, we will show that these capacities are equal for degradable channels, thus demonstrating the equivalence of privacy and quantum coherence in this context. We use these ideas to find new bounds on the key rate of quantum key distribution protocols with one-way classical post-processing. For the Bennett-Brassard-84 (BB84) protocol, our results demonstrate that collective attacks are strictly stronger than individual attacks.

This mission is the statement-level formalization of The private classical capacity with a symmetric side channel and its application to quantum cryptography (arXiv:0705.3838v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed paper result): single-letter ss-private capacity (Theorem 5 (seed paper result): single-letter ss-private capacity, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Equation (5): combined convex-hull BB84 bound: Meaning of conv and its admissible interpolation domain for the nonlinear independent-error channel family (source-ambiguity)
• Unnumbered main result: collective attacks outperform individual attacks on BB84: Matched individual/collective optimized protocol model and numerical comparison witness (source-ambiguity)
• Section IV.E: degradable-mixture collective attacks and their key-rate bound: Exact optimized key rate after the specified environmental measurement (source-ambiguity)

Selected references

• The private classical capacity with a symmetric side channel and its application to quantum cryptography, arXiv:0705.3838v1, https://arxiv.org/abs/0705.3838v1

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is one of the basic parameters of combinatorial optimization: computing it is NP-hard, and random graphs are the standard test bed for what typical instances look like. For the Erdős–Rényi–Gilbert graph $G_{n,p}$, in which every edge is present independently, the behaviour of $\alpha$ is known to first order in the dense regime (Grimmett–McDiarmid 1975) and in the sparse regime (Frieze 1990). Independence of the edges is what all these arguments use, and it is also the feature that real networks most obviously lack.

A. Gupte and Y. Zhu (arXiv:2207.04514, Mathematics of Operations Research, 2025) introduce a random graph in which the edges at a vertex are dependent through a Markov chain, and ask which classical properties survive. Their first main result is a lower bound on $\alpha$ of order $n/\log n$ that holds with high probability. This mission formalizes that result, read in the arXiv version v4 (24 May 2024).

Setting

Fix an initial probability $p\in(0,1]$ and a decay parameter $r\in(0,1)$, and write $\gamma:=1-r$. The recursive Markov random graph $G^r_{n,p}$ (Definition 1 of the paper) has vertices $v_1,\dots,v_n$ and is generated vertex by vertex. When $v_i$ arrives, its edges to the earlier vertices form a row of Bernoulli variables $X^i_1,\dots,X^i_{i-1}$, with $X^i_j=1$ when the edge $(v_j,v_i)$ is present. Rows of different vertices are independent. Within a row:

1. the first edge $(v_1,v_i)$ is present with probability $p$;
2. given the previous edge of the row, the edge $(v_j,v_i)$ is present with probability $p^i_{j-1}$ if $(v_{j-1},v_i)$ is absent, and with probability $r\,p^i_{j-1}$ if it is present, where $p^i_{j-1}=\mathbb P\{X^i_{j-1}=1\}$.

So each row is a non-homogeneous Markov chain whose transition matrix (display (2) of the paper) depends on the marginal of the previous edge. The marginals then obey the recursion $p^i_j=f_\gamma(p^i_{j-1})$ with $f_a(x)=x(1-ax)$, and a present edge lowers the chance of the next one by the factor $r$. At $r=1$ the model is $G_{n,p}$; the paper assumes $r<1$ throughout.

The average degree is $d(G)=2|E(G)|/n$. A property holds with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$, and $\xi_n$ concentrates to $c$ if $\mathbb P\{|\xi_n-c|\le\varepsilon\}\to1$ for every $\varepsilon>0$. The logarithm is natural.

Formalization targets

Goal: Theorem 2.1

For every $p\in(0,1]$, $r\in(0,1)$ and $\varepsilon>0$,

The constant $\gamma/(2+\varepsilon)$ is the paper's, and the statement is required for every $\varepsilon>0$ and every admissible $p$, $r$.

Milestones

In attack order:

• the recursion $x_{n+1}=f_a(x_n)$: Lemma 4.1 (elementary properties of $f_a$), Lemma 4.2 (the terms are of order $1/n$), Lemma 4.3 (the partial sums are $\frac1a\log n+O(1)$);
• the edge probabilities: Lemma 3.1 ($p^i_j=p^i_{j-1}(1-\gamma p^i_{j-1})$), Lemma 6.1 (two-sided bounds of order $1/(\gamma j)$), Lemma 6.2 (bounds on conditional probabilities along a row), Lemma 3.2 (one Markov chain represents every row);
• the decay chain: Lemmas 10.1–10.4 (second moment, a Chebyshev step, a Slutsky step, $\mathbb E S_n^2/(\mathbb E S_n)^2\to1$) and Corollary 4.6, a law of large numbers $S_n/\log n\to1/\beta$ for Markov chains of Bernoulli variables with the decay transitions;
• the graph: Theorem 2.2 ($d(G^r_{n,p})/\log n$ concentrates to $2/\gamma$), Lemma 5.1 ($\alpha(G)\ge\max\{n^2/(n+2m),(2n-m)/3\}$ for every graph), and display (11), which combines them.

Significance

The theorem shows that the dependence between consecutive edges does not destroy the $n/\log n$ scale of the stability number. Combined with the paper's upper bound $\alpha\le cn$ (Theorem 2.4) and its analysis of the greedy algorithm (Proposition 2.3), it places $G^r_{n,p}$ between the dense and the sparse regimes of $G_{n,p}$. Theorem 2.2, a milestone here, is of independent interest: the graph has average degree $(2/\gamma+o(1))\log n$, and Corollaries 2.5–2.7 of the paper derive from it bounds on the minimum degree and the chromatic number and the existence of large clique minors.

The formalization adds a checked account of a proof whose printed version has gaps. Several printed lemmas are false as stated: Lemmas 4.2 and 4.3 lose a scaling factor, Lemma 6.2 has a wrong upper bound, Lemmas 10.1 and 10.4 are stated in a setting where they fail and Lemma 10.1 has a wrong constant, Theorem 4.4 is false without a Markov hypothesis, and the stochastic-dominance step (5) in the printed proof of Theorem 2.2 is false. Each affected milestone is stated in a minimally corrected form. Theorem 2.1 and Theorem 2.2 themselves are true. None of these results has a machine-checked proof.

Difficulty

A first idea is to transfer $G_{n,p}$ arguments directly. For $G_{n,p}$ with $p\approx c\log n/n$ the bound comes from Turán's theorem plus concentration of the edge count, and the edge count is a sum of independent indicators. In $G^r_{n,p}$ the edges at a vertex are strongly dependent: the edge count of a row is the partial sum $S_{i-1}$ of a non-homogeneous Markov chain whose marginals decay like $1/(\gamma j)$, so its mean grows only like $\log i/\gamma$. Standard laws of large numbers do not apply, and concentration of a row sum around $\log i/\gamma$ needs a second-moment bound that uses the Markov structure; the marginal recursion alone does not suffice (a comonotone coupling with the same marginals has row sums that stay bounded). The heart of the mission is therefore Corollary 4.6, a law of large numbers for this chain, built from the recursion estimates of Lemmas 4.2–4.3 and the second-moment bound of Lemma 10.1, and its transfer to the average degree through the independence of the rows.

Formalization scope

The vertex set is Fin n, the paper's $v_k$ being k − 1, and the edge $(v_j,v_i)$ is G.Adj (j−1) (i−1). The law of $G^r_{n,p}$ is an explicit finite weight rmrgWeight n p r G on SimpleGraph (Fin n). It is a product over rows, each row's weight being the Markov chain above with the transition out of edge $j$ using the $j$-th iterate of $f_\gamma$ from $p$. Probabilities are rmrgProb n p r E, the sum of the weights of the graphs in $E$. Definition 1's phrase "independent of all other edges" cannot hold for the next edge of the same row; it is read through the paper's generation process (rows independent, each row a Markov chain with transition matrix (2)). Lemma 3.1 is the milestone certifying that the marginals of this weight obey the recursion. A sanity file checks that the weights sum to $1$ for $n=2,3$ and that the first two edge marginals are $p$ and $p(1-\gamma p)$.

The decay chain is IsDecayChain P Y β on a probability space: $\{0,1\}$-valued measurable variables, the Markov property, and the two transition rules, with conditional probabilities written multiplicatively. Expectations are Bochner integrals, and "w.h.p." and concentration are limits of probabilities of the events $\{|\cdot-c|\le\varepsilon\}$, as defined on p. 4 of the paper. Variances in Lemma 10.2 come with square integrability for all large $n$, so the hypothesis $\sigma_n^2=o(\mu_n^2)$ is not met by the junk value $0$.

A trivializing formalization is ruled out: the weight is exactly the law of Definition 1, not one favouring sparse graphs, and no hypothesis of the goal pins the graph or the probability.

The corrections, each with a counterexample satisfying the paper's hypotheses, are declared on the items:

• Lemma 4.2 and Lemma 4.3 use $\ell_n(ax_1)$ and $f_1(ax_1)$, and the bound $x_n\le1/(4a)$ is non-strict;
• Lemma 6.2's first upper bound is $1-r\,p^i_{j-1}$;
• Lemmas 10.1 and 10.4 are stated for the decay chain of Corollary 4.6 (Lemma 10.4 for every $\beta\in[0,1]$, which keeps §10's range $(0,1]$), and Lemma 10.1's constant is $1+2/\gamma$.

Theorem 4.4 is false as stated and is not an item; Corollary 4.6, which the proof of Theorem 2.2 cites, replaces it. Displays (5)–(10), Proposition 2.3, Theorem 2.4 and Corollaries 2.5–2.7, 4.5, 4.7 and 5.2 are out of scope.

A complete development needs:

• a law of large numbers for non-homogeneous Bernoulli Markov chains;
• the finite-law calculus for rmrgProb: marginals, independence of rows, the row-to-chain identification;
• Caro–Wei/Turán-type lower bounds on SimpleGraph.indepNum, which Mathlib does not yet have.

The last two are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of Theorem 2.2 that avoid the printed stochastic-dominance step.

Selected references

• A. Gupte, Y. Zhu, Large independent sets in recursive Markov random graphs, arXiv:2207.04514v4, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2207.04514
• Y. Caro, P. Hansen, D. Sopena (CHS03 in the paper), cited for Lemma 5.1, Theorems 10 and 11; see the paper's bibliography.
• G. R. Grimmett, C. J. H. McDiarmid, On colouring random graphs, Mathematical Proceedings of the Cambridge Philosophical Society 77, 1975. https://doi.org/10.1017/S0305004100051124
• A. M. Frieze, On the independence number of random graphs, Discrete Mathematics 81, 1990. https://doi.org/10.1016/0012-365X(90)90149-C
• O. Frank, D. Strauss, Markov graphs, Journal of the American Statistical Association 81, 1986. https://doi.org/10.1080/01621459.1986.10478342

Motivation

A single machine receives jobs over time. Each job $j$ arrives at its release time $r_j$ with a length $v_j$ and a cost function $g_j$, and all three become known only at arrival. The machine may interrupt a job and resume it later (preemption). The objective is the total delay cost $\sum_j g_j(C_j)$, where $C_j$ is the completion time of job $j$. Weighted flow time ($g_j(t)=w_j(t-r_j)$), weighted completion time and tardiness are special cases. With arbitrary nondecreasing $g_j$ the problem is the generalized integral completion time problem, GICS.

Even offline, with general nondecreasing costs and arbitrary release times, this problem is strongly NP-hard. The best known approximation is $O(\log\log nP)$ (Bansal and Pruhs, 2014). Online, no algorithm has a bounded competitive ratio on a unit-speed machine even for weighted flow time (Bansal and Chan, 2009). The standard remedy is speed augmentation: the online machine is $s$ times faster than the offline optimum it is compared with.

Prior speed-augmented results covered special cost structures. Im, Moseley and Pruhs (SICOMP 2014) treated $g_j=w_jg$ with one function $g$ shared by all jobs. Angelopoulos, Lucarelli and Thang (Algorithmica 2019) treated convex or concave $g$, identical job densities, and FIFO or HDF policies. Etesami (Operations Research, 2022; arXiv:1906.02644) gave the first speed-augmented competitive algorithm for job-dependent nondecreasing $g_j$ on a single machine, subject to a structural condition on the class of cost functions. This mission formalizes that result.

Setting

Jobs are $j=1,\dots,n$ with $0\le r_1\le\cdots\le r_n$ and $v_j>0$. On $[r_j,\infty)$ each $g_j$ is nonnegative, nondecreasing and differentiable, with $g_j(r_j)=0$ (§II, p. 5). A fractional schedule with machine capacity $c$ assigns a processing rate $x_j(t)\ge 0$ to every job and time. Rates vanish before $r_j$, satisfy $\sum_jx_j(t)\le c$, and process every job fully: $\int x_j\ge v_j$. After the integration by parts on p. 6 and the rescaling $g_j\leftarrow g_j/v_j$, the fractional cost is the linear objective

The benchmark $\mathrm{OPT}_c$ is the infimum of this cost over all fractional schedules: the value of LP (1) for $c=1$, and of the slower LP (21) for $c=1/(1+\epsilon)$. Its dual (2) has one variable $\alpha_j\ge 0$ per job and a density $\beta_t\ge 0$ on the time axis, with constraints $\alpha_j/v_j\le\beta_t+g_j(t)$ for $t\ge r_j$.

For a time $s$, GFCS(s) is the offline problem in which a set $A$ of jobs, with lengths $\rho_j$, all start at $s$. Its optimal value is $\mathrm{RNF}$ (Definition 3). An optimal integral schedule processes one job at a time.

Algorithm 2 re-solves at every arrival. When job $k$ arrives, it takes the jobs still alive, with their residual lengths, together with job $k$. It solves GFCS($r_k$) for them as if no further job would come, and follows an optimal integral schedule of that instance until the next arrival.

A class $H$ of cost functions is monotone substitute (Definition 5) if adding a job to an identical-release instance can only postpone the optimal processing of the existing jobs. The curvature of the class enters through

Formalization targets

Goal: Theorem 3 (p. 20)

for every run of Algorithm 2 on an instance whose cost functions lie in a monotone substitute class. This is the statement that Algorithm 2 is $2K$-speed $2$-competitive. The goal takes any $K\ge1$ with $(t-r_\ell)g''_\ell(t)\le(K-1)g'_\ell(t)$, not a closed formula for $K$.

Milestones, in the order the proof uses them

1. Weak duality for the slower LP (21), p. 21.
2. Strong duality with attainment for GFCS(s), and the existence of a maximal optimal dual (largest $\int\beta$), p. 12 and p. 17.
3. Lemma 6: the cost increment $\Delta_n(\mathrm{Alg})=\mathrm{RNF}'(r_n)-\mathrm{RNF}(r_n)$ is at most the new dual variable $\alpha'_n$.
4. Lemma 4: the new optimal $\beta'$ dominates the old $\beta$ on $[r_n,\infty)$.
5. Lemma 5: the duals generated by Algorithm 2 are feasible for (2).
6. (20): optimal $\beta_t$ is at most $\hat\beta_t$, the total increase of the cost functions over the processing remaining after $t$.
7. Replacing the β-tails by $\hat\beta$ keeps the generated dual feasible.
8. (24): $\int_{r_n}^\infty\hat\beta_t\,dt=\sum_\ell\int_{I_\ell}(t-r_n)g'_\ell(t)\,dt$.
9. The (26) bound: $\int_{r_n}^\infty(\hat\beta'_t-\hat\beta_t)\,dt\le K\,\Delta_n(\mathrm{Alg})$.
10. The trade-off: $\mathrm{Cost(Alg)}\le\frac{1+\epsilon}{1+\epsilon-K}\,\mathrm{OPT}_{1/(1+\epsilon)}$ whenever $1+\epsilon>K$; the goal is the case $1+\epsilon=2K$.

Significance

The result covers job-dependent nondecreasing cost functions. Previous speed-augmented guarantees needed a single shared function or a fixed convexity type. It applies to any monotone substitute class: dominating families, classes for which HDF or HRDF is offline-optimal, and classes with an insertion-type optimal offline policy (p. 20). Combined with the black-box reduction of Lemma 1, it gives a speed-augmented guarantee for the integral objective $\sum_jg_j(C_j)$. For concave costs, $K=1$ and the bound becomes $(1+\epsilon)$-speed $\frac{1+\epsilon}{\epsilon}$-competitive (Example 3).

The result is proved in the paper, and no machine-checked proof of it or of any of its lemmas is known. The paper argues in a time-discretized network-flow model whose quantization error it describes only as "negligible" (Remark 2). A formal proof must therefore carry out the continuous version: strong duality for a semi-infinite assignment LP, the monotonicity of the optimal dual, and the bound (20) without the value function's differentiability.

Difficulty

Every LP in the argument has one variable per job and per time instant, so finite-dimensional LP duality does not apply directly. Dual attainment, and the existence of a dual with maximal $\int\beta$, must be proved for this time-indexed LP. The paper's Lemma 4 argument splits the time axis into the set where the new dual exceeds the old one and its complement; in continuous time these are measurable sets defined only almost everywhere. The bound (20) is a one-sided derivative of the value function, and the paper uses it without proving differentiability. The final step is a layer-cake comparison: postponed processing intervals and a nonincreasing integrand give a smaller integral. It needs the right notion of postponement. Monotone substitution is used only there; the rest of the chain holds for every nondecreasing cost.

A first idea is to treat Algorithm 2 as a fixed policy such as HDF and analyze it with potential functions. That fails here, because the algorithm is defined only through optimal offline solutions, and their structure depends on the class of cost functions.

Formalization scope

All declarations live in the namespace GenCostSched.GFCS and import one definitions file, GenCostSched.GFCS.Model.

Representation. Jobs are Fin n and times are real. The cost functions are the scaled $g_j/v_j$ of p. 6, supplied as data together with their first and second derivatives, which are tied to them by within-derivatives on $[r_j,\infty)$.

Conventions committed to:

• Schedules are measurable rate functions; integral schedules have rates in $\{0,1\}$, process each job exactly its length, and finish in finite time.
• Costs, processed amounts, $\mathrm{OPT}_c$ and $\mathrm{RNF}$ are valued in $[0,\infty]$.
• Dual variables are per unit length ($a_j=\alpha_j/v_j$). $\beta$ is an integrable density, and dual feasibility holds for almost every $t$.
• A machine $2K$ times faster is encoded as the online machine at capacity $1$ against the LP benchmark at capacity $1/(2K)$, the normalization of (21).

Readings:

• Monotone substitute is read as follows: for every identical-release instance from $H$ and every optimal integral schedule, adding a job leaves an optimal integral schedule that has processed at most as much of each old job by every time.
• Runs of Algorithm 2 re-solve with an optimal integral schedule (optimal among all fractional schedules) that postpones the continuing one.
• $K$ is any real $\ge1$ with $(t-r_\ell)g''_\ell\le(K-1)g'_\ell$.
• Lemma 4 is posed as printed, for every pair of optimal duals of the continuous LPs of Definition 3. The proof's choice of the maximal $\beta'$ matters only in its time-discretized model; with continuous cost functions the continuous dual optimum is unique up to null sets.