Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Brouwer's fixed point theorem says that a continuous map of a closed simplex into itself has a fixed point. Many existence questions in game theory and mathematical economics produce instead a point-to-set mapping: to each point it assigns a whole set of admissible responses, for instance the set of best replies of a player to the others' strategies. Such a set need not be a single point, and no continuous single-valued selection need exist. Kakutani's 1941 note, A generalization of Brouwer's fixed point theorem, gives the fixed point theorem for this setting, and shows on the same three pages that it implies two results of J. von Neumann: an intersection theorem for two closed subsets of a product of convex sets, and the minimax theorem.
Timeline, as the paper records it:
Let with its Euclidean norm, and let . Kakutani writes for the family of all closed convex subsets of ; as printed, it contains the empty set. A point-to-set mapping of into assigns to each a closed convex set .
is upper semi-continuous (in the paper's sense) when
This is a sequential closed-graph condition. The paper remarks that for a closed it is equivalent to the graph being closed in .
An -dimensional closed simplex is the convex hull of affinely independent points of . A fixed point of is a point with .
Let be nonempty, bounded, closed and convex, and let be upper semi-continuous on with every value , , a nonempty closed convex subset of . Then
Milestones 8 and 9 stand off the goal's proof path: the paper proves Theorem 2 from the Corollary, using milestone 8 to check upper semi-continuity.
The Corollary is the form in which Kakutani's theorem is used: existence of equilibrium points in -person games (Nash), of competitive equilibria (Arrow–Debreu), and of solutions of generalized games and variational inequalities all reduce to a fixed point of a point-to-set mapping with nonempty closed convex values on a compact convex set. Theorem 2 in turn gives the minimax theorem (the paper's Theorem 3) in a few lines.
The results are classical and their proofs are known; what is missing is a machine-checked version. Mathlib does not contain Kakutani's theorem, and on Prove2Me the theorem is not posed. Brouwer's theorem is proved on the platform (AGT.brouwer_fixed_point) and enters as a reference milestone. Theorem 3 is already proved on the platform as a special case of Sion's minimax theorem (FamousTheorems.sion_minimax_theorem, Mathlib's Sion.minimax) and is therefore not posed here. A related open platform statement, Debreu's 1952 fixed point lemma for a contractible polyhedron with contractible values and a closed graph (SocialEquilibrium.Existence.fixed_point_of_contractible_polyhedron), generalizes Theorem 1 on polyhedra but not the Corollary, since a bounded closed convex set need not be a polyhedron. Once proved, the goal is the standard entry point for formalized equilibrium existence results.
Brouwer's theorem needs a continuous single-valued map, and a point-to-set mapping with closed convex values need not admit a continuous selection: the mapping on equal to for , at and for is upper semi-continuous and has none. So the obvious route, select and apply Brouwer, fails; any proof must pass through approximations and a limit in which the graph condition and the convexity of the limiting value both enter. The approximation step needs a family of triangulations of the simplex with mesh tending to zero, which Mathlib does not provide. The transfer from a simplex to a general convex set needs a continuous retraction, which uses convexity and closedness of in Euclidean space.
EuclideanSpace ℝ (Fin m), included. A point-to-set mapping is a total function Φ : E → Set E; only its values on are constrained.IsClosedConvexSubset S A is the paper's (, closed, convex) and admits as printed. Nonemptiness of the values (and of , and of in Theorem 2) is a separate, labelled hypothesis: with , or , the printed hypotheses hold and there is no fixed point, while the paper's proof picks "an arbitrary point from ".IsUpperSemicontinuous S Φ is the paper's sequential condition, with sequences in and limit . It is not Berge's open-neighbourhood upper hemicontinuity.ContinuousOn ψ S', MapsTo ψ S' S and ψ x = x on ; "clearly an upper semi-continuous point-to-set mapping of into " is stated as three conclusions; "closed subset of " is closedness in (the same for closed ); is ; " in " is the product .The alternating direction method of multipliers (ADMM) solves problems of the form subject to by alternating a minimization in , a minimization in and a dual ascent step. Its practical appeal, as surveyed by Boyd, Parikh, Chu, Peleato and Eckstein in Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Foundations and Trends in Machine Learning, 2011, doi:10.1561/2200000016), rests on the fact that each of these minimizations is often trivial to carry out: a projection, a linear solve, or a componentwise formula. Chapter 4 of the book, "General Patterns", catalogues the cases that recur in every later application (lasso, basis pursuit, sparse inverse covariance selection, consensus and sharing problems). This mission formalizes the statements of that chapter, culminating in the identification of the update for an penalty with soft thresholding.
Vectors live in with the Euclidean norm . An extended-real-valued function is given by its effective domain and its finite values there. Fix a penalty parameter , a matrix and a vector . The -update of ADMM (p. 25) is
where "argmin" denotes a minimizer over . When the right-hand side, as a function of , is the proximity operator (§4.1).
The chapter evaluates in four situations:
The soft thresholding operator (§4.4.3, p. 32) is, for ,
applied componentwise to vectors.
For , and , a vector minimizes over if and only if
The statement gives both that the soft-thresholded vector is a minimizer and that it is the only one.
The results of this chapter are what make ADMM an implementable algorithm rather than a conceptual one. Soft thresholding is the -update of the lasso (§6.4), of distributed -regularized regression (§8.2) and of sparse inverse covariance selection (§6.5); projections are the updates of every constrained problem in Chapter 5; the linear-system form (4.1) and the KKT system are the updates of least squares and quadratic programming. Every later chapter of the book cites these identities without proof, so a formal library of them is the substrate on which formal statements about specific ADMM instances can be built.
None of these statements is open as a mathematical question: all are classical facts of convex analysis. The book states them without proof (the goal is justified by a reference to subdifferential calculus in Rockafellar's Convex Analysis). This mission poses their formal statements as Lean proof goals. The matrix inversion lemma already has a machine-checked proof on the platform (the Woodbury identity) and is reused. A related but distinct statement, that singular value shrinkage is the proximity operator of the nuclear norm (Cai, Candès and Shen, 2010), is posed separately on the platform and is not this mission's target.
The goal objective is not differentiable, so setting a gradient to zero does not apply; the minimizer sits exactly on the kink of whenever . A proof has to handle the three regimes of and must establish global optimality, not only stationarity, together with uniqueness. Passing from the vector problem to the scalar ones requires the separability statement, which is a statement about minimizers of sums over a product domain, not about any particular function. For the quadratic milestones, the difficulty is linear-algebraic: showing that invertibility of forces positive definiteness, and, for the equality-constrained case, that a minimizer exists and depends affinely on even when is rank deficient and the KKT matrix is singular.
Vectors are EuclideanSpace ℝ (Fin n), so ‖·‖ is ; matrices are Matrix (Fin p) (Fin n) ℝ acting through Matrix.toEuclideanLin. The conventions committed to are:
IsXUpdate, IsProx and IsProjection say " is a minimizer"; no choice function is used. Where the book says "the solution", the theorems state an equivalence " is a minimizer equals the formula", which gives existence and uniqueness at once.lam, since λ is a Lean keyword); for the soft thresholding identities (implicit in the book, where , and false for ); in (4.2), as on the page; symmetric positive semidefinite (Matrix.PosSemidef); invertibility of in (4.1); closed, convex and nonempty for the projection; nonemptiness of for the existence part of §4.2.5; of arbitrary rank.The trivializing formalization to avoid is stating the goal as the subgradient condition , or as agreement of the three formulas for : the goal is global minimality and uniqueness of the soft-thresholded vector for the objective. Not formalized: the flop counts and caching remarks of §§4.2.1–4.2.4 and the iterative-solver discussion of §4.3, which make no mathematical claim.
Contributions welcome: proofs of any milestone; the general block-separability statement of §4.4.1; a lemma connecting IsProx with Mathlib's orthogonal projection onto complete convex sets.
Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping , so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).
The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?
The abstract monotone model consists of a state space , a control space , nonempty constraint sets , a terminal function , and a mapping defined for , and , which is monotone: implies .
A selector is a function with ; a policy is a sequence of selectors, and it is stationary if all are equal. The operators are
the cost of a policy is , is the cost of the stationary policy , and the optimal cost is . A policy is optimal if .
Assumption I (uniform increase) is for all , ; under it the sequence defining is nondecreasing, so the limit exists in . Assumption I.1 says commutes with limits of nondecreasing sequences above , and I.2 says that for some , for all and . Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below , and a lower shift bound).
The DP algorithm (value iteration) generates ; for and the level sets
collect the controls that keep the stage- cost below .
Let I, I.1 and I.2 hold, let be a Hausdorff space, and let be compact for all , and . Then (a) some policy satisfies
(b) for every such policy, has an accumulation point whenever ; and (c) any that picks such an accumulation point at those states, and any admissible control where , defines an optimal stationary policy:
In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff ), Proposition 5.10 (under the compactness hypothesis, and a stationary optimal policy exists), Proposition 5.6 (-optimal policies from approximate attainment, with explicit constants and ), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and -optimal policies under D, D.2 with finite and ), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).
Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.
Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.
The obvious route to (c) is to pass to the limit in . That fails twice. First, need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, is not assumed continuous in at all: the only regularity in is compactness of the level sets , and the only regularity in is I.1 along monotone sequences. States with need separate treatment, because there the level sets give no control on .
For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of and essentially, and both hypotheses are needed.
Functions are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them is the limit (limUnder) of the policy compositions, which exists under I or D; is the iterate T^[k]; the composition applies first; the model requires nonempty and ; "I.2 holds" is the existence of a scalar , and results that name the scalar take it as a parameter. An accumulation point of a sequence in is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that is admissible. is computed pointwise in and equals where does.
The book computes in with . Mathlib's EReal gives , so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable (expect, positive and negative parts summed in , when the positive part diverges) and the sum inside the minimax supremum (badd, when either summand is ), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose and are these mappings; such models exist because the mappings are monotone.
A formalization in which or is introduced as an arbitrary fixed point of , or in which (c) assumes that is a limit of , would make the goal trivial or different; both are ruled out by the definitions above.
Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.
A stochastic process is reversible when a film of it run backwards is statistically indistinguishable from the film run forwards. For Markov processes in equilibrium this distributional symmetry has an algebraic counterpart, the detailed balance conditions, and that counterpart is what makes large classes of queueing networks, migration processes, loss networks, clustering processes and population-genetics models solvable in closed form. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) builds the whole theory of product-form equilibria on this link, and Chapter 1 sets it up.
The criterion that bears Kolmogorov's name goes back to A. Kolmogorov, "Zur Theorie der Markoffschen Ketten" (Math. Annalen 112, 1936), who showed that reversibility of a chain can be read off its transition probabilities around closed cycles. Kelly's Chapter 1 (§§1.1–1.7) states the criterion for chains (Theorem 1.7) and processes (Theorem 1.8), together with the detailed-balance characterization (Theorems 1.2, 1.3), the cut and tree lemmas (1.4, 1.5), the monotonicity of relative entropy (Theorem 1.6), truncation and rate alteration (Lemma 1.9, Corollary 1.10), and the description of the time-reversed process (Theorems 1.12–1.14). This mission is the first in a series covering the book.
Let be a finite state space. A continuous-time Markov process , , is specified by transition rates , , with Kelly's convention . Its generator is the matrix with off the diagonal and , and its transition matrices are . The rates are irreducible if every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers summing to one that satisfy the equilibrium equations
The stationary process with rates and equilibrium distribution has finite-dimensional distributions
It is reversible (Kelly, p. 5) if has the same distribution as for all . The rates satisfy detailed balance with if for all , and Kolmogorov's cycle condition if
for every finite sequence of states . The discrete-time analogue replaces rates by a stochastic matrix and by the matrix power , .
For a stationary, irreducible Markov process on a finite state space,
The left side is a statement about the joint laws of the process at all finite sets of times; the right side involves the rates alone, not even the equilibrium distribution.
Theorem 1.8 is the working test for reversibility throughout the book and the queueing literature: a model's reversibility, and with it a product-form equilibrium obtained by solving detailed balance, can be decided by checking a finite list of cycles in its transition diagram. Theorem 1.3 converts the distributional property into equations that later chapters solve explicitly; Theorems 1.12 and 1.13 underlie the treatment of quasi-reversible queues and networks in Chapter 3; Lemma 1.9 and Corollary 1.10 produce the equilibria of loss systems and queues with shared buffers.
The algebraic content of several of these results is already proved on the platform at the level of rates: detailed balance implies the equilibrium equations, the reversed rates preserve , truncation preserves detailed balance, and Kolmogorov's criterion is equivalent to detailed balance for two-way communicating rates. What is not formalized anywhere is the process-level statement: that these conditions are equivalent to the time-reversal symmetry of the finite-dimensional distributions built from . This mission supplies that layer, which connects the rate identities to the probabilistic notion they are meant to capture.
The rate-level identities are short; the difficulty is the passage between them and the process. Reversibility constrains the joint law at every finite set of times, and that law is built from the matrix exponential , whose entries are not explicit functions of the rates. Relating the two requires the analytic facts about for a generator (stationarity of , the semigroup property, behaviour as , strict positivity of the entries for under irreducibility) that Mathlib does not yet provide for Markov generators, together with bookkeeping for tuples of times given in arbitrary order, with ties. For Theorem 1.8 a positive, normalized equilibrium has to be produced from the cycle condition alone, on rates that may vanish in one direction only: two-way communication is not a hypothesis, so the platform's proved rate-level criterion does not apply directly. A first attempt that defines reversibility as detailed balance avoids all of this and proves nothing new; it is excluded below.
The state space is a Fintype with decidable equality; Kelly allows a countable state space, and this restriction is stated in every item. Rates are q : S → S → ℝ with 0 ≤ q j k for j ≠ k and q j j = 0 as hypotheses. The transition matrices are NormedSpace.exp (t • generator q). Time sets are ℝ (processes) and ℤ (chains). Finite-dimensional distributions are defined for arbitrary finite tuples of time points by sorting them with Tuple.sort. Equilibrium means positive, summing to one, and satisfying (1.3) (resp. ), and every theorem takes the equilibrium distribution of the stationary process as a hypothesis. Existing platform definitions are reused: FullBalance, DetailedBalance and reversedRates from KellyStochasticNetworks_Balance, the stochastic-matrix vocabulary of mm_basic, and truncatedRates from KellyStochasticNetworks_LossNetwork.
Reversibility is not defined as detailed balance or as equality of with its reversed rates: under such a definition Theorems 1.2 and 1.3 would be tautologies and Theorem 1.8 would be the already proved rate-level criterion. It is the distributional definition of p. 5. Kolmogorov's condition ranges over all sequences of all lengths, repetitions allowed, and two-way communication is not assumed.
A complete development needs the matrix exponential of a generator (positivity, the semigroup property, the derivative at , and ), which is reusable for any finite-state continuous-time Markov chain, and a lemma on reversing sorted tuples. Lemma 1.1 (a general stationary process) and Lemma 1.11 (a non-stationary reversal) are not included. Proofs of any milestone, and generalizations to countable state spaces, are welcome.
Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.
Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.
The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).
A project has activities with ; activity is the project beginning and the project completion. Activity has a duration , with . The project network has arc set ; an arc with integer weight imposes the temporal constraint on the start times. A schedule is a real vector with and ; it is time-feasible if it meets every temporal constraint.
Cumulative resources carry integer demands : depletes units at the start , replenishes units at the completion , and is the initial stock. The inventory at time is
With safety stock and storage capacity (integers, by (2.12.1)), is feasible if it is time-feasible and for every and every . The decision problem of asks whether a feasible schedule exists.
For renewable resources with capacities and requirements , a set is forbidden if for some . A delaying alternative for is a set such that is not forbidden; it is minimal if no proper subset of is one.
In there are no resources, schedules must also satisfy , and the objective here is with weights .
NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.
Assuming PARTITION is NP-complete,
are both NP-complete.
The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along (on the platform as CookPvsNP.npComplete_of_polyReducible).
The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.
Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.
The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.
First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.
Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.
The Lean development fixes the following conventions.
Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.
A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of , and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.
Many questions about polynomial equations — which equations can be solved by radicals, which geometric constructions are possible with ruler and compass, how the roots of a polynomial are related — become questions about the symmetries of a field extension. The fundamental theorem of Galois theory, going back to Évariste Galois, is the dictionary that makes this possible: for a finite Galois extension it matches intermediate fields with subgroups of a finite group, so that questions about fields become questions in finite group theory. The same dictionary underlies Kummer theory and class field theory, and it is the step that turns the unsolvability of the general quintic (Abel–Ruffini) into a statement about solvable groups.
This mission follows the Wikipedia article Fundamental theorem of Galois theory (revision 1345286594): its main statement, its list of properties of the correspondence, three of its worked examples, and its section on the infinite case.
A field extension is a field with a field inside it; it is finite when is finite-dimensional as an -vector space, of dimension . An intermediate field is a field with . The automorphism group is the group of field automorphisms of with for every .
The two maps of the correspondence are:
The extension is Galois when it is normal and separable; for a finite extension this is equivalent to . When is Galois, is written .
For an infinite algebraic Galois extension, carries the Krull topology: the coarsest topology for which each restriction map , with a finite Galois subextension and discrete, is continuous.
For a finite extension ,
The result. The correspondence turns the lattice of intermediate fields of a finite Galois extension into the (reversed) lattice of subgroups of a finite group, with degrees matching indices and normal subextensions matching normal subgroups. This is the tool used to classify subfields, to compute Galois groups of explicit polynomials, and to prove that solvability by radicals corresponds to solvability of the Galois group.
Formalizing it. The theorems are classical, and Mathlib contains formal proofs of the general finite and infinite correspondences (for example IsGalois.intermediateFieldEquivSubgroup and the InfiniteGalois namespace). This mission's contribution is a statement set indexed by the source: the converse direction ("only if Galois") as the goal, the non-Galois behaviour, each listed property, and the concrete examples of the article. The explicit examples require genuine computation: degrees of towers, minimal polynomials, and counting subgroups and subfields.
The general statements reduce to Artin's theorem and a degree count, but the non-Galois milestone asks for four separate claims about injectivity and surjectivity, each needing the correct direction of Artin's theorem. The examples cannot be settled by a general principle: showing that has exactly five intermediate fields, or that the splitting field of has degree , requires irreducibility arguments and an explicit transfer through the correspondence. Showing that has no non-trivial automorphism requires knowing that the other two roots of are not real.
All statements use Mathlib's IntermediateField F E, IntermediateField.fixedField, IntermediateField.fixingSubgroup, the automorphism group E ≃ₐ[F] E, and IsGalois (normal and separable). Finite means FiniteDimensional F E. Subgroups in the finite statements range over all subgroups; in the infinite case the Krull topology is Mathlib's standard topology on E ≃ₐ[F] E. Degrees are Module.finrank, orders are Nat.card, and the index is Subgroup.index. The concrete fields of the examples are taken inside (for and , with the real cube root) or as the abstract splitting field (for ). The quotient milestone takes the normality of and of as instance hypotheses; they are equivalent by milestone 5, so neither is vacuous.
The article's Example 3 (the anharmonic group acting on ) and the "Applications" section are out of scope for this first mission. No new definitions are needed; contributions of proofs for any milestone are welcome.
Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.
This mission states those results for the local flow of a vector field on an open subset of , as in the book.
Let be open and of class . An integral curve of is a differentiable on an open interval with . For each there is a unique maximal one through at time , defined on the open interval . Its value at time is , the flow. The flow is local: may be bounded.
For , the -limit set is the set of for which there are and with . The stable and unstable sets of are , where is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant is attracting if is a neighborhood of . A trapping region is an open connected with compact closure such that for all .
The divergence of is . On phase space , a Hamilton function defines Hamilton's equations , , whose right-hand side is the Hamiltonian vector field . The Lorenz equation is , , with . Volume is Lebesgue measure.
For on an open , with the flow of on , every measurable and every time at which all points of are alive satisfy
The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives , so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.
Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an -limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.
Lemma 8.8 and Theorem 8.10 need the flow map to be a diffeomorphism of the set of points alive at time onto its image. They also need its Jacobian to satisfy the first variational equation , whose determinant obeys Liouville's formula for linear systems. None of this is available for a general vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of , not just , to be alive at . Without that, can have infinite volume (, , ).
Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about must first establish that the points involved are alive at time . The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function from the text has , not , so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.
is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points , momenta first. volume on it is Lebesgue measure on . The flow is a pair satisfying IsMaximalFlow, which makes the unique maximal integral curve on . Nothing assumes . The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:
A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with assumed. It must be proved for the flow of built from itself.
A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.
Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4Almost every existence theory for elliptic, parabolic and hyperbolic partial differential equations works in Sobolev spaces: function spaces defined through weak derivatives and integrability rather than classical differentiability. Energy methods produce solutions whose derivatives are known only to be square-integrable. Sobolev embedding theorems are what turn that information back into integrability or continuity of the solution itself, and they are used at every step of the regularity theory.
This mission covers Chapter 3, §3.1–3.8 of J. K. Hunter's graduate lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): weak derivatives, the spaces , approximation by test functions, and the two embedding regimes and .
Timeline. S. L. Sobolev proved the embedding for in 1938 by potential-theoretic methods. E. Gagliardo (1958) and L. Nirenberg (1959) independently gave the elementary proof, including , that the notes follow. The inequality behind it, for products of functions of variables, is also known as the Loomis–Whitney inequality (1949). C. B. Morrey (1940) proved the Hölder estimate for . The sharp constants were found by Federer–Fleming and Maz'ya (1960, , equivalent to the isoperimetric inequality) and by G. Talenti (1976, ).
Throughout, carries Lebesgue measure and the Euclidean norm , and is open. A test function is infinitely differentiable, and its support is a compact subset of . For a multi-index with , .
A locally integrable has weak derivative if
The Sobolev space , for and , consists of the whose weak derivatives , , exist and lie in . It is normed by , with the maximum of the suprema when .
For the Sobolev conjugate is , so that . For , is the gradient, its Euclidean length, and . The Hölder seminorm is .
For , and every ,
The goal's constant is explicit, and it is not the sharp one. A later sharp constant (Talenti's) would strengthen the goal but would not invalidate it.
The result. Theorem 3.28 is the quantitative core of the embedding . Density (Theorem 3.24) extends it to all of , giving Theorem 3.31. From there, extension operators and Rellich–Kondrachov compactness follow, and with them the existence and regularity of weak solutions to elliptic equations (Chapters 4–6 of the same notes). Morrey's inequality is the complementary statement for and yields continuity of Sobolev functions. Without these estimates, a weak solution obtained by the Lax–Milgram or Galerkin method carries no pointwise or integrability information.
Formalizing it. Mathlib contains a Gagliardo–Nirenberg–Sobolev inequality for compactly supported functions with a non-explicit constant (MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, restated on the platform as FamousTheorems.gagliardo_nirenberg_sobolev and included here as a reference item). Mathlib has no weak derivatives in the integral form used here, no spaces on open sets, no density theorem for them, no embedding, and no Morrey inequality. This mission asks for the explicit constant, the Loomis–Whitney-type product inequality in the form the proof uses, and the first results on Sobolev spaces built from integral-form weak derivatives.
The explicit constant cannot be read off Mathlib's existing inequality, whose constant is defined through its own proof. It has to come from the one-dimensional bound (Lemma 3.26) combined with the product inequality (3.10). Theorem 3.27 is an induction on dimension in which Hölder's inequality is applied on sections of and then integrated over the remaining coordinate. Expressing " with the th coordinate omitted" and Fubini across those splittings of is the bulk of the measure-theoretic bookkeeping. For the argument has to be applied to , which is only .
Theorems 3.24 and 3.31 need weak derivatives to commute with mollification and cutoff. They also need the weak derivative of a limit to be identified, and completeness of . None of this is available for the integral-form definition. Morrey's inequality needs averages over balls and polar-coordinate integration.
EuclideanSpace ℝ (Fin n) with volume. Coordinates are 0-based (i : Fin n), and multi-indices are Fin n → ℕ. is ‖gradient f x‖, which equals the operator norm of fderiv ℝ f x. norms are eLpNorm in , with real exponents coerced by ENNReal.ofReal.ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞). ContDiff ℝ ⊤ means analytic in current Mathlib, and using it for test functions would leave only the zero function, making every function weakly differentiable. A test function on has HasCompactSupport φ and tsupport φ ⊆ Ω, so the test class is all of . A smaller class would trivialize weak differentiability, and this formalization rules that out.MemW k p Ω f is membership in . sobolevNorm is the norm of Definition 3.23, valued in and built from a chosen weak derivative (unique a.e.). For it uses the essential supremum.Line search methods for unconstrained minimization of a smooth function choose a direction and a step and set . Classical rules (Armijo, Wolfe) insist that every step decrease . For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when is strongly convex.
Timeline:
Fix parameters , and . Write and . The Nonmonotone Line Search Algorithm (NLSA) keeps weights and reference values :
with chosen freely at each step. A step is accepted either by the nonmonotone Wolfe conditions
or by the nonmonotone Armijo rule , where is a trial step and is the largest integer such that the first inequality holds and . With one recovers the monotone rules.
The direction assumption asks for constants with and . The function is strongly convex with constant if
Let be the minimizer, , , and the set of points within distance of .
Let be strongly convex with minimizer , let be Lipschitz continuous on bounded sets, let , let the directions satisfy the direction assumption at every iteration, and let for all . Then there is with
The goal fixes no value of : it asserts only the existence of a linear rate.
In the paper's order of use:
Here is a Lipschitz constant of on . A further result on the same definitions is Theorem 3.2: if converges R-linearly with ratio inside a compact convex set on which is strongly convex, then the sufficient decrease condition with reference value holds for all large .
Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.
These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants , and in checked form, and a checked record of the repair of the printed statement described below.
The obvious argument would show that contracts at each step. It fails: the method is nonmonotone, and may exceed . The quantity that contracts is , and only is controlled by the line search. The contraction must be derived by relating to in two regimes, and the second regime needs a bound on from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region and the step bound enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.
Conventions:
EuclideanSpace ℝ (Fin n), is ContDiff ℝ 1, and is ⟪gradient f x, d⟫_ℝ.IsGreatest.Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large , but Theorem 3.1 concludes (3.5) for each , and its proof uses the assumption at every . As printed the theorem is false: with the Wolfe step gives , which violates (3.5) at whenever . The goal therefore requires the direction assumption for every .
The step bound "there exists with " is stated with the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use , so nothing is lost.
Trivializing formalizations are ruled out:
A complete development needs:
The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).
An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.
The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level . They also gave a verification condition under which the barrier at is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.
Let be a spectrally negative Lévy process on a filtered probability space with and Lévy triplet . Its Laplace exponent is , finite for :
Increments after time are independent of . Initial capital is added to . The standing assumptions are the following: does not have monotone paths, , and either , , or has a density.
A dividend strategy is a nondecreasing, left-continuous, adapted process with . The risk process is and the ruin time is . The strategy is admissible () if no lump sum exceeds the current reserves. Its value is
with discount rate . For , consists of the admissible strategies that keep for .
The -scale function is the unique continuous nondecreasing function on with for large . It is extended by on . The barrier strategy reflects at the level , paying at time . The paper computes its value
and the optimal barrier level is , read as when this set is empty and for all . The generator is
Assume , or has bounded variation, or . Then and:
The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.
The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, , and optimality over all strategies reduces to one inequality on . It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.
The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.
The analytic part is elementary once the value formula (5.1) is available: the choice of , Proposition 3(i) and Lemma 3(i) follow from the shape of . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for . Those identities rest on excursion theory, or on the martingale property of up to exit. The verification step, Proposition 4(i), needs Itô's formula for . Here is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only regularity when has bounded variation. Just proving that and imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of enter the Itô expansion separately and must each be bounded.
Time is (ℝ≥0). is a structure carrying the triplet and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform for . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument (it is unique). is an extended real, since it is for unbounded variation without a Gaussian part.
Values of strategies and value functions lie in . The dividend integral is a Lebesgue–Stieltjes integral over : it counts the lump sum at time and excludes a payment at the ruin instant.
Several conventions are fixed, and each is disclosed in the item it affects:
A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and is a conclusion.
A complete development needs:
The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.
In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first rounds.
The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.
Fix a dimension and an unknown parameter . In round the learner is given a nonempty decision set , chooses , and observes the reward
There is a filtration such that is -measurable and is -measurable and conditionally -sub-Gaussian: for all , with fixed.
For a regularization parameter let and let be the regularized least-squares estimate. With and a known bound , the confidence ellipsoid is
The OFUL algorithm chooses, in round , a pair maximizing over . The pseudo-regret is , where .
If , for all , and , then for every , with probability at least ,
For any positive definite , and : with probability at least , for all ,
With probability at least , for all (first claim). If , then with probability at least , for all , (second claim, stated here for ).
Theorem 3 bounds the regret of OFUL by with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.
All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases , , of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.
The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix , which is itself built from the adaptively chosen actions; a bound for each fixed does not give it.
Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed for , so sums over are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy ) requires; this is an added hypothesis. Every "with probability at least , for all " is stated as an outer-measure bound on the failure event, with the time quantifier inside the event. is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.
OFUL is a predicate on the whole process: in every round the chosen pair maximizes over , with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward is the supremum over , finite because of the reward bound.
Two corrections to the printed Theorem 3 are made and disclosed. The printed is replaced by , which is what the determinant–trace bound gives; for the corrected bound implies the printed one. The hypothesis is added: for the printed logarithm can be negative, and the printed bound would then assert . In the second claim of Theorem 2, is added, because at the claim does not follow from the first claim and the paper's proof is not available.
The goal is a probability bound over the noise, not the pathwise statement "if for all then ". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same as the conclusion.
Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on , log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general and , and reusable determinant lemmas are all welcome.
A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.
Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.
Let be a finite set of players. A game is a function from subsets of to the reals with . It is convex if
A payoff vector is , and . It is feasible if . The core is the set of feasible with for every ; in particular on .
For a nonempty coalition , the face is the set of core points with ; by convention , and . The family is the core configuration. It is complete if no is empty, and regular if and
For an ordering of the players, is the set of the first players, and the marginal vector pays each player its marginal contribution .
A payoff vector is dominated by if some nonempty coalition has and for all . A set of feasible vectors is stable if every feasible vector is either a member of or dominated by a member of , but not both.
The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").
The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors , as a further item that is not on the path to the goal.
The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.
Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.
The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint . Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.
Players are Fin n (a relabelling of the paper's finite set ), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ( plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.
Conventions committed to:
IsConvexGame.Fin (m + 1).Set.extremePoints ℝ.A formalization in which the dominating coalition may be empty, in which regularity omits , or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.
Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.
Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every with contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: , so a positive answer would contain the Green–Tao theorem.
Timeline.
The problem is open for every .
A set is an arithmetic progression of length if and for some (for the size condition forces ). For , denotes the largest size of a subset of containing no arithmetic progression of length . A set has divergent reciprocal sum if .
For every ,
This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.
A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of : bounds of the shape for every would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.
Divergence of is a very weak condition: such sets can have density zero, and the natural approach through requires bounds just past . For this barrier was only broken in 2020. For the best known bounds (Leng–Sah–Sawhney) save only a power of in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.
All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over ). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element , if present, contributes . "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with are written without a multiplicative constant and with "for all sufficiently large "; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every " forms are welcome.
A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.
A random variable with mean is sub-Gaussian with parameter (Definition 2.2) if for all ; it is sub-exponential with parameters (Definition 2.7, a strictly milder condition) if the same bound holds only for , with the convention so that recovers the sub-Gaussian case exactly.
A sequence , adapted to a filtration , is a martingale difference sequence if each is -measurable and . Such sequences arise throughout statistics via the Doob martingale construction: given a function of independent variables , setting telescopes to , converting a deviation question about into a martingale concentration question.
A function is -Lipschitz with respect to the Euclidean norm if for all (Eq. (2.38)).
Let be i.i.d. standard Gaussian and be -Lipschitz with respect to the Euclidean norm. Then is sub-Gaussian with parameter at most , and hence
The bound is dimension-free: it depends on only through 's Lipschitz constant, not the ambient dimension itself.
For any differentiable and convex , for independent — the interpolation identity Theorem 2.26's proof is built on.
Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound for , the sum is itself sub-exponential with parameters , and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.
Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field —
the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid
inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform
(azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as
kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz
concentration is separately significant: it is the tool behind dimension-free operator-norm
bounds for random matrices, concentration of the empirical spectral distribution, and much of
the machinery of Chapters 5 and 6 of the same book.
Formalizing it. No faithful prior art exists on the platform for either the martingale
Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale
Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz
concentration" returned no hits; the existing Vershynin-book item
HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on
the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian
vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as
open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused
from the platform's existing, already-proved formalizations.
The naive approach to Theorem 2.26 — try to bound directly via a Lipschitz-type argument in — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an -net of the domain) picks up a factor that grows with . The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity with the linear, and hence exactly computable, Gaussian quantity , at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly times while keeping track of the interplay between the two parameters per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.
Expectations are Bochner integrals against an explicit probability measure, with integrability
required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner
integral silently returns for a non-integrable function, which this mission's definitions
rule out as a trivializing formalization). The sub-exponential condition's domain restriction
|λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division
convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention
for the degenerate sub-Gaussian case.
" independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's
HasGaussianLaw predicate together with explicit coordinatewise mean-zero and
identity-covariance hypotheses, which together pin down the standard multivariate normal law,
plus IndepFun. The inner product is realized as
fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to — equal to
by the Riesz representation of the gradient on a
Hilbert space, avoiding the need to separately construct a gradient vector field.
Theorem 2.19's printed parameter pair for part (a), "," is formalized
as : Definition 2.7 parametrizes the sub-exponential MGF bound
by (with appearing in the exponent), so a literal transcription of the printed
pair's first entry would silently square the effective parameter and make part (a), read
literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from
part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is
the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full
derivation.
Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.
Call cube-free if no triple has all seven of , , , , , , inside . The triple is unconstrained, so a degenerate one counts. Write for the largest size of a cube-free subset.
The conjecture. for every .
This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of , arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.
The bound is sharp, and the extremal set is explicit: , the odd residues together with those congruent to 4 mod 8. Its size is . In the layer language of Long and Wagner this is .
The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at , and it is the largest class on which the conjectured constant is proved.
For arbitrary sets the best published unconditional bound is . Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward . The residual gap is exactly , that is elements.
Small values are , , , , , , , matching from on.
State those values honestly. They come from solver searches, Gurobi in Long and Wagner for and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at ", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So is solid and is not certified. Nothing in this mission rests on either.
The goal item is the conjecture itself, for , and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances and are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.
The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then and .
Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves in no layer at all and needs the last layer special-cased.
CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.
Euler's constant measures the gap between the harmonic numbers and the logarithm:
It appears wherever the harmonic series is compared against an integral, and it is the value at of the digamma function, , equivalently . Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
For and the arithmetic questions were settled long ago: both are irrational and transcendental. For , neither is known. It is not known whether 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,
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.
Progress has come in three forms, and the milestones below formalize each.
Conditional bounds on a putative denominator. If were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing to places by an algorithm built on modified Bessel functions, showed any denominator exceeds ; a continued-fraction analysis by Papanikolaou (1997) pushed this past . 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 with the Euler–Gompertz constant
Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of and 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 , gave criteria equivalent to the irrationality of in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of , together with the identifications and and the numeric bounds . Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is , where
The formalization must establish membership of every real number at least , including the endpoint, and show that no half-line starting below is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune -regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
For a finite simple graph and a vertex set , the associated cut consists of all edges with one endpoint in and one in . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.
The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
The main theorem follows the paper's structural lemma:
The graph may depend on . The existence quantifier does not request an efficient algorithm or a numerical order bound.
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
Thus choosing refutes the intended universal assertion that some girth threshold works for every graph of average degree below .
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every , Matching Cut is NP-complete even for bipartite graphs of girth at least and maximum degree at most . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least means every such cycle has length at least , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
A polynomial is split if and for some and . Split polynomials are the simplest non-constant maps defined over that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into .
Say is -collapsible if there are split with , collapsible if it is -collapsible, and eventually collapsible if it is -collapsible for some . Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree : Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is . For the one-step notion the picture is different — degrees and are settled, and degree is open. That one-step cubic case is this mission's goal.
Let be an algebraic number with . After an affine change of variable over one may assume is a root of a depressed cubic
with discriminant . When the cubic is totally real (three real roots); when it has one real root and a complex-conjugate pair. In the latter case write the roots as
and set , the parameter that controls the archimedean obstruction below. Scaling sends , so the single rational invariant
determines the problem up to scaling: the search space is one rational parameter, not two.
This is the weakest statement that settles the case: it fixes no bound on , and asserts only that some split exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
The mission also carries, as a plain theorem rather than a milestone, the single open instance — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree . A disproof would be at least as informative: a single cubic admitting no split with would separate -collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing , and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance and the goal itself are open.
The obvious approach is to write down a split with rational roots and force by solving for the roots. This works when is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose and is split with . Irreducibility of forces to be divisible by , hence , hence . Each factor lies on a fixed circle through and determined by , and a convexity argument on then forces
As one has , so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For the bound already gives , which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as . For an algebraic number of any degree with a real conjugate and a non-real conjugate , irreducibility gives the same relation , the images again lie on a circle through and , and the parameter is , which specialises to in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case () the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of . Whether degrees stay bounded there is itself unsettled.
Representation. IsSplit f says and for a nonzero rational and a multiset of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for in an arbitrary field carrying a -algebra structure, not only for , so the results apply verbatim to a root in , in , or in . The goal theorem is stated over , with "cubic" expressed as .
Ruling out a trivialisation. Collapsible places no lower bound on and does not require the value to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: would make , impossible for an irreducible cubic dividing a polynomial that splits over . Constant is excluded by . Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
Conventions in the archimedean milestones. In the cubic bound the parameters enter as real numbers satisfying the factorisation identity, with the normalisation ; this is not a restriction, since is determined only up to sign and the sign may be chosen. Under it , and the conclusion is with the natural-number degree.
In the general bound the corresponding normalisation is . It forces , so is genuinely non-real and , hence and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when , which the hypothesis excludes and which cannot occur for a depressed cubic with . No degree hypothesis on is needed: possessing both a real and a non-real root already forces .
Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of on . The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of of any degree.
[VM-STATUS-20260908-R05-PROVED]
Status update (2026-09-08): The root theorem
OPG500Counterexample.eight_vertex_counterexampleis now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
Let be a finite simple graph. A positive edge-length assignment is a function
such that for every edge . The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle is -geodesic when, for every pair of vertices on , at least one of the two – arcs of has length equal to the shortest-path distance between and in . Equivalently, there is no – path in whose length is strictly smaller than both – arcs of . The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph on vertices . The vertices induce . For each , set and join to exactly the three core vertices other than . The four vertices are pairwise nonadjacent. Thus the frozen edge set is
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
Formalize the following statement for the fixed graph :
The existential cycle may depend on . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
The Lean development will use Fin 8 for the vertices of and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924The linear feasibility problem takes a matrix and a vector and asks whether the system of linear inequalities in real unknowns
has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.
What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time . In the real-number model the input is a list of exact real numbers, each arithmetic operation (), comparison, or memory move costs one unit, and a running time may only depend on and . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every , , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.
For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of but not on or , covering network flows and all -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).
For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.
The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).
Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.
Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.
The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of ; no data-independent perturbation exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).
The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.
Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:
It fixes nothing about ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.
Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of
from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.
Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound and the perturbation estimates, Khachiyan's theorem: for integer data bounded by , every admissible ellipsoid run decides feasibility within
The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on .
Level 3 — the goal (open). A uniform program with data-independent polynomial cost:
The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.
Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function would make the statement trivially true and is not the theorem. Division is totalized as and the branch test is ; both are benign for the class of programs quantified over.
The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.
A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
Fix a prime , a positive integer , and a weight . Let be a normalized cuspidal Hecke eigenform of weight on with nebentypus and Fourier coefficients (necessarily algebraic). Fix embeddings and . No condition is imposed. The character is extended by zero on nonunits modulo .
The form is ordinary when . The ordinary root is the root of
with . This convention also covers the case: if , then and the unit root is (MTT I.§12).
A measure means a continuous -linear functional on the continuous functions . It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.
The two periods and normalize the signed modular integrals. Write
and use for sign . A period system specifies nonzero periods, algebraic normalized values for , and finite generation over of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.
The goal is to construct an ordinary root, a period system, and a measure with the following interpolation property. Let be a primitive Dirichlet character of conductor , where , and let . Put . With the positive-exponential Gauss sum , define the algebraic number by
The required identity is
where all algebraic character values in the following expression are transported by :
This is the scalar period-normalized form of MTT I.§14. At both character values at vanish, leaving . At the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for , and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of ; there is no asserted continuous map from to . The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including , are allowed. Natural-number subtractions occur only in theorem contexts with and .
The signed projections use a factor of . Their normalized measures are added, and the period sign is . These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
The mission is to prove the combined open goal
for finite point sets in strictly convex position in the Euclidean plane.
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an -point set determines at most unordered unit-distance pairs. This gives the Problem 96 bound and therefore . The package uses this one-way dependency; it does not seek a reverse implication.
Let be finite. Strict convex position means that every point of is an extreme point of the convex hull of . For , the pinned multiplicity at radius counts points with . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance , then takes the supremum over convex-independent -point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.
The Problem 97 target is the canonical statement that every nonempty finite convex-independent has no four-equidistant-point property:
The Problem 96 target is the canonical asymptotic statement
where is the supremum of the unordered unit-distance counts determined by convex-independent -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound for every natural number .
The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.
The source proof reduces Problem 97 to strong induction on . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
Problem97.IsCounterexample.
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.
The canonical source is pinned at commit
757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source
statements for Problem 97
and Problem 96.
The source repository reports closed proofs of the conditional bridge to the bound
(conditional three-times bound),
the counting milestone
(nine-point counting bound),
and the exact nine-point exclusion
(exact nine-point exclusion theorem).
The remaining large-cardinality milestone is the
removable-vertex step,
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean v4.27.0; these mission statements target the
platform's v4.33.1. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
|A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of , and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.
The history is a sequence of partial uniformities:
The von Mangoldt function equals if is a prime power and otherwise. The Chebyshev function counts primes with weights; the prime number theorem is the assertion .
A Dirichlet character modulo is a multiplicative function , supported on the units and taking root-of-unity values there. The principal character is the indicator of the units; a character is quadratic (real) if and , and primitive if it is not induced by a character of a proper divisor of . The Dirichlet -function , defined for , extends meromorphically to , entire except for a simple pole at when is principal.
The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum
related by finite character orthogonality. Write for principal and otherwise. A zero of lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given is the exceptional set , which the results below constrain to have at most one element.
The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.
(1) zero_free_region (§14, pp. 88–96). There is an absolute such that for
every and every ,
with at most one exception, which is real, lies in , is a simple zero, and can occur only for quadratic non-principal .
(2) pnt_dlvp (§18, pp. 111–114). For some and all ,
(3) psi_char_of_region (§20, pp. 121–125). For a region constant there are
such that, whenever is an exceptional set for with
respect to and ,
(4) siegel (§21, pp. 126–131). For every there is
such that for every real primitive non-principal ,
(5) siegel_zero (§21, second form). For every there is
such that for every real primitive non-principal ,
(6) siegelWalfisz (§22, pp. 132–134). For every there are such
that for all , all , and all with ,
This is literally the platform proposition ThreePrimes.SiegelWalfisz.
A corollary, not a milestone, records the progression form siegel_walfisz_ap: for
and ,
Goal (three_primes, §26). There is such that every odd is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal
leaves unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace ThreePrimes
(by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and
Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis
ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of
(DirichletCharacter.LFunction),
its functional equation, the non-vanishing of on ,
Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free
region for , the explicit formula for , Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
PNT+ project contour
machinery for — Borel–Carathéodory, the
inequality, a zero-free rectangle, and MediumPNT,
. That is a template for the
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
The first idea is to run the argument character by character. It works for complex and breaks for real ones. The positivity device that pushes zeros off compares , and the trivial character at nearby points; when is quadratic, is principal and contributes the pole of at at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the term present, and milestone (6) is exactly the assertion that for this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of on together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in .
Sums run over with , matching Vino.vmSumChar and
ThreePrimes.SiegelWalfisz; Davenport sums over . The two differ by the single
term , negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's Chebyshev.psi. is Mathlib's
DirichletCharacter.LFunction, so no continuation is reconstructed.
The zero-free region is Davenport.InRegion c q s, namely
; the exceptional zero
is packaged as IsExceptionalSet c χ E: is a subsingleton, every element is a real
zero of in and can exist only for quadratic non-principal ,
and at every of the region outside . Milestone (1) adds
simplicity as for .
Milestone (3) takes the region constant as a parameter rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large the
hypothesis IsExceptionalSet c χ E may be unsatisfiable for some , making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small with a witness for every
, so instantiating milestone (3) at that discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with
the conclusion a lower bound on ; since is real
for real , this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are ineffective; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term
(if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal .
Milestone (6) requires strictly, which is what makes a
genuine saving over the trivial ; with allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for as an entire function of order , the zero-counting estimate (§16, pp. 101–103), the truncated explicit formula for (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction . All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the versions, and of sharper constants are welcome.
Mathlib.NumberTheory.LSeries.DirichletContinuation.
docsPolynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
Fix and the complex symplectic Lie algebra . The relevant maximal parabolic subalgebra has an abelian nilradical . Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free -module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar and a polynomial parameter . Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
Prove that for every there is one generator presentation and one family
of -representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that is a weight module exactly when is constant, and the stated simplicity criterion outside the exceptional arithmetic set
For exceptional , prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family .
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
The mission works over with natural rank . The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family . Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.