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?
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial -sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
Let be an abstract simplicial complex on a finite vertex set . Its geometric realization is formed from probability vectors whose supports are faces of . The condition that is a simplicial -sphere means that this realization is homeomorphic to the unit sphere .
For each face , assign a copy of the closed disk at vertices in and the boundary circle at vertices outside . The associated moment-angle complex is
The all-ones point is a canonical basepoint. Write for the based loop space with the compact-open topology. For a space , the mission uses total integral singular homology
as an additive abelian group. Saying that an abelian group is a subgroup means that there is an injective additive homomorphism .
For every finitely generated abelian group , prove that there are an integer and a simplicial complex on Fin m such that and there are injective homomorphisms
The quantifier order matters: the same and the same must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
The theorem gives a universality statement for moment-angle manifolds over simplicial -spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of , the union of disk-circle products, the homeomorphism , and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
Lean represents using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit -sphere.
The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in , and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.
A loss network accepts a request only when all resources needed by that request are available. An accepted telephone call, for example, occupies circuits on several links at once. A blocked request leaves immediately. Resource sharing makes route occupancies dependent, even when the arrival streams are independent. For a large network, its exact equilibrium probabilities may be easy to describe but expensive to evaluate. A limit theorem gives a tractable description of fluctuations around the network's typical occupancy. This mission concerns the fixed-topology, growing-capacity regime in Chapter 3 of Kelly and Yudovina, Stochastic Networks, using the supplied Lecture Notes PDF.
The question is not only where mean occupancy settles. Capacity constraints can remove fluctuation directions altogether. The target identifies the surviving Gaussian distribution and retains the moment convergence needed to extract mean occupancies from it.
There are finitely many links, indexed by , and finitely many routes, indexed by . The circuit-requirement matrix has nonnegative integer entries: a route- request occupies circuits on link . Independent Poisson streams bring requests at rates . Holding times are independent exponentials of mean one. An arrival is accepted precisely when the capacities permit its entire resource requirement.
The occupancy vector records calls in progress. With capacity vector , its feasible states are . Equation (3.3) gives the product-form law
These are countable occupancy states. The route and link index sets are finite; the occupancy coordinates have no fixed upper bound shared across the scaling sequence.
For network number , rates and capacities are and . The matrix stays fixed and has full row rank. Rates and finite-network capacities are positive, and , coordinatewise. The limiting capacities are real. A blocking vector determines carried traffic . It satisfies , with equality wherever . The limiting data also satisfy strict slack: whenever . These are the standing conditions of §3.5.1 in the source, printed page 62.
The first milestone supplies the actual normalizing sum in Equation (3.3), its positivity and convergence, detailed balance for the specified loss rates, and the resulting probability measure. It connects the exact law to the published product-form balance theorem without assuming a normalizer.
The second milestone references the complete integer-capacity primal and dual characterization of Theorem 3.10. The continuous mode uniquely maximizes
Its blocking representation is the one above. A companion theorem extends all clauses to positive real capacities. Lemma 3.13 is the third milestone:
The goal is Theorem 3.14. Center the exact occupancy law at its finite-network continuous mode:
Let , let , and put . The target is
where is the centered Gaussian supported on . Every mixed moment converges, and consequently . All these conclusions, including moments, belong to the printed theorem, page 64.
The Gaussian limit distinguishes active links from links with spare capacity. Active constraints suppress certain directions, so the limiting covariance can be singular even though all unconstrained coordinate variances are positive. The theorem also justifies passing from the limiting distribution to mean carried traffic; weak convergence alone does not justify that passage.
The published library already contains a proved product-form detailed-balance theorem with an assumed convergent normalizer. It also contains an Open statement of the full integer-capacity primal and dual characterization. Neither is a proof of the Gaussian limit. This mission adds an explicit measure model, a canonical law for null-event Gaussian conditioning, the required normalization obligation, and targets for distribution and moment convergence. The source presents the limit theorem with a sketch; the formal theorem is an unproved target, not a claim that the sketch has already been machine checked.
Local approximations to probability masses do not by themselves control mass escaping to infinity. They also do not establish convergence of unbounded moments. Remarks 3.15 and 3.16 in the source, pages 64–65, explicitly leave tail estimates out of the sketch. The formal goal retains those obligations without assuming tightness or uniform integrability. This omission is recorded as finding F3.
Another difficulty is that the event generally has probability zero under the independent Gaussian law. Ordinary division by its event probability does not define the intended distribution. Strict slack is substantive as well: at a critically loaded one-link system, removing it would incorrectly predict an unconstrained normal limit for fluctuations that are always nonpositive, as recorded in F1.
Lean uses finite link and route indices, natural matrix entries and finite-network capacities, real rates, and the full countable occupancy space. It reuses the published loss-state and weight definitions. The product measure of real Gaussians is mapped by the explicit residual . Thus the limiting covariance and support are fixed by the data. Empty active sets retain the independent Gaussian; full active rank may give a point mass. Network zero is outside the positive-data assumptions and has no effect on the limits.
Weak convergence is expressed through every bounded continuous real test function. Moments use every multi-index of natural powers, with integrability stated in the conclusion. The blocking selector is computed from the equations, with a zero fallback outside their domain of existence. Existence under positive real capacities remains a theorem obligation. No stochastic limit, moment bound, or convergence premise is hidden in that definition. In particular, a balance identity, an arbitrary proposed limit law, or convergence of means alone cannot satisfy this goal.
No selected statement contains an estimate or an unspecified failure probability, so there are no explicit-constant replacements. The sketch's unnumbered remainder estimates are not additional targets. Finite-network positivity is the standing domain in which the source defines ; no strict slack is imposed on individual finite networks.
Beyond the paper. One strengthened companion extends Theorem 3.10 from positive natural to positive real capacities while retaining every conclusion. Finding F5 records that the source's dual argument uses positivity, not integrality. The faithful integer-capacity item stays referenced as a milestone. No sharpness probe or variant of a proof gap is posed. The strengthened statement supplies the real-capacity bridge needed by the limiting regime.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a. Equivalence to a particular published printing has not been established.Queueing models describe systems that repeatedly change state: a customer arrives, a service completes, or a circuit becomes free. Their long-run behaviour depends both on how frequently states are visited and on how long each visit lasts. Looking at an equilibrium trajectory backwards produces another process, whose transitions can expose relationships among these quantities. Chapter 1 of Kelly and Yudovina, Stochastic Networks (2014) introduces this operation before using reversibility in network models. The present target is its countable-state process theorem, Proposition 1.1, in the supplied lecture-notes PDF.
A finite matrix identity alone does not describe what happens to an observed random trajectory. The object here is an actual collection of random variables on one probability space, indexed by every real time. This distinction matters for queues: their occupancy can have arbitrarily large integer values, even when every state has a finite rate of departure.
A state space is a nonempty countable set equipped with its discrete measurable structure. On a probability space with probability measure , the variable records the state at time . The Markov property says that the conditional law of a later observation, given a finite history with positive probability, depends only on the latest state in that history. This property is defined directly through event probabilities.
A jump rate is nonnegative, and the book sets . Its row sum is the exit rate from ; every exit rate is positive and finite. Irreducibility means that every state can be reached from every other along a finite sequence of positive-rate transitions. The paths have positive holding intervals and only finitely many changes on each bounded time interval. This is the chapter’s nonexplosion convention.
An equilibrium distribution consists of strictly positive numbers summing to one and satisfying
For a process in equilibrium, at every time. Stationarity is recorded as invariance of every finite-dimensional distribution under a common translation of its time arguments. These conventions follow the source’s definitions on printed pages 13–15, PDF pages 21–23.
The first milestone is Exercise 1.1. If is exponential with rate , then, for ,
If is independent and exponential with rate , then is exponential with rate . The existing proved memorylessness result is retained as a reference; the new exercise item includes both source conclusions.
Exercise 1.2 distinguishes the distribution at an arbitrary time from that at a jump. With the finite normalizer , the jump-chain probabilities and equilibrium masses are
The target asserts positivity, normalization, and the jump-chain equilibrium equations. This milestone is a supporting result about the same rate model; it is not claimed to be a prerequisite invoked by the printed reversal proof.
Exercise 1.3 characterizes the Markov property by conditional independence of the past and future. For any finite past observation event , finite future observation event , and present state with positive probability, it asserts the equivalence with
Both directions of the equivalence are part of the target.
The goal is Proposition 1.1: for the actual random variables , the reversed process is stationary and Markov, with equilibrium distribution and rates
This includes the off-diagonal small-time conditional-probability limits. All four targets are from printed pages 16–17, PDF pages 24–25, of the supplied source.
The theorem identifies the stochastic process seen under reversal, including its conditional laws and the rate at which each possible transition occurs. It supplies the foundation for distinguishing general stationary processes from reversible ones. Reversibility requires the reversed rates to agree with the original rates; stationarity by itself does not require that agreement.
The existing finite-state rate-balance theorem establishes an algebraic part of the picture. An existing finite-state reversal theorem treats finite-dimensional distributions constructed from a finite transition matrix. This mission adds the countable-state theorem for specified random variables on a common probability space. The mathematical result is classical; the deliverable is a faithful formal statement and, subsequently, a machine-checked proof. The local theorem bodies remain proof obligations.
The central issue is preserving conditional laws when the ordering of observations is reversed. A balance equation has no history events and cannot establish this property. Countable summations also require genuine convergence; a real-valued infinite sum without a summability condition can return Lean’s default value and lose the intended probabilistic meaning.
The printed proof has a minor diagonal oversight, recorded as finding F1. Its displayed small-time expansion cannot hold on the diagonal, where the probability of staying in the current state approaches one. The statement’s zero-diagonal convention remains intact. The goal must also retain nonexplosion without imposing a finite mean jump intensity in equilibrium: those are different requirements, as finding F3 illustrates.
All random variables are measurable and all measures used for probability calculations are probability measures. Real conditional probabilities are ratios of finite event probabilities, with positive conditioning events at every nontrivial use. Exponential laws and independence use Mathlib’s existing measure-theoretic definitions. Finite time lists use Fin n, including empty lists. State spaces use Countable, never Fintype.
The process predicates are explicit local abbreviations inside the goal statement. They contain real definitions, not unproved model axioms. The path predicate permits either adjoining state as the value exactly at a jump, because reversing time exchanges left and right continuity. Away from jump endpoints it requires locally constant paths, with finitely many possible changes on every bounded interval. No claim that the literal reversed path is right-continuous is made.
The published balance definition is retained as a reference. Its formulas appear directly in the theorem statements, so no new globally named balance or reversed-rate definition is introduced and no missing shared module is imported. Every infinite real sum is guarded by Summable or HasSum. The normalizer’s positivity is proved as part of Exercise 1.2, while positivity of each equilibrium mass is a standing source assumption. No asymptotic constants are instantiated: the targets contain no big-O estimates or high-probability bounds.
The goal cannot be discharged by defining Markovianity to mean past–future independence, or by substituting a rate-balance identity for the reversed process. Contributions proving the conditional-law equivalence, the countable summation identities, and the full reversal statement fit this scope. No variant items are posed; the faithful source statements remain the goal and milestone anchors.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.John Conway asked whether a graph on 99 vertices can have every edge in exactly one triangle and every nonedge in exactly one quadrilateral. He included this question among his five $1,000 problems and explicitly accepted either a construction or a proof of impossibility (Conway, 2017). This mission organizes structural constraints and graph reconstruction around the existing public formal statement, which remains open. It complements the existing Conway mission: both point to the same mathematical question, while this mission curates additional published intermediate theorems and the precise bridges still needed to use them.
The historical restriction most relevant here is Wilbrink's 1984 theorem that a hypothetical graph cannot be vertex-transitive (Wilbrink's paper). That result is already formalized on Prove2Me. The consolidated local Conway99 development also contains graph-owned point, finite-field, and rooted constraints. Its written and finite-check results have different verification levels; the platform-accepted lemmas cited below are the machine-checked part of that work.
A strongly regular graph with parameters is a finite simple graph on vertices in which each vertex has neighbours, adjacent vertices have exactly common neighbours, and distinct nonadjacent vertices have exactly common neighbours. Write for a candidate graph and for its integer adjacency matrix, whose entry is when and are adjacent and otherwise. Let be the identity matrix and the all-ones matrix. In this mission, the parameter tuple is .
The condition makes each edge part of a unique triangle. Each vertex's 14 neighbours split into seven paired edges. The condition makes each nonadjacent pair have exactly two common neighbours. These facts lead to triangles and the matrix equation , both already proved on the platform (triangle count, matrix identity). Choosing one vertex as a root splits the remaining vertices into its 14 neighbours and 84 nonneighbours; the graph's actual adjacency blocks then satisfy further identities (rooted theorem). The word actual matters: arbitrary matrices satisfying some of these identities have not thereby been shown to arise from one graph.
This is the already published Conway99.conway_99 theorem, reused as the goal. A graph satisfying it proves existence; a proof of the negation of this full existential settles nonexistence. Neither outcome has been established in the archive.
The first layer collects necessary facts about every hypothetical : rooted block equations, point-Gram identities, and finite-field identities. The accepted theorems are rooted blocks, point Gram, and finite fields. An independent binary cut-response rank theorem supplies reusable seven-vertex algebra; its statement does not assume a Conway graph. A selected twelve-owner contact theorem gives a further conclusion only when its chosen triangle, owner set, and regularity premises hold.
The reconstruction layer asks whether compatible local data can be obtained from, or assembled into, one graph satisfying all four strongly regular parameters. The public adjacency-matrix formulation and triangle line-system formulation are still open. A future coclique-completion equivalence concerns graphs with a specified independent 22-set; it cannot replace the unrestricted goal unless that set is shown to exist in every candidate. No unpublished or pending statement is presented as a completed milestone.
An accepted admitted-coclique spike theorem supplies a precise lattice membership identity when a 22-point set and its point-vector average are already admitted to one lattice. It does not produce that coclique, establish the needed lattice for every graph, or close the reconstruction gap. An accepted printed-census correction is retained as a reference to prevent the known erroneous expressions from being reused as graph counts; it is an audit of formulas, not a structural exclusion.
A construction would settle Conway's existence question with a checkable 99-vertex object. A nonexistence proof would explain why the local triangle and common-neighbour conditions cannot coexist globally, despite the standard parameter equations being consistent. Either result must address the whole graph, not one selected root, lattice, shell, or completion packet (Conway's question; formal goal).
The formalization already gives reusable graph-owned interfaces: block identities from an actual root, a point Gram representation, and modular restrictions. Those are machine-checked necessary conditions, while deeper rank, lattice, triangle-transport, and finite-support exclusions in the consolidated local development remain written or locally checked mathematics. This mission makes their status visible and provides a place to connect faithful formal versions as they are published. A conditional theorem remains useful, but its hypotheses must be derived from the candidate graph before it can narrow the unrestricted goal.
The adjacency equation and its eigenvalue multiplicities constrain every candidate but do not determine the binary off-diagonal entries of . Local equations can have feasible matrix or incidence data even when those data have not been embedded in a common simple graph. Conversely, excluding a fixed support, one lattice choice, or a branch with an ordinary point leaves other configurations untouched. The consolidated local frontier records those coverage gaps, including exceptional-only configurations and unexcluded incidence systems. The central task is to close a graph-wide bridge or exhibit a graph, while retaining every hypothesis on narrower results.
The goal uses Mathlib's SimpleGraph.IsSRGWith and quantifies over a finite vertex type, a graph, and decidable adjacency exactly as in the published statement. Supporting statements may use Fin 99 after an explicit relabelling, integer adjacency matrices, finite triangle sets, real Gram matrices, and finite-field reductions. They must derive data from one G, or mark any independent packet as an additional hypothesis. A theorem about selected owners, a prescribed coclique, a particular determinant or rank, or a saved finite support must keep that restriction visible; none may silently assert that every candidate supplies it.
Existing published definitions and theorems should be imported by their platform IDs. Contributions are welcome for exact bridges between graph, matrix, triangle, and coclique representations; proofs that a conditional packet follows from every candidate; faithful formalizations of written universal constraints; and a construction or unconditional contradiction. The mission's published milestones record actual theorem statements. Prospective bridge descriptions remain research targets until they have separately audited and published platform IDs.
Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.
Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.
A bandit problem with arms is a family of probability distributions on , each with a finite expectation. A strategy plays for rounds. In round it picks an arm as a measurable function of , where the are independent uniforms on . It then observes a reward drawn from and a fresh independent uniform . The strategy together with the problem determines the law of ; is its expectation. The number of draws of arm is
is the Kullback–Leibler divergence between two probability measures: when is absolutely continuous with respect to and the integral exists, and otherwise. The binary divergence , for , is the Kullback–Leibler divergence between the Bernoulli distributions of parameters and . For it is given by (5):
It equals for and .
The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on ; fullHistoryMeasure ν ψ T is the law of , fullPullCount ψ a is , and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for .
For every strategy , every pair of bandit problems , every horizon , and every -measurable statistic with values in :
in , with . The arm laws have the finite expectations required in §1.1; their divergences may be infinite.
The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem and a statistic , usually . The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.
The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.
Two points need care. First, Lemma 1 is stated for an arbitrary -valued . The data-processing inequality only gives it directly for indicators of events, and pushing forward by gives a law on , not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When for an arm that is drawn with positive probability, the left side is and there is nothing to prove. When such an arm is never drawn, its term is . The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.
Fin K, indexed from . The horizon is a natural number; at both sides are . For no policy exists, so needs no hypothesis.FullStrategy K, measurable functions of the paper's . The same strategy runs under and . The local history law includes every auxiliary uniform, so may depend on any of them.Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.klBer, never a real formula. A real formula would return a finite junk value at , where (5) is , and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to , would be a weaker theorem and is not the target.unitInterval. is real-valued and measurable, with values in .StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size.
(https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.
A linear program asks for a point minimizing subject to linear inequalities . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev () norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables is a small constant, and what matters is how the running time grows with .
Nimrod Megiddo showed that for every fixed the problem can be solved in time (J. ACM 31(1), 1984).
Timeline.
Fix . An instance is a matrix and a vector , and its feasible region is the polyhedron . Here is the number of constraints and the number of variables.
The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory . It performs exact on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of in memory: the numbers and , then row by row, then . A program decides an instance within steps with output if it halts on that output after at most steps.
Megiddo's method rests on multidimensional search. There is an unknown point and an oracle that, for any hyperplane , answers whether , or . Given hyperplanes with , the question is how many oracle calls determine the position of relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, is an optimal solution, or a minimizer of the infeasibility function when the system is infeasible. The oracle is implemented by solving problems in variables.
The program and the constant depend on only. No explicit form of is fixed.
The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most is feasibility of together with , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.
Formalizing it. The result is proved and classical. The platform already has the cases (linear time) and (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.
The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces constraints after one step. Pivoting methods have no known bound linear in . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on only.
SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every . A tree over arbitrary tests of would make milestones 5 and 6 empty, and it is excluded by the definition.0, 1 of Fin (d + 2), and its is Fin.last d of Fin (d + 1).The diagonal Ramsey number is the least such that every red/blue colouring of the edges of the complete graph contains a monochromatic copy of . Ramsey's theorem guarantees that is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of
It is not even known whether this limit exists.
Timeline.
So today, if the limit exists, it lies in .
For consider simple graphs on the vertex set . A red/blue colouring of the edges of is the same as such a graph (the red edges) together with its complement (the blue edges). A -clique of is a set of exactly vertices, any two of which are adjacent in . Define
In the Lean development this is Erdos77.diagonalRamsey k. Small values: , , , , .
The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining remains the ultimate aim; any proof of a specific value would in particular prove this goal.
The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds and are the products of decades of work, and the lower bound base has resisted improvement since 1947.
Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.
There is no known sub- or super-multiplicativity for that would give existence of the limit via Fekete's lemma: the natural product constructions relate to and only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.
sInf of an empty set of naturals is ; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.atTop filter on ; "" in GNNW is encoded as "for every , eventually with exponent ".Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.A set of integers is a Sidon set if all of its pairwise sums () are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let
A counting argument shows , and the true order was settled early: . What remains open is the size of the error term . Erdős and Turán asked whether it is smaller than every power of ; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.
Timeline.
No upper bound with an error exponent below is known, and no lower bound of the form for every is known either.
A set in an additive commutative monoid is Sidon if for all ,
For a finite set , is the largest size of a Sidon subset of (the empty set is Sidon, so this is well defined), and
The first values are (OEIS A143824).
This is a two-sided statement: it asks both for an upper bound and for a matching lower bound for large . Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.
The result itself. An affirmative answer would pin down to up to a sub-polynomial error, in both directions; Erdős even speculated that might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of . Either answer would be the first change in the exponent of the error term since 1941.
Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this . The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.
For the upper bound, every known argument counts differences in short windows and loses at the scale ; improvements since 1941 only change the constant in front of . For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about in a modulus of size about , and the loss comes from the gap between and the nearest admissible modulus; bringing it below requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.
Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value is a natural number cast to ; is the real square root and , are real powers of . The goal's is Mathlib's Asymptotics.IsBigO along atTop on . The goal is not trivialized by any junk value: is a genuine finite maximum, and the statement concerns all large .
Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for with ; a prime number theorem in short intervals is needed for ). Contributions of reusable Sidon-set lemmas are welcome.
FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjecturesA sunflower (also called a -system) with petals is a family of sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of -element sets contains a sunflower with petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.
Timeline.
The conjecture itself remains open, even for .
Fix natural numbers (the uniformity) and (the number of petals). A family of sets is -uniform if every member of has exactly elements. A subfamily is a -sunflower if and there is a set with for all distinct .
The sunflower threshold is the least natural number such that every -uniform family (over any ground set) with contains a -sunflower.
The constants are left unspecified; only the exponential shape in is asked for. A disproof (the negation of this statement) would equally settle the problem.
A supporting sanity check, , is taken from the source formalization.
A positive answer would show that sunflower-free -uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a factor per coordinate, including monotone circuit lower bounds. A negative answer would show the -type bounds of 2019–2021 are essentially the truth.
On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.
The classical induction on (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about at each of steps, which is where comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor per level, and no known technique removes it. The case is already open.
Set (Set α) and sizes are measured with Set.ncard, which returns on infinite sets. Consequently, for only finite members can be "-element", and the condition with only applies to finite families. All targets assume (except the sanity check), so the quirks do not affect them.answer(·) statement.Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.
Dirac showed in 1931 that quantum mechanics permits isolated magnetic charges provided electric charge is quantized, but in Maxwell's theory such a magnetic monopole is a point singularity attached to an unobservable "Dirac string". In 1974 G. 't Hooft and, independently, A. M. Polyakov observed that in gauge theories where the electromagnetic group sits inside a larger group with compact covering group, monopoles arise instead as smooth, finite-energy solutions of the classical field equations, with no singularity and no string. 't Hooft's paper (Nucl. Phys. B79 (1974) 276) does this for the SO(3) model of Georgi and Glashow and computes the mass numerically. The resulting "'t Hooft–Polyakov monopole" became the model example of a topological soliton in gauge theory.
Timeline. 1931: Dirac's quantization argument (Proc. R. Soc. A 133, 60). 1972: Georgi–Glashow SO(3) electroweak model (PRL 28, 1494). 1974: 't Hooft and Polyakov (JETP Lett. 20, 194) describe the regular monopole, 't Hooft by a spherically symmetric ansatz, a reduced one-dimensional energy functional and a numerical minimisation. 1975: Prasad and Sommerfield find a closed-form solution in the limit (PRL 35, 760). For no closed form is known.
Space and isospin space are both . A static configuration in the gauge consists of a Higgs triplet and a gauge field , . With coupling , Higgs self-coupling and vacuum value (eqs. (2.1)–(2.3), with ),
and the static energy is
The vector masses are and the Higgs mass is . A static solution is a smooth configuration of finite energy at which is stationary under all compactly supported smooth variations. 't Hooft's gauge-invariant electromagnetic tensor (2.17) is
The spherically symmetric ansatz (2.8) is , with . The monopole boundary condition is as (eqs. (2.6), (2.11)).
For all , , there are radial profiles such that the configuration (2.8) is a smooth finite-energy static solution with
i.e. a regular magnetic monopole whose far field is (2.20).
The existence of a regular monopole is what makes the monopole a particle of the theory: its mass (eq. (3.3)) is finite and calculable, and its magnetic charge is fixed by topology rather than put in by hand. The ingredients (hedgehog ansatz, the zero of the Higgs field forced by the boundary condition, the reduction to an ODE system, the gauge-invariant electromagnetic tensor) are reused throughout the theory of solitons in gauge theories.
The result is established in the physics literature; 't Hooft's own argument is partly numerical (trial functions). The mission asks for a machine-checked development: the algebraic and calculus identities of Sects. 1–3, the topological zero, and a complete existence proof for the spherically symmetric solution for every . No machine-checked proof of any of these is known to the proposer.
The identities (milestones 1, 4, 6–9) are finite computations, but milestones 4, 5 and 9 must go through Fréchet derivatives of vector fields on and spherical coordinates, where most of the work lies. Milestone 3 is a degree-theoretic statement not available off the shelf. The goal needs an actual existence theorem for a nonlinear coupled ODE system on with singular coefficients at and boundary conditions at both ends, followed by regularity of the resulting fields at the origin and the passage from the reduced (radial) equations to the full field equations. 't Hooft's numerical minimisation over trial functions gives no proof that a minimiser exists or is smooth.
is EuclideanSpace ℝ (Fin 3) with Lebesgue measure; indices run over Fin 3 = {0,1,2}, the Levi-Civita symbol is an explicit formula, partial derivatives are Fréchet derivatives in coordinate directions. Fields are static and in the gauge , where the Gauss-law equation holds automatically, so "static solution" means: fields, integrable energy density, and zero derivative of the energy along every smooth compactly supported variation of and . Lean's total operations are used: division by zero is and the Bochner integral of a non-integrable function is ; every statement using them either excludes the degenerate input or is insensitive to it (the goal demands integrability explicitly). The constant is included so the vacuum has zero energy, as in (2.9).
Two deviations from the printed text, both flagged in the milestones: (i) with standard Pauli matrices, is , whereas (2.6) prints ; the milestone states the computed identity. (ii) With , (2.20) gives while (2.21) prints ; the flux milestone therefore states the magnitude , and the sign is fixed by (2.20). The asymptotic analysis (2.14)–(2.15) is formalized as an exact statement about pure power laws. The numerical values of in (3.3) are not formalized.
A trivializing reading of the goal is ruled out: the solution must satisfy the non-trivial boundary condition, which by milestone 3 excludes the vacuum, and the stationarity must hold for all variations, not only spherically symmetric ones.
Useful reusable infrastructure: spherical-coordinate integration of radial functions on , calculus of hedgehog fields, and a Brouwer-degree / no-retraction argument for maps of the sphere. Contributions of any milestone, and of alternative existence proofs (variational, shooting), are welcome.
Every generalization bound presented so far in this series is for classification, where the
error of a prediction is binary (correct or not). Regression asks a different question:
predictions are real-valued, and error is measured by the magnitude of the deviation from
the true label, via a loss function L. Chapter 11 develops generalization theory for bounded
regression, showing that the same two complexity measures used for classification —
Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function
itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or
a reduction to classification via level-set thresholding (pseudo-dimension route).
A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D
on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible);
R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For
a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the
regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2
develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in
its first (predicted-value) argument, the Rademacher complexity of the loss-composed family
G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via
Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with
chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent,
purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of
VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own
Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a
pseudo-dimension generalization bound by reducing regression to a family of classification
problems (one per threshold t), using the tail-integral identity Eq. 11.5.
Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with
probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).
Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its
first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).
Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any
δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).
Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any
δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).
Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show
"how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization
bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from
this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction —
combined via a new observation (Proposition 11.2) specific to loss-composed families, not a
restatement of either. Theorem 11.8 is the chapter's second, structurally independent
technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a
VC-dimension-style growth-function argument), but the reduction itself — regression to a
continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq.
(11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension
has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall
content either: GET /theorems?q=generalization%20bound%20regression and
GET /theorems?q=pseudo-dimension both return zero hits.
Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz
constant taken in the first argument of L only — the predicted value h(x_i), holding the
true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong
argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is
the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier
c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style
classification bound (Corollary 3.19) to the family of thresholded classifiers — whose
VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that
conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim
definition by relabeling, would misrepresent this chapter's genuinely different (real-valued,
threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.
Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless
simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter
being stated for real-valued scores and labels. EmpiricalRademacherComplexity/
RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a
draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized
via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather
than the sign-function form of Definition 11.4 directly, since the two coincide except at a
measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's
HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it
as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never
a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem
11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified
outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed
y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only,
per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the
book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the
inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any
of the four theorems.
Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation
of the general theorem for a specific loss family, not a separate numbered theorem); Theorem
11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces,
background/illustration rather than the chapter's general machinery — drafting only these
examples instead of the general Theorem 11.8 would be this chapter's trivializing
formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof
(an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear
regression, kernel ridge regression, SVR, Lasso and their online variants), which is
applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.
Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case .
Timeline.
Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any .
Fix an integer . A non-trivial -term arithmetic progression is a list of natural numbers with common difference ; the requirement is what "non-trivial" means, and it forces the terms to be distinct. A finite set is -AP-free if it contains no such progression. Write
The mission takes its formal definition of verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length when every subset of it that is an arithmetic progression of length forces . Progressions of length and count as trivial, so under that convention every set is free of them and ; the interesting range begins at . Every statement in this mission that depends on the convention carries an explicit hypothesis on .
On that range, is non-decreasing in both and , satisfies , and hence, by Fekete's subadditivity lemma, converges. Szemerédi's theorem is the statement that the limit is ; the whole difficulty of this mission lies in how fast it goes to .
This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of .
The headline theorem in that file, erdos_142, states with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for " — has no known right-hand side for any , which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for , where , and open for every . It fixes no constants, so no future improvement can invalidate it.
Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the , and variants above, and the only two files in that repository that mention at all are the ones for #142 and #139.
Proving for all yields, by a standard summation argument, Erdős's conjecture that every with contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.
Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same ; those are the only two files there that mention . The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.
Every known upper bound for runs a density increment: if of density has no -term progression, find a long subprogression on which has density , and iterate. The bound this produces is governed entirely by two quantities — how large the increment is, and how much of the interval survives one step. For the increment is extracted from an inverse theorem for the Gowers -norm, and the best available correlation bounds there are quasipolynomial in ; iterating a quasipolynomial increment cannot do better than , which is nowhere near . Reaching requires an increment with polynomial dependence on together with a subprogression of polynomial length, and that combination is currently available only for , through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at is , so the answer is not a power of and cannot be produced by any argument whose output has that shape.
The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.
The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length with first term and difference when it has exactly elements and equals ; it is free of length- progressions when every progression of length inside it forces ; and is the supremum of over subsets free of length- progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over ; the file proves the two facts that make it a genuine maximum (le_r and r_le).
An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.
Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length- and length- progressions are trivial, so every set is free of them and ; monotonicity of in therefore holds only from onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is at ; this is invisible to atTop.
A trivializing formalization is ruled out by construction: one milestone asserts rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.
A full development needs: discrete Fourier analysis on , Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the case of a general- milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.
FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of . https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.leanAn elliptic curve over is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group (Mordell, 1922), so for an integer , the rank. No algorithm is known that decides, for a given curve, whether , i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts from an analytic object, the Hasse–Weil -function : it asserts that equals the order of vanishing of at . It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
Timeline.
A Weierstrass equation over is
with discriminant ; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when (Mathlib's typeclass IsElliptic). Its rational points are the rational solutions together with the point at infinity , an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a -module,
the in .
The Hasse–Weil -series is built prime by prime. For each prime take a Weierstrass equation for that is minimal at (integral coefficients, with the -adic valuation of as small as possible) and reduce it modulo ; put when the reduction is smooth (good reduction). The local factor is
and , convergent for by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function , an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value . This is the complete -series of Wiles' Remark 1; it differs from the incomplete product over in Wiles' display by finitely many factors holomorphic and non-zero at , so both have the same order of vanishing there.
An -function of is an entire function with for (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of at is the with , ; in Lean, analyticOrderAt Λ 1, valued in , with value exactly when vanishes identically near .
BSD.birch_swinnerton_dyer)For every elliptic curve over there is an entire agreeing with on such that
This is Wiles' Conjecture (Birch and Swinnerton-Dyer): with and . Open.
BSD.weak_birch_swinnerton_dyer)There is an -function of with if and only if is infinite. Wiles: "In particular this conjecture asserts that is infinite." Open.
BSD.mordell): is a finitely generated abelian group.BSD.lSeriesSummable): converges for . Wiles: "this Euler product is then known to converge for ."BSD.exists_isLFunction): has an -function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an -function of vanishes to order at most at , its order equals the rank. Wiles: "If with and or , then the conjecture holds."A bridging lemma, BSD.isLFunction_unique, records that an -function of is unique when it exists.
The result itself. The conjecture makes the finiteness of decidable from and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of -functions.
Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on , minimal models and reduction types over discrete valuation rings, and the Hasse–Weil -series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of . On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as ; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own -series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of , founders on Ш. On the analytic side one can certify or numerically but cannot certify an exact zero, and the only known bridge from -values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order and the conjecture is not known for a single curve of rank . Iwasawa theory (Kato, Skinner–Urban) relates -adic -functions to Selmer groups but yields -adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
WeierstrassCurve ℚ with IsElliptic (); no minimality or integrality of the model is assumed. Mathlib's -series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the in ; for a group of infinite rank Mathlib's finrank is , a case milestone 1 excludes.WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value where the Dirichlet series diverges. BSD.IsLFunction constrains only on ; milestone 2 shows the series is genuine there, and the bridging lemma shows is then unique.analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that near .No trivializing formalization. The existential cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is or ; the hypothesis is required, not decorative.
Out of scope. The refined conjecture (the leading coefficient in terms of Ш, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш, number fields and abelian varieties, and the functional equation of .
Infrastructure needed and welcome contributions. Heights on and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of ; a bridge from Mathlib's WeierstrassCurve.LSeries to the -series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.
Our goal
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.
Important references
Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
OpenGA's role
OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
If is algebraic and , is transcendental? Guy Diaz asked this in 2004 and it is still open. Note it is , not — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that itself may be transcendental while only its modulus is constrained.
Write for the algebraic numbers in and
for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of has algebraic modulus. He states it as
« Soit avec ; alors est transcendant. »
The statement fits on one line and needs no machinery beyond and . It has been open for twenty-two years.
It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.
The mission decomposes into work that can be done now, without any open input.
Two milestones are conditional theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all Prop-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.
A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where and are -linearly dependent.
The remaining two milestones are classical theorems that the platform's Mathlib does not have: Hermite--Lindemann and the six exponentials theorem. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.
Only the top node needs genuinely new transcendence.
One structural remark that shapes the whole ladder: Hermite--Lindemann is a special case of the goal, not just an input to it. If is algebraic then is algebraic, hence so is , and the goal applied to gives that is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.
| 1873, 1882 | Hermite, then Lindemann: is transcendental for algebraic . In particular every non-zero element of is itself transcendental, so a counterexample would be a transcendental number with algebraic modulus and algebraic exponential. |
| 1934--35 | Gelfond and Schneider settle Hilbert's seventh problem. |
| 1966 | Lang's Introduction to Transcendental Numbers records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The four exponentials conjecture stays open, and still is. |
| 1966 | Baker's theorem on linear forms in logarithms. |
| 1997 | Diaz studies the companion condition , assertion (4-1), p. 237. |
| 2000 | Waldschmidt's Diophantine Approximation on Linear Algebraic Groups states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with , at p. 15. |
| 2004 | Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps and enter a transcendence proof at all? |
| 2026 | A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched. |
For a candidate one has with algebraic, hence
So is not independent data: complex conjugation on is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at https://github.com/carlok/diaz-modulus-lean: a ring homomorphism fixing and carrying to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over separates a candidate from an ordinary complex number placed on the same circle.
The practical consequence for solvers: accumulating algebraic relations between and until they collide cannot settle this. A successful attack has to introduce information that is not a rational function of over — which is precisely Diaz's own methodological question, still open.
Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean — verified in all three of the platform's pinned revisions (0df444a3, c5ea0035, 777aaa61), none of which contains transcendental_exp. Hence the choice to carry it as a Prop and give it its own milestone rather than assume it. There is an open PR, leanprover-community/mathlib4#28013 (feat: Lindemann-Weierstrass Theorem, opened 2025-08-05, label awaiting-author as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.Algebra.trdeg has almost no computational API. It is cardinal-valued, with transcendence bases and lift_cardinalMk_eq_trdeg, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if with transcendental over then ". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.A -packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.
A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph satisfies . Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.
A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a -factor. Candidate C02 gives an explicit proposed family of order that has -factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.
All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.
A -factor is represented by a natural number , together with a bijection
such that, in every block, positions and are adjacent and positions and are adjacent. The path is not required to be induced: an ambient edge between positions and is allowed because the two selected path edges still form a copy of .
A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching such that the relative complement is a divisible 2-factor.
The explicit graph is defined on . Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.
For every finite simple graph ,
This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.
The mission also formalizes the part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a -factor. Two route lemmas state that divisible 2-factors split into -factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.
The C02 milestones ask first for the complete 18-vertex statement and then for the full family:
This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every in the proposed family explicitly satisfies the desired conclusion.
A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a -factor; the C02 family does not claim this.
Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced -factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.
The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated -factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.
The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.
The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.
The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The family includes . The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.
Welcome contributions include proofs of the model lemmas, the finite statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.
14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.mdThe smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1
Let be the unit sphere in , with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on . The given atlas is arbitrary: it is not defined by transporting the standard structure from .
For a homeomorphism , let denote the atlas transported from the standard sphere along . A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate requires, for every given smooth atlas on such an and every such , a structomorphism between and . It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]
For every manifold with the preceding hypotheses, the goal is
This is the source predicate . Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
The atlas formulation has the exact equivalence
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
where is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]
Write for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
where denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
Explicit standard-disk foundations form another track. For every , they concern the manifold-with-boundary structure on , its boundary set , and the smooth collar
The collar is a closed embedding, has image
and satisfies , using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a map from a manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is . These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]
For each integer , let be the closed unit disk in and let be any homeomorphism of its boundary. The twisted double identifies the boundary point in a left copy of the disk with in a right copy. With the quotient topology, the target is
This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth ; the reverse requires smooth . The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of . They are exploratory tools, not established milestones in a proof of the main goal.
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order . Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every , so their dimensions are . The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.
Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.
Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.
Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.
Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a -dimensional polytope with facets is at most . Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in and ?
Work in . An H-polytope is a set cut out by finitely many linear inequalities: given vectors and reals , it is
where is the standard inner (dot) product — so each condition is one linear inequality, with normal vector and offset . Throughout, is assumed nonempty and bounded. The parameter counts the inequalities in the given description; since every polytope with facets admits a description by exactly inequalities, bounds stated in terms of over all descriptions are equivalent to bounds in terms of facet counts.
A vertex of is an extreme point. Two vertices are adjacent when the segment is an extreme subset of ; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that is a one-dimensional face — an edge. The combinatorial diameter of is the diameter of the graph of vertices and edges. Throughout, "diameter at most " is expressed as: every two vertices are joined by a walk of steps, each step staying put or crossing an edge — a form that is monotone in and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
Every polynomial in and is dominated by some and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
Six classical results over the same definitions: the Hirsch bound in dimension (Klee; Klee–Walkup); Larman's bound ; Naddef's bound for -polytopes; the Kalai–Kleitman bound ; Todd's bound for full-dimensional with ; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds .
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all in scope. The dimension parameter is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.
Welcome contributions: any milestone in any order (dimension_three_bound for cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
In many sequential decision problems, changing the action is costly or administratively limited: a retailer can revise a posted price only a few times per season, a clinical trial can change its treatment allocation only a few times, and a firm can reconfigure its production line only so often. The multi-armed bandit with switching constraints (BwSC) captures this tension between learning and limited adaptivity: the learner must explore to find a good action, but every change of action consumes a hard budget. Simchi-Levi and Xu (arXiv:1905.10825, Management Science 2023) determine the optimal regret of this problem up to logarithmic factors.
Timeline. Classical bandit theory gives the minimax regret for arms and horizon with unlimited switching (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020). Cesa-Bianchi, Dekel and Shamir (2013) showed that in adversarial bandits with switching costs the regret is . For stochastic bandits processed in a fixed number of batches, Perchet, Rigollet, Chassang and Snowberg (2016) and Gao, Han, Ren and Zhou (2019) obtained regret rates of the form for batches. Simchi-Levi and Xu (2019, revised 2021) treat a hard budget on the number of switches and prove matching upper and lower bounds; the lower bound, Theorem 2, is the subject of this mission.
There are arms and rounds. In round the learner picks and observes a reward from the unit-variance Gaussian environment with mean vector ; admissible environments have mean spread . A policy chooses by a Markov kernel from the past actions and rewards; is the law of the history. The regret is
With unit switching costs, the number of switches is . For a budget , the class of -switch policies consists of the policies whose number of switches is at most almost surely under every environment.
The budget enters through the phase index (with ) and the remainder (so ). Two rates appear, with :
In Lean these are IsSwitchPolicy S T π, qIdx S K, rIdx S K, rateA K S T, rateB K S T, on top of the published BanditPolicy, banditMeasure, banditRegret and gaussianBandit.
There is an absolute constant such that for all , , and every , some admissible Gaussian environment satisfies
The constant is not fixed: the goal asserts the shape of the bound, which survives any improvement of constants.
The proof in Appendix J (pp. 59–75) reduces to the regime (p. 59, two bounds by outside it) and then runs a five-step program on two families of environments:
The result. Theorem 2, together with the AdaLS upper bound (Theorem 1), shows that the optimal regret is for every , and . In particular, for fixed the regret as a function of is : it changes only when crosses a multiple of , a phase transition in the switching budget, and switches suffice for the classical rate. The lower bound holds for all randomized adaptive policies, not only batched ones.
Formalizing it. The result is proved on paper but has no machine-checked proof. Formalizing the lower bound adds a reusable change-of-measure toolkit for adaptively collected data: a reverse Fano-type inequality over families of measure spaces, stopping-time-based counting arguments on switching patterns, and divergence bounds for censored histories. Three printed steps needed repair (see Formalization scope), so the formal development also certifies a corrected version of the argument.
The obvious argument fails at the counting step. A naive choice of risky events (arms unobserved in fixed time windows) only gives a sum of probabilities of at least , which vanishes when is at the end of a phase; this loses the floor in the exponent. The paper's events in the last window are defined through the stopping time at which the switching budget is exhausted, and they interact with the measure-change step: the restricted measures must hide enough information about the tested arm to make divergences small, while still deciding the stopping-time event. A second difficulty is that the policy is adaptive and randomized, so all events and measures are path-dependent.
Fin T → Fin K × ℝ; rounds are 1-based in every statement (entry is round ). Environments are unit-variance Gaussian (gaussianBandit), which is all the proof uses (p. 59).IsSwitchPolicy S T π asks the budget to hold almost surely under every unit-variance Gaussian environment, a weaker requirement than the paper's "for all sub-Gaussian ", so the goal covers at least the paper's policy class. The regret lower bound is witnessed by one Gaussian instance with mean spread at most , which implies the paper's bound on the supremum.klDiv in , and the reverse KL is ; conditional expectations in Lemmas 8 and 10 are stated in product form.ExploreFirst.FundIneq.klBer, the first half of Lemma 5 (ExploreFirst.Collective.lemma_6) and the classical bound BanditAlgorithm.bandit_minimax_lower_bound. Needed and reusable beyond this mission: the divergence decomposition for stopped histories, joint convexity and data processing for KL across different spaces, and the KL divergence of unit-variance Gaussians. Proofs of any milestone, and of the Gaussian-instance reduction, are welcome.A decision maker who must choose between two uncertain profits and rarely knows their own utility function precisely. Stochastic dominance replaces a single utility by a whole class of them: is preferred if every utility in the class prefers it. The resulting partial orders are the basic consistency requirement for risk and acceptability functionals in finance, insurance and stochastic programming: a sensible acceptability functional must never rank a dominated position higher. Dominance constraints are also optimization constraints in their own right, as in the portfolio models of Dentcheva and Ruszczyński (2003).
The analytic characterizations formalized here have a long history. The equivalence of concave dominance with the existence of a mean-preserving kernel goes back to Hardy, Littlewood and Pólya, Blackwell, Stein, Sherman, Cartier, Fell and Meyer, and was given its general form by Strassen (1965). The equivalence between the integrated distribution and integrated quantile function forms of second-order dominance is due to Ogryczak and Ruszczyński (1999). The mission follows the presentation in Chapter 1 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), §1.2.1–1.2.3, pp. 6–19.
All outcomes are profit variables: larger is better. A distribution is a probability measure on , with distribution function and left-continuous quantile function
For a distribution with a finite first moment, the integrated distribution function (IDF) and the integrated quantile function (IQF) are
and is its mean. For a nonzero mean, the Lorenz curve is .
Four orders are defined through utility classes. For distributions (laws ), means
for every in the class for which both integrals exist: all nondecreasing for first-order dominance ; all nondecreasing concave for second-order dominance ; all concave for concave dominance ; all convex for convex dominance . In the Lean development these are FSD μ₁ μ₂, SSD μ₁ μ₂, CCD μ₁ μ₂, CXD μ₁ μ₂, and , , , , are distributionFunction, quantileFunction, integratedDistributionFunction, integratedQuantileFunction, lorenzCurve, all in the namespace RiskFunctionals.StochDominance.
For probability measures on :
and, when both have a finite first moment,
The goal is the conjunction of all six parts.
Theorem 1.13 converts statements about infinitely many utility functions into checkable statements about one function: a distribution function, a quantile function, or one of their integrals. Every later use of dominance in the book rests on it: the consistency of the average value-at-risk and of distortion functionals with second-order dominance, the representation of deviation functionals, and the dominance-constrained portfolio models. Part 4 is the bridge from an order on distributions to a construction on random variables (a mean-preserving spread), and part 6 is the form in which second-order dominance enters optimization, through the integrated quantile function that underlies the average value-at-risk.
All six equivalences are classical and proved in the literature. What the mission adds is a machine-checked version in the book's own conventions: utility-defined orders with the "integrals exist" side condition, the profit sign, the left-continuous quantile function and the lower-tail integrals. The platform already holds proved results in neighbouring conventions (Shaked–Shanthikumar's tail-integral characterization of the increasing concave order for random variables, and the conjugacy of second-order performance and quantile functions in Dentcheva–Ruszczyński's form); connecting them to the book's formulation is part of the work.
The directions from an analytic condition back to the utility-defined order are the substance: they must cover every utility of the class that happens to be integrable against the two given laws, including unbounded ones, and the book's printed argument for part 3 passes to a limit over concave utilities without saying why the integrals converge. Part 4 is Strassen's theorem; the book gives no proof, only a reference, and the kernel has to be a measurable family of probability measures satisfying the mean condition at every point, not merely almost everywhere. Part 6 rests on the duality (1.19)–(1.20), which the book derives from a Young inequality (1.18) printed with the inequality reversed, so the printed route cannot be followed literally.
Distributions are probability measures on , not random variables on a common space; random variables appear only where the book constructs them, each on its own probability space. "For which the integrals exist" is integrability of with respect to both laws. Concavity and convexity are on all of . The quantile function is real-valued; every statement restricts to or assumes finite, so the junk value of an empty infimum never enters. The first moment is a hypothesis exactly where the book uses , or . Suprema are stated as least upper bounds. In part 4 the kernel is a Markov kernel on , the mean condition holds for every and includes integrability of the identity under each .
A trivializing formalization is ruled out: dropping the integrability side condition from the utility classes would make every order compare junk values, and quantifying the orders over all utilities without it would make first-order dominance false for unbounded distributions; neither is done.
Proposition 1.16 is printed with the comparison ; the formal statement reads it as and assumes nonzero means, since the Lorenz curve is a quotient by the mean.
Beyond the paper. One variant is posed beside the faithful statements. [Corrected] Proposition 1.16 (ccd_iff_lorenz_corrected, finding F2) assumes positive instead of nonzero means: for a negative common mean the division reverses the comparison, and , satisfy with , so the faithful Proposition 1.16 is expected to be disproved.
The development needs Mathlib's Bochner integral, push-forward measures, Markov kernels, and convex and concave functions on . The quantile function, the IDF/IQF conjugacy and the quantile coupling are reusable for every later chapter of the book (the average value-at-risk, distortion and deviation functionals). A supporting reference item, the proved tail-integral characterization of the increasing concave order for random variables, may be imported for part 5. Contributions of auxiliary lemmas (the quantile Galois connection, integrability of the quantile function under a first moment, approximation of concave utilities) are welcome.
Bandwidth allocation determines how quickly a network transfers each file, but files also arrive and depart while the network operates. An allocation can be feasible at every instant and still allow the number of unfinished files to grow without an equilibrium. The relevant question is therefore about the interaction of the allocation rule with the changing population of flows. Chapter 8 of Kelly and Yudovina's Stochastic Networks studies this question under a separation between rapid packet-level control and slower file-level changes. The target here is its characterization of stability for weighted alpha-fair allocations.
The distinction matters even in small networks. Capacity assigned to one route can prevent another route from using several resources together. Consequently, unused capacity at individual resources does not by itself identify a stable allocation policy. A stability theorem must address both the network constraints and the stochastic evolution of the population. The chapter contrasts alpha-fair sharing with priority rules that can have a smaller stability region.
A route is a nonempty collection of resources used by a file transfer. There are finitely many routes and resources. The incidence matrix has entry when route uses resource , and zero otherwise. Resource has positive capacity . A state records the number of unfinished files on each route; there is no upper bound on this count.
Files arrive on route as independent Poisson processes of positive intensity . Their sizes are independent exponential random variables with positive parameter , so their mean size is . The offered load is . If each file on route receives rate , its aggregate service allocation is . Births have intensity , and departures have intensity when .
For positive weights and , the weighted alpha-fair allocation maximizes the aggregate objective
subject to and . Active routes receive positive rates; inactive routes have zero aggregate allocation and zero utility contribution. These are the model and optimization rule in Sections 8.1–8.3 of the supplied source.
The first milestone is Exercise 8.3. The per-flow objective is concave on its finite-utility domain, and its coordinate derivative has the common form
The second milestone is Equation (8.5). For a feasible comparison vector positive on active coordinates, the full supporting-utility chain is
The third milestone is Exercise D.2. With the chapter's Lyapunov function and first-order expression , the actual generator satisfies a remainder bound uniform over the entire state space:
The constant is independent of . Under strict subcriticality, this exercise also asks for a strictly negative drift outside a finite exception set and a finite bound inside it.
The goal remains the complete Theorem 8.2:
The source identifies this equilibrium property with positive recurrence. Equality at a resource capacity belongs to the nonpositive-recurrent side of the equivalence. None of the milestones substitutes for that stochastic conclusion.
Theorem 8.2 identifies the stability region using only the offered loads and capacities, for every fixed positive choice of weights and alpha. Those choices affect allocation but do not change the region asserted by the theorem. The result also distinguishes stability from instantaneous feasibility: the conclusion concerns a probability law for an unbounded population over continuous time. This is the result stated in Chapter 8, rather than a new research conjecture.
The formalization reuses published feasibility, utility, concavity, derivative, tangent, and deterministic drift results. Its remaining targets include inactive routes and the stochastic equivalence. The new definition layer supplies a countable transition function and an invariant-distribution predicate usable in subsequent flow-level results. The proposed theorems are proof targets, not completed machine-checked proofs.
The chapter presents a sketch of the stability proof. A finite-time conditional increment is not automatically its first-order approximation, especially when some coordinates are empty. Reallocation also changes service rates while every route remains nonempty; finding F6 records a two-route counterexample to the sketch's explanation of finite-time equality. A negative expression obtained from the optimization problem is therefore insufficient to establish positive recurrence. Exercise D.2 addresses the actual drift and the uniformity needed over unbounded counts.
The necessity sketch also identifies a single-resource reduction with the equal-sharing exercise. For unequal weights, that identification requires additional justification: the reduced allocation need not share capacity equally. This proof gap is recorded with a two-route instance. It does not change the printed theorem or introduce a variant. The separate printed mistakes in Exercises 8.1, 8.2, and 8.10 remain documented findings; those exercises are outside the selected milestones.
Finite index types represent resources and routes, while states are functions into the natural numbers. Parameters are real and positive, and every route uses at least one resource. Zero-count departures are explicitly absent. The utility retains the logarithmic case and both ranges on either side of one. Concavity includes active zero rates when alpha is below one; otherwise that boundary has extended utility minus infinity. Coordinate derivatives are asserted where the active-coordinate derivative exists.
The process is represented through its continuous-time transition function, constructed as a Poisson mixture of powers of a bounded-rate transition matrix. Equilibrium requires invariance for every nonnegative real time and a probability measure on canonical trajectories whose coordinate process realizes all the stationary Markov finite-dimensional distributions. Probability sums use extended nonnegative reals, so divergent mass is not replaced by zero. The rate bound is the explicit quantity
It is a construction parameter, not an approximation constant or a new capacity restriction. No big-O or high-probability assertion is used. In Exercise D.2, the remainder constant may depend on the fixed network and on the chosen positive tolerance, but not on the state; the finite exception set uses total occupancy.
Positive recurrence is not defined as negative drift or rate balance, and neither a stationary distribution nor a drift inequality is assumed in the goal. Further contributions can establish the process properties, the generator estimates, and the recurrence equivalence. The existing published definitions are retained under their original names; other chapters' unpublished modules are not imported.
An accepted call earns revenue but occupies circuits that could serve later calls. In a network, those consequences extend beyond the links used by the original call: a change in blocking on one link changes the traffic reaching other links. Network planning therefore needs a marginal value that accounts for these indirect effects. Chapter 4 of Kelly and Yudovina's Stochastic Networks develops such values for the Erlang fixed-point approximation. The relevant question is how revenue changes when offered traffic or installed capacity changes, with the network allowed to settle to its new fixed point.
The mission concerns this sensitivity calculation. It complements the scalar Erlang formula and fixed-point uniqueness results, which already have published formalizations. It does not claim that the approximation equals the exact stationary performance of the underlying stochastic loss network.
A loss network has finitely many links and routes. Link has a positive integer number of circuits. A call of route requires circuits at link , where the matrix entries are nonnegative integers. Its offered traffic is , and carrying it earns a real value . Every link in the stated system is used by at least one route.
The Erlang fixed point assigns a blocking probability to each link. In the independent-link approximation, the acceptance probability and carried traffic of route are
Write for carried circuit load and for reduced offered load. The defining equations are , where is Erlang's scalar blocking formula. Revenue is .
The capacity derivative requires an additional convention. The scalar Erlang formula is extended by linear interpolation between successive integer capacities, and the network fixed point is then recomputed using that extension. At the original integer capacities, capacity sensitivity means the derivative from the left. Interpolating the final network revenue would define a different function. These conventions are specified on printed page 102 of the supplied source.
The goal is Theorem 4.6, printed page 103. Define the improvement quantity
There is a unique route-surplus vector and link-cost vector satisfying
The goal asserts existence of the derivatives and their values:
Uniqueness concerns all solutions of the local cost equations, independently of whether they also satisfy a derivative identity.
Three source milestones support this target. Exercise 1.8 gives the scalar Erlang traffic derivative. Theorem 3.20 supplies existence and uniqueness of the integer-capacity fixed point. Both are reused as published references. Exercise 4.9 supplies the matrix characterization. With and , it states
The symmetric matrix is positive definite and invertible, and the unique costs are
These are the claims of Exercise 4.9, printed pages 106–107, including both the equivalence and the explicit solution.
An implied cost assigns the marginal revenue effect of capacity to an individual link. A route's surplus compares its direct value with the total implied cost of the circuits it uses. The theorem thus relates local quantities to derivatives of a network-wide objective. As explained in Remark 4.7, the link costs are also shadow prices for capacity. Their interpretation includes the effect on later traffic, rather than just the revenue of the currently admitted call.
The formal contribution is the precise connection between the actual fixed-point revenue function, one-sided capacity sensitivity, and the unique local linear system. The published scalar derivative and fixed-point theorem remain references, not duplicate problems. The new definition layer and matrix characterization provide reusable objects for later formal work on routing and capacity sensitivity. The submitted theorem statements are proof obligations; successful compilation does not supply their proofs.
Differentiating revenue while holding the blocking vector fixed misses the indirect effects that the theorem measures. Blocking is itself an implicit function of all offered traffics and capacities. Moreover, the scalar interpolation has corners at integer capacities, so ordinary two-sided capacity differentiability is not the required statement. The formal obligations include existence of the appropriate derivatives; merely evaluating a total derivative operator would not establish that existence.
The printed proof explicitly treats a – incidence matrix, whereas the surrounding fixed-point model allows arbitrary nonnegative integer circuit requirements. Finding F2 records this proof-scope gap. The goal retains the general integer statement. Exercise 4.9 also requires legitimate denominators and an invertible matrix; these properties must be established from the network data rather than supplied as assumed conclusions.
Links and routes use finite, zero-based index types. Values, traffic, and blocking coordinates are real. The base capacities are positive integers, offered traffic is positive, and each link is used. The last condition states the domain of the printed weighted-average quotient: an isolated link would make its denominator zero. No injectivity or rank condition on the incidence matrix is imposed. Empty link sets are allowed; in that case every route has acceptance one and revenue is linear in offered traffic.
The scalar Erlang formula and integer fixed-point relation reuse the series' published definitions. The new physical fixed-point selector is constructed from the interpolated equations, with a total fallback outside the existence domain. Its definition assumes no differentiability or cost identity. The goal additionally verifies the selected integer-capacity vector against the published fixed-point relation. A formalization that assumes the sensitivity identities, or replaces revenue by an arbitrary function constrained to satisfy them, would trivialize the target and is excluded here.
No asymptotic notation or unspecified constants occur in these targets. Exercise 4.8's marker-route reduction is left as a proof resource rather than a separate milestone. The queueing-cost strict-convexity assertion in Exercise 4.7 is outside this loss-network mission; its counterexample remains recorded as F1. Finding F3 records why the displayed improvement formula cannot simply be extended to noninteger base capacities: at unit load and capacity , a single-link example gives actual capacity derivative but cost formula . No variant item is posed.