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?
In A Model of Leptons (Weinberg, Phys. Rev. Lett. 19, 1264 (1967)) Steven Weinberg proposed that the photon and the intermediate bosons of the weak interaction are gauge fields of a single symmetry group, , and that the visible differences between them — the photon is massless, the weak bosons are heavy, and their couplings differ — come from a spontaneously broken symmetry of the vacuum rather than of the Lagrangian. The Goldstone bosons that such a breaking would normally produce are removed by the gauge fields (the Higgs–Englert–Brout–Guralnik–Hagen–Kibble mechanism). This model became the leptonic sector of the Standard Model of particle physics.
The paper is three pages long and its quantitative content is a short chain of finite-dimensional algebra: after the scalar field is replaced by its vacuum value, the gauge-boson mass terms form a quadratic form whose diagonalization gives the charged boson , the neutral boson and the massless photon, together with formulas for their masses, for the electric charge and for the weak coupling constant. This mission formalizes that chain.
The model has two gauge couplings (for the isospin fields ) and (for the hypercharge field ), and a complex scalar doublet whose vacuum expectation value is with real. Replacing by in the Lagrangian (eq. (4) of the paper) leaves the spin-one mass terms (eq. (7))
At a fixed spacetime point we write the gauge fields as a vector . The mass terms are then for the symmetric mass-squared matrix
A field of definite mass is a linear combination whose coefficient vector satisfies . The paper's candidates are
with masses , , . The rationalized electric charge is , and the weak coupling constant is defined by . The electron gets the mass from its Yukawa coupling . The electric charge in the paper's conventions is , where is the third isospin component and the hypercharge.
The goal theorem states, for :
where are the coefficient vectors of , and, for all and all field values,
so the massless field is the photon and it couples to with strength .
The milestones follow the paper's numbered equations: eq. (7) as a quadratic form; eqs. (8)–(9) ( and ); eqs. (10), (12) ( and ); eqs. (11), (13) (photon massless); the orthonormality of (10)–(11); eq. (15) (the charge); eq. (16) (); ; ; the parameter-free forms of the bounds BeV, , BeV; and the tree-level vacuum condition .
The result itself. These formulas are the tree-level predictions that made the model testable: a massless photon, a charged and a neutral with , and the relations tying , , and to . The existence of the neutral boson (and its neutral currents) was the model's new prediction, later confirmed experimentally.
Formalizing it. The results are classical and fully proved on paper. The mission produces a machine-checked record of the paper's algebra, with every hypothesis stated (for example, that and are not both zero), and a reusable encoding of the electroweak boson mass matrix.
The mathematics is elementary; the difficulty lies in faithfulness. The paper's sign conventions are not fully consistent (substituting the vacuum value into eq. (4) as printed gives in the second mass term, while eq. (7) prints , which is the combination consistent with eq. (10)). The numerical claims (40 BeV, 80 BeV, ) depend on experimental inputs and on rounding. The formalization therefore takes eq. (7) as printed as its starting point and states the bounds in parameter-free form.
WeinbergLeptons_Model, in namespace WeinbergLeptons.In the multi-armed bandit problem a learner repeatedly chooses one of actions and observes only the loss of the action it chose. Two models of the environment dominate the literature. In the stochastic model the losses of each arm are drawn i.i.d. from a fixed distribution, and the optimal pseudo-regret grows like , where is the gap between the mean loss of arm and that of the best arm (Lai and Robbins, 1985). In the adversarial model the losses are arbitrary and the optimal rate is (Audibert and Bubeck, 2010). Algorithms that are near-optimal in both models without knowing which one they face are called best of both worlds.
Timeline:
There are arms and rounds . In round the learner draws an arm from a probability vector in the simplex , the environment fixes losses , and only is observed. The environment may adapt to the past actions and use its own randomization, modelled by a seed drawn once from a probability measure . The pseudo-regret is
with the expectation over the seed and the learner's draws; a minimizing arm is a best arm in hindsight .
α-Tsallis-INF is online mirror descent on the simplex. With , regularization parameters and learning rates , set
The learner keeps importance-weighted loss estimates , their sums , and plays . The potential splits the regret into a stability term and a penalty term .
In the stochastically constrained regime the loss differences have fixed means, , with a unique best arm ( for ). Then and . Write . Theorem 4 uses
With , for every ,
Lemma 17 (Hessian control along a mirror step); Lemma 11, cases 1 and 4 (instantaneous stability); Lemma 20 and Lemma 12, part 2 (penalty); Lemmas 14 and 16 (scalar inequalities for the learning-rate factors); displays (26) and (30) of Appendix D, the stability and penalty bounds under the parameters of Theorem 4.
Lemmas 20 and 12 cover any causal unbiased loss estimator satisfying the bandit feedback assumptions; the other bandit bounds use the importance-weighted estimator.
The theorem shows that the logarithmic stochastic rate is not special to the -Tsallis entropy: for every , tuning the regularizer to the gaps gives pseudo-regret of order in stochastically constrained environments. This places the log-barrier () and entropic () regularizers of earlier algorithms in one family, and isolates the role of asymmetric regularization. Unlike Theorem 1, it needs the gaps to tune , so it is a statement about the reach of the method rather than a practical algorithm.
The result is proved in the paper; no part of it has a machine-checked proof. Formalizing it produces a complete verified analysis of an online-mirror-descent bandit algorithm with time-varying, non-monotone learning rates, including the stability–penalty decomposition, the Hessian control of Lemma 17 and the explicit constant chase of Appendix D. The analysis also checks two points the paper leaves open: the printed bound has where its proof gives , and Appendix D applies Lemma 12, which assumes non-increasing learning rates, to a rate that increases for a few early rounds when is small.
The obvious argument bounds each round's stability by (Lemma 11, case 1) and sums. That bound contains the best arm, whose weight tends to one, so it grows polynomially in and cannot give a logarithmic rate. The arm has to be removed from the stability, which needs a shifted second-order expansion where losses become slightly negative, and that is only controlled once (Lemma 17). The early rounds before must be paid for separately, and the asymmetric and the learning rate interact through constants that must be tracked exactly for the self-bounding step to close.
Arms are Fin K with and the paper's arm is i - 1. Rounds start at 1; an action sequence is h : ℕ → Fin K with h 0 unused. The adversary is the published RegretBandits.Adversarial.Adversary (losses in depending on past actions only) composed with a seed drawn from a probability measure, with losses measurable in the seed. Expectations are explicit: an integral over the seed of a finite sum over action paths weighted by . The algorithm is an argmax predicate on the weight function, never a choice function. is a real supremum over the simplex. Logarithms are natural, and real powers are Real.rpow with nonnegative bases.
The goal takes ; the endpoints , where the paper's learning rate and regularizer are limits, are not stated. The regime "stochastically constrained with a unique best arm" is replaced by the two consequences the proof uses: the self-bounding inequality and . Every such regime satisfies both, so the formal statement is at least as strong as the printed one. The constant in the first term is the one the proof reaches. A trivial formalization is ruled out: the expectation is a genuine probability law, the gaps are tied to the losses through the self-bounding hypothesis, and the weights are determined by the algorithm, so the bound cannot hold vacuously.
A complete development needs the explicit law of a bandit run with an adaptive randomized adversary, unbiasedness of the IW estimator, convex conjugates and Bregman divergences on the simplex, and elementary real analysis for Lemmas 14 and 16. The run-law and the stability–penalty decomposition are reusable for any mirror-descent bandit algorithm. Proofs of any milestone, and of the scalar Lemmas 14 and 16 in particular, are welcome independently.
Runtime monitoring checks a running system against a specification by inspecting its trace of events as it is produced. Policies on data, such as "every published report was approved within the last 10 days" or "each value stored in in reaches out within 5 time units", quantify over data values and constrain the time between events. Metric first-order temporal logic (MFOTL) expresses such policies: it extends first-order logic with past and future temporal operators that carry intervals of allowed time differences.
Basin, Klaedtke, Müller and Zălinescu (J. ACM 62(2), Article 15, 2015) give a monitor for MFOTL properties with bounded. It allows negation and quantification over the infinite domain without restriction, because every relation it manipulates is represented by a finite automaton: the input structures are automatic structures. The paper implements it in the prototype tool MonPoly-Reg (§6). Its correctness rests on Theorem 3.9: the monitor reports exactly the violations of , at every time point.
A signature has finitely many constants and predicates with arities. Formulas are built from and by , , and the temporal operators (previous), (next), (since) and (until), where is a nonempty interval of with . A formula is bounded if every in it has .
A temporal structure assigns to each time point relations and a time stamp ; constants are rigid, , and exceeds every bound. Satisfaction is Definition 2.2; for example holds at if holds at some with and holds at all . For with free variables , the satisfying set is
A domain representation is a regular language over a finite alphabet with a surjection whose equality relation is regular. A relation is regular if the words (the letter-by-letter convolution, padded with ) with form a regular language.
The monitor (Fig. 2) reads one element per loop iteration. It extends each to with auxiliary relations (and , for since and until) for every temporal subformula , built incrementally by the constructions of §3.4 once a list of pending triples says that enough of the future has been read. When is complete it outputs the set with , where is with each top-level temporal subformula replaced by the atom .
For every input satisfying the restrictions of §3.1 and every bounded :
where each output is followed by line 11 setting to the next index. This records counter values reached inside the while loop, including values that may never appear at a loop entry. Part (ii) excludes the vacuous reading of (i).
Theorem 3.9 makes a sound and complete monitor for the safety fragment , bounded: every violation at every time point is reported, nothing else is, and every output is a finitely represented (regular) set even though it may be infinite. It covers unrestricted negation and quantification, which finite-relation monitors (§4 of the paper) cannot handle. The incremental constructions of §3.4 are the template reused by later MFOTL monitors.
The paper gives a mathematical proof of its monitor's correctness. This mission asks for a Lean proof that checks the MFOTL semantics, automatic relations over , and the correctness of this particular monitor, including the until construction whose printed version is defective (see Formalization scope).
Two parts are hard. The regularity claims need the fundamental property of automatic structures: first-order definable relations are regular, which requires closure of padded convolution languages under Boolean operations, cylindrification, permutation of tracks and projection, the last with removal of trailing padding. The arithmetic constraints of the since and until constructions additionally need successor and offset relations definable from .
The scheduling argument is the other part. Correctness of a build at requires that every input relation, at time points up to for until, was built before and not discarded since. Following only the syntax of does not settle this: a needed relation for a subformula at a later time point may be built in the same iteration as 's.
The domain is , as §3.1 assumes. Relations are sets of lists of natural numbers, ordered by the sorted free variables. Interval upper bounds are in ; intervals carry the proof that they are nonempty. The representation is a single parameter shared by the hypothesis "every is regular" and the regularity claims of the conclusions; it is never chosen existentially. The binary predicate interpreted as is a hypothesis.
Two hypotheses on besides boundedness are the paper's own "without loss of generality" assumptions: each temporal subformula occurs once in (§3.6), and the direct subformulas of each , subformula have the same free variables (§3.4; achieved by padding with , as in §3.5). No other restriction is placed on .
The printed until construction (§3.4.4) is repaired: the guard of is " for all ", since the printed guard empties in the paper's own example of §3.5; keeps only tuples with , since otherwise a -witness at time point survives to time point when ; and time-stamp equations are encoded additively. Lemma 3.8(i) reads and adds . "Effectively computable" in Theorem 3.9(i) is not formalized. Part (ii) uses the output at index as the record of the line-11 increment to ; for , the counter is initialized by line 2. Loop-entry states alone can skip counter values reached within one iteration.
The monitor is a state machine whose builds and outputs are computed only from its store of relations; it never consults the satisfaction relation or satisfying sets. A formalization in which line 7 reads the semantics would turn Theorem 3.9(i) into a restatement of Lemma 3.4, and is ruled out. A build whose input is missing stores nothing, so a monitor that silently fails would violate (ii).
Contributions welcome: the theory of automatic relations (reusable beyond this mission), the semantic halves of Lemmas 3.4–3.8, and the scheduling invariants.
A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension under a finite exponential-moment condition Bates and Chatterjee, 2021.
The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.
Fix . A path starts at the origin in and makes one of its nearest-neighbor moves at each integer time. The environment consists of independent, identically distributed real random variables with common law . The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature determines the weight of a path of length :
The endpoint mass function is the sum of weights of paths ending at , divided by the sum of all path weights. Thus is a probability mass function on . For , the -atoms are the sites , and is their total mass. The strict inequality matters at a threshold equal to an atom mass.
Write for , with , and . The standing condition is that this exponential moment is finite for every . The paper's Theorem A characterizes the high-temperature phase by and the low-temperature phase by Bates and Chatterjee, 2021, pp. 4–5.
The goal is both clauses of Theorem 1.1. For every positive deterministic sequence , low temperature gives
At high temperature there exists a positive deterministic sequence for which the same average converges almost surely to . The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.
The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:
The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.
A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.
The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of . Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.
Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the choices per step, and the normalization of are explicit. An environment is a measurable independent family on a probability space with common law . The unused time-zero row comes from indexing cells by ; only rows with index at least one enter the polymer. The moment condition includes the full interval , and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on , , and rather than on an arbitrary realization.
Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient . Finite partial isometries carry the degree penalty through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward the zero measure, which is not the paper's object either. The infimum is taken over the set itself, never as a real infimum whose empty inner range defaults to . The intermediate results in §§3–4 and Lemma 5.1 use the standing range. Theorems 1.1 and 5.2 explicitly include . Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.
Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when ). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.
A set-valued predictor returns, for each input , a set of plausible responses rather than a single guess. Such sets are used wherever a model's output feeds a decision with asymmetric costs: a medical classifier that lists every diagnosis it cannot rule out, a segmentation model that marks every pixel that may belong to a tumour, a protein-structure predictor that reports a range of distances. Bates, Angelopoulos, Lei, Malik and Jordan, Distribution-Free, Risk-Controlling Prediction Sets (J. ACM 68(6), 2021), calibrate a nested family of such predictors so that a chosen loss is controlled with high probability, without distributional assumptions.
Calibration says nothing about which family to calibrate. Any nested family can be made risk-controlling; families differ in how large their sets are, and large sets are uninformative. §4 of the paper asks which family is best in the population: which predictor achieves a given risk with the smallest expected set size. For a weighted miscoverage loss (Theorem 7, §4.2) the answer thresholds a weighted conditional density, in the spirit of the optimality results of Sadinle, Lei and Wasserman (2019) for classification. Theorem 8 (§4.3) extends the answer to every loss of integral form. This mission formalizes Theorem 8.
Let take values in with law , marginal , and conditional law of given . Prediction sets are subsets of a measurable space (in the paper's examples ). A set-valued predictor is a map .
Fix a finite measure on and a nonnegative cost ; is the cost of leaving out of the prediction set when the true response is . The loss of a set is the total cost of what it leaves out,
and the risk of a predictor is (§2.1). Larger sets have smaller loss. The conditional expected cost of omitting at is
and for the threshold predictor of display (11) is
It includes exactly the points whose omission is expected to cost at least . The size of a set is its -measure, , and the expected size of a predictor is .
In Lean: setLoss μ ℓ y S, risk P μ ℓ T, condLoss κ ℓ x z, thresholdSet κ ℓ lam x and expSize P μ T in the namespace RiskControl.Optimal.
For every and every set-valued predictor (with measurable graph),
No constant is involved; the statement is uniform over , , and .
The result. Theorem 8 identifies the population-optimal shape of a set-valued predictor for every loss that charges for omitted points through a nonnegative cost and a finite measure. It justifies building nested families by thresholding an estimate of the conditional expected cost: if the estimate were exact, no other predictor with the same or smaller risk could have smaller sets on average. It contains the weighted-miscoverage case (Theorem 7) when is discrete and is counting measure, and it covers losses for which no such special case exists, such as costs that depend on the distance between and .
Formalizing it. The proof on p. 27 is a chain of eight displays. A machine-checked version settles the measure-theoretic points the chain passes over: the conditional expectation inside an integral over a random set, the cancellation of possibly infinite terms, and the range of . To our knowledge no formal proof of Theorem 8 or of the Neyman–Pearson-type optimality results it generalizes for set predictors exists in Lean or Mathlib.
The natural reading of the proof subtracts the quantity from both sides of the risk comparison to pass from complements to sets. Nothing in the setting makes this quantity finite, so that step is not valid as written, and a proof that follows the displays literally breaks there. The theorem itself does not need finiteness of , and no such hypothesis is in scope.
The other obstacle is measure-theoretic bookkeeping. The conditional expectation is indexed by a point of a second space, and must be a jointly measurable function of before it can be integrated over the random set ; here it is given by a regular conditional distribution, and every integral over needs the measurability of the graph of .
The development needs Mathlib's composition of a measure with a kernel, Tonelli's theorem for kernels and lower integrals over sections of a measurable set. Lemmas about expected -sizes of random sets (milestone 4) and about moving a kernel integral inside a set integral (milestone 1) are reusable beyond this mission. Proofs of the milestones, and of the goal by other routes, are welcome.
A trained classifier or regressor returns a point prediction, but many uses of machine learning need a prediction set: a set of plausible labels together with a guarantee about how often, or how badly, it misses the truth. Medical imaging, protein structure prediction and multi-label classification are examples where a user wants a set whose expected loss is bounded, not just a best guess. Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 68(6), 2021) give a procedure that wraps any black-box predictor and returns sets whose risk is controlled, with no assumption on the data distribution beyond i.i.d. calibration data.
The procedure generalizes split conformal prediction (Vovk, Gammerman and Shafer, 2005) and the tolerance regions of Wilks (1941), which control only the probability of missing the label, to an arbitrary monotone loss on sets (false-negative rate, coverage of a segmentation mask, a hierarchical loss). This mission formalizes its central guarantee, Theorem 1 (p. 5), together with the abstract form Theorem A.1 (p. 26) from which the paper derives it.
Let be a random pair in with law , and let be a set of labels. A set-valued predictor is a map . The paper considers a family indexed by a closed set that is nested:
A loss on sets is required to decrease as the set grows:
The risk of is , and the section assumes some with .
A risk-controlling prediction set at levels (Definition 1, p. 2) is a data-dependent predictor with with probability at least .
Given an i.i.d. calibration sample , a pointwise upper confidence bound is a function with
UCB calibration selects
In Lean, the risk is RiskControl.UCB.risk P L T lam, the calibration set of (4) for one realization r of is calSet Λ r α, and is lambdaHat Λ r α.
In the setting above, if (3) holds for every and is continuous on , then
Nothing is assumed of beyond (3); and are arbitrary reals.
Theorem 1 turns a confidence bound for one fixed parameter into a guarantee for a parameter chosen from the data. No uniform convergence over is needed, so any concentration inequality for a mean (Hoeffding, Bentkus, the betting bound of Waudby-Smith and Ramdas) yields a calibration procedure immediately; the paper's Theorems 2–5 and 9–10 are of exactly this form, and the later Learn-then-Test and conformal risk control frameworks build on the same template.
The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked version of an argument whose printed form has a gap. The printed proof of Theorem A.1 introduces and asserts "by continuity", which is false when is not an interval. Finite grids, the usual choice of in practice, are not intervals. The theorem remains true, and milestones 2 and 3 state the corrected steps. No formalization of risk-controlling prediction sets or of conformal prediction is known to exist in Lean or on this platform.
The obvious argument applies the confidence bound at ; that fails because depends on the data, so (3) says nothing at . The proof must find one deterministic point at which a failure of calibration forces a failure of (3). The paper's choice works only when attains the value on ; on with , , and the exact bound , the event has probability one, so the printed last step does not bound anything. The second difficulty is boundary behaviour: may contain , the infimum in (4) may be over an empty set, and the calibration set need not contain its own infimum.
EReal (the extended reals with the order topology); is only compared, never added. Continuity of is in the subspace topology of .Set 𝒵, i.e. (the paper uses for most of its examples).WassersteinDRO.Duality.nominalRisk, a Bochner integral. Because a non-integrable integrand integrates to in Lean, Theorem 1 assumes is -integrable for every .Fin n → 𝒳 × 𝒴 under the product measure . is an arbitrary real function of the sample and of ; an infinite bound is represented by any value .EReal, so as on the page. Since need not belong to , the failure event is "the set in (4) is nonempty and "; when the set is nonempty, . When it is empty the procedure certifies nothing, and the natural output is , of risk .Needed infrastructure is small: closed subsets of EReal and their infima and suprema (IsClosed.sInf_mem, IsClosed.sSup_mem), continuity within a set, monotonicity of the Bochner integral, and monotonicity of outer measure. Proofs of the milestones are welcome individually; the deterministic milestones 2 and 3 are reusable for every UCB-calibration theorem of the paper.
Two classical extremal results bound the number of edges of an -vertex graph under a single restriction. Turán's theorem (1941) says that a graph with no clique on vertices has at most edges, the edge count of the balanced complete -partite graph. The Erdős–Gallai theorem (1959) gives the maximum number of edges of an -vertex graph whose largest matching has at most edges. N. Alon and P. Frankl, Turán graphs with bounded matching number (arXiv:2210.15076v1; J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002), combine the two restrictions. Their Theorem 1.1 determines the maximum for the clique constraint and every (mission 1 of this series). Their Proposition 3.1, the goal here, treats a whole class of forbidden graphs, the color-critical ones, when is large in terms of the forbidden graph and is large in terms of .
Color-critical graphs are the natural class for exact Turán results: by a theorem of M. Simonovits (1968), for a color-critical of chromatic number the Turán graph is extremal for -freeness once is large. Proposition 3.1 is the analogue of Simonovits' theorem under a matching constraint.
All graphs are finite and simple. For a graph , a matching is a set of pairwise disjoint edges, and the matching number is the largest size of a matching. For a graph , is -free if it contains no subgraph (not necessarily induced) isomorphic to . The chromatic number is the least number of colors in a proper vertex coloring. is color-critical if it has an edge with ; examples are complete graphs and odd cycles.
The Turán graph is the complete -partite graph on vertices with classes of sizes as equal as possible; is its number of edges. For and , the graph is the complete -partite graph on vertices consisting of classes of sizes as equal as possible whose total size is , and one further class of size . Its number of edges is .
In the Lean development, vertices of are Fin n; the shared objects of this series live in TuranMatching.Clique.Setting: is matchingNumber, is turanNum n k (Mathlib's turanGraph), is bigGraph n k s, is gNum n k s, color-criticality is IsColorCritical, and the set of vertices of degree exceeding is highDeg G s.
There is such that for every color-critical with there is with: for all and ,
The maximum is stated as an upper bound for every admissible together with an admissible graph attaining . The thresholds and are left existential, as on the page.
The proposition settles, for every color-critical and large parameters, the Turán problem with a bounded matching number, and identifies the extremal graph , which does not depend on beyond its chromatic number. For it agrees with the large- case of Theorem 1.1 of the same paper. The structural steps (few high-degree vertices, the independence of the low-degree side) are reusable in other degree-based arguments under matching constraints.
The result is proved in the paper; none of it is formalized. The mission produces, besides the goal, two classical theorems absent from Mathlib in the forms needed here: the matching-number consequence of Vizing's theorem (milestone 3) and Simonovits' exact Turán theorem for color-critical graphs (milestone 7). Milestone 7 is a cited classical theorem, not a result of Alon and Frankl; it is posed because the proof rests on it. Mathlib currently has Turán's theorem for cliques and the Erdős–Stone–Simonovits density theorem, but not the exact result for color-critical graphs.
Milestones 1, 2, 4, 5, 6 and 8 are elementary counting arguments, though each requires building matchings or explicit counts in Lean. Milestone 8 contains the paper's "easy to see" isomorphism, which in Lean is an identity between two edge counts, with .
Milestone 3 needs Vizing's edge-coloring theorem (a graph of maximum degree is properly -edge-colorable). A naive greedy edge coloring gives only colors, which bounds the edge count by about and is too weak for the comparison in milestones 4 and 5.
Milestone 7 is the hardest item. The density version (Erdős–Stone–Simonovits) gives edges only; the exact bound for color-critical requires Simonovits' stability method, an argument that an almost-extremal -free graph is close to followed by a cleaning step that uses the critical edge.
Graphs are SimpleGraph (Fin n) with decidable adjacency; edges are counted by #G.edgeFinset. The matching number is the supremum, in , of the edge counts of matching subgraphs; the set is nonempty and bounded, so this is the true maximum and not a junk value. is defined as the edge count of the graph , not by a closed formula. Chromatic numbers live in (Mathlib's chromaticNumber), both in the definition of color-critical and in the hypothesis . -freeness is Mathlib's SimpleGraph.Free (no subgraph copy). The vertex type of is any finite type in the lowest universe.
Conventions committed to:
A formalization that states only the upper bound, without an attaining graph, or that places the existential after is fixed as a constant independent of , or that defines or so that they take junk values, is a different and weaker statement and is ruled out.
Infrastructure that would be reusable beyond this mission: a matching-number API on Mathlib's Subgraph.IsMatching (in particular for and the behaviour under induced subgraphs); Vizing's theorem; and Simonovits' theorem. Contributions of any of these, and of partial results toward milestone 7 (for example the case ), are welcome.
Many allocation problems divide indivisible goods among agents who are entitled to different shares but cannot pay with real money: course seats among students, shifts among workers, inherited items among heirs. A standard mechanism gives each agent a budget of artificial currency and lets a market run. When budgets are equal this is the competitive equilibrium from equal incomes (CEEI) of Varian (1974), the basis of the course-allocation mechanism of Budish (2011). With indivisible items, however, an equilibrium can fail to exist: one item and two agents with equal budgets already admit none, because whoever does not get the item could afford it at any price the owner can pay.
Babaioff, Nisan and Talgam-Cohen (arXiv 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) ask whether this failure is robust or a knife edge, and answer for two agents with additive preferences: an arbitrarily small, strict inequality between the budgets restores existence. Budish's approximate CEEI perturbs budgets randomly for the same reason; this mission formalizes the exact two-agent result.
A discrete Fisher market has a set of indivisible items and two agents. Agent has a valuation assigning a real value to every bundle , and a budget . Valuations are additive (), normalized (), non-negative, monotone ( when ) and strict (different bundles have different values). Budgets are normalized, ; money has no value to the agents.
An allocation is a partition of all items between the agents. Item prices give bundle prices . Agent demands if and for every bundle with . A competitive equilibrium (CE) is a pair in which each agent demands her own bundle. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent.
Agent 's budget-proportional share is (her budget times ). Her truncated share is the best value she gets in a PO allocation that gives her at most that share:
The Lean development uses the same names: bundle σ i for , price, IsCE, IsPO, IsStandardValuation, GetsTruncatedShare.
For every two-agent additive market there is such that every budget pair with
admits a CE in which for both agents. The goal fixes no value of ; it asserts only that one exists for each market.
Two companion statements are drafted without being milestones: Theorem 4.4 (second welfare theorem) and Theorem 5.2 (a budget-proportional allocation implies a CE).
The result. Theorem 7.1 shows that the non-existence of CEEI with indivisible goods is a measure-zero phenomenon for two additive agents: equal budgets are the only bad point near equality, and the equilibrium obtained is also fair in the truncated-share sense. It justifies tie-breaking by tiny budget differences in practice. It is the two-agent base case of the paper's main open question (§9.1, p. 20), whether generic almost-equal budgets guarantee a CE for more than two agents; the paper also leaves open two agents with arbitrary generic budgets and non-identical preferences (p. 21). For arbitrary, not almost-equal, budgets, Segal-Halevi (AAMAS 2018) shows that genericity does not guarantee existence for four additive agents.
Formalizing it. No machine-checked proof of any result of this paper is known. The paper's own argument for one case of the goal is incomplete: in Case 2(b) of the proof of Theorem 7.1 (p. 19) it asserts that the two candidate allocations are mirror images of each other and that the rectangles are empty. Both claims fail on an explicit three-item market. Theorem 7.1 itself held in every one of 6000 markets checked numerically during planning, including that one, where a CE with truncated shares exists at prices proportional to one agent's valuation. A formal proof therefore has to supply an argument the paper does not contain; the two false steps are not posed as milestones.
The milestones 1–5 are finite combinatorics on the Pareto frontier with sign bookkeeping. The difficulty sits in Case 2(b) of the goal: every allocation gives one agent more than and the other less. The natural route, invoking Lemma 6.3, needs some to be empty, and in that case both can be non-empty. Lemma 6.3 does not cover it, and the paper's symmetry argument cannot be repaired by choosing smaller, since in the counterexample the two candidate allocations stay the same for every small . A complete proof must show directly that one of the two "as fair as possible" allocations is supported by suitable prices.
Items are Fin m and agents Fin 2; the paper's agents 1, 2 are indices 0, 1, so "" reads b 1 < b 0. An allocation is a map σ : Fin m → Fin 2, which builds in that every item is allocated exactly once. All quantities are real numbers. Demand quantifies over every bundle, with strict inequality . Prices are non-negative by definition of a CE. The truncated share is a maximum over PO allocations only.
Two conventions are disclosed restrictions or additions:
In the goal is chosen after the valuations and before the budgets. A formalization in which depends on the budgets, demand ranges over a restricted family of bundles, allocations need not allocate every item, prices may be negative, or the truncated share is a maximum over all allocations, would be a different and in several cases trivial statement; all of these are ruled out.
The definitions file GenericBudgets.AlmostEqual.Setting holds the market, CE, PO, the fairness notions, combination pricing, Condition (1), and , and is reusable for any two-agent indivisible-goods market with budgets. Proofs of the milestones, a repaired argument for Case 2(b), and general -agent versions of the CE and PO infrastructure are welcome.
Trained neural networks are increasingly embedded inside optimization models: to verify that a classifier is robust to small input perturbations, to optimize over a learned surrogate of an expensive system, or to choose decisions whose outcome is predicted by a network. When the network uses rectified linear units (ReLU), each neuron is piecewise linear, and the whole network can be written exactly as a mixed-integer program (MIP) with one binary variable per neuron. How fast a branch-and-bound solver closes such a model depends on how tight the linear-programming relaxation of each neuron's formulation is.
Anderson, Huchette, Tjandraatmadja and Vielma (arXiv:1811.08359v2, the IPCO 2019 extended abstract) gave a formulation (6) of a single ReLU neuron over a box that uses only the original variables and one binary variable, and is ideal: its LP relaxation has integral extreme points (Proposition 1, p. 6). The price is an exponential family of inequalities (6b), one for every subset of the support of . The present mission formalizes their Proposition 2: each of these inequalities is facet-defining, so no member of the family can be dropped without weakening the relaxation. A longer journal version of the work, with different numbering, appeared later (arXiv:1811.01988); this mission follows the extended abstract.
Fix , a weight vector , a bias , and bounds with for every (§1.3, p. 4). Write and . The sign-adjusted bounds are
so that and are the maximum and minimum of over . The support is . Strict activity means : the neuron is neither always off nor always on over the box. The paper assumes it throughout (§1.3).
Formulation (6) (p. 6) consists of the points with
In Lean, form6 w b L U is this set, and relax6 w b L U is its LP relaxation ( in place of ). The right-hand side of (6b) for the subset is rhs6b w b L U I x z.
An inequality is facet-defining for a set when it holds on , its face is nonempty, and , the dimension of a set being that of its affine hull. The paper uses this standard notion without defining it.
Under and strict activity, for every , the inequality (6b) for is facet-defining for
The page states the result as "Each inequality in (6b) is facet-defining", and adds right after the proof line: "We require the assumption of strict activity above, as introduced in Section 1.3."
The result. Proposition 1 shows that (6) is ideal; Proposition 2 shows it cannot be made smaller: removing any single inequality (6b) produces a strictly weaker relaxation. Since the family has members, this is what justifies the paper's practical recommendation to start from the big- formulation and separate inequalities of (6b) on demand (Proposition 3, p. 7) rather than to search for a smaller ideal description in the same variables. The facet structure also gives the geometric picture the paper describes after Proposition 2: each facet is the convex combination of an -dimensional face at and an -dimensional face at .
Formalizing it. The result is proved in the paper, in a half-page appendix; it has not been machine-checked. The formalization adds two things. First, the proof is written for "without loss of generality by appropriately interchanging and "; the Lean statements are for every sign pattern, including zero weights. Second, the appendix exhibits affinely independent points on the face, which bounds the face dimension from below; the statement that the face has dimension exactly one less than the polyhedron also needs the polyhedron to be full-dimensional and the face to lie in a proper hyperplane, steps the extended abstract leaves implicit and a complete proof must supply.
The arithmetic in each step is elementary. The work lies in the bookkeeping: choosing a single that keeps every perturbed point inside the box and on the correct side of (this is exactly where strict activity enters), checking the perturbed points against all inequalities of (6b) and not only the one for , and turning a row-reduction argument on an matrix into a statement about AffineIndependent and finrank of a vectorSpan in Lean. The natural shortcut, proving only that affinely independent tight points exist, is not Proposition 2: it says nothing about the dimension of the polyhedron itself.
Inputs are Fin η → ℝ (indices for the paper's ); a point is p : (Fin η → ℝ) × ℝ × ℝ with p.1 = x, p.2.1 = y, p.2.2 = z. are given by their closed forms and . In (6b), "" ranges over all indices outside , zero weights included; ranges over subsets of , as on the page.
Every goal and milestone keeps the standing assumptions of §1.3, for all and strict activity, except the affine-independence milestone, which holds without them and is stated without them (a stronger statement). No other hypothesis is added. Strict activity excludes , so no nonemptiness assumption on the index set is needed.
IsFacetDefining P g is the standard notion: validity, a nonempty face, and with dimensions the finrank of the vectorSpan. The equation is written with on the left so that no natural-number subtraction can make the empty set or a point a facet. The polyhedron is the convex hull of the points of (6), not the set form6 itself (which is not convex, since ); by Proposition 1 it equals the LP relaxation relax6, but the statement does not depend on that.
The shared objects of this paper (the ReLU graph, , , , support, strict activity, formulation (6), ideality) come from the shared definitions module ReluMIP.Ideal.Setting, common to the companion mission on Proposition 1; this mission's own definitions module adds form6, IsFacetDefining, the sign inward, and the indexed family facetPts of the points. The facet notion and the affine-independence argument are reusable for other facet proofs of polyhedra in product spaces. Proofs of the milestones, of the goal, and of the full-dimensionality step are all welcome.
A lower bound on the Ricci curvature of a Riemannian manifold and an upper bound on its dimension can be expressed without coordinates in two ways. The Bakry–Émery condition is a property of the heat semigroup and its generator: the iterated carré du champ dominates (Bakry–Émery 1985). The Riemannian curvature-dimension conditions and are properties of a metric measure space, defined through optimal transport (Ambrosio–Gigli–Savaré 2014). A basic test for any notion of "Ricci curvature at least , dimension at most " is its behaviour under products: on a product of manifolds, Ricci curvature bounds combine and dimensions add.
The paper of Ambrosio, Gigli and Savaré (arXiv:1209.5786) proves that and coincide on a natural class of Dirichlet-form spaces, and draws from it, in its §5.1, two tensorization results. The first (Theorem 5.1) is the stability of under products. This had been proved in Ambrosio–Gigli–Savaré 2014 only under a nonbranching assumption on the factors; the equivalence removes that assumption. The second (Theorem 5.2) is the dimensional statement: the product of two Riemannian Energy measure spaces satisfying and satisfies , the bound on the dimension of the product that the smooth case predicts.
Let be a complete separable metric space with a Borel measure . A Dirichlet form is a quadratic, -lower semicontinuous, Markovian functional with dense domain . Its generator is defined by for all , and its heat flow solves . The carré du champ is the density of . For , is the weak form (2.33) of , written through the functional .
The intrinsic distance is . An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a space whose metric is , with full-support measure and an exhausting function; a Riemannian Energy measure space (Definition 3.16) is in addition upper regular, and every with has a continuous version. An space (Definition 3.1) is a length metric measure space with the growth bounds (MD.b) and (MD.exp) on which the relative entropy has an gradient flow in .
The product (5.1) of and is with
and the Cartesian Dirichlet form (5.2) is
where and .
If and are Riemannian Energy measure spaces satisfying (MD.exp), and , then
In the parametrization the product satisfies with .
implies . 2. Theorem 5.1, p. 60: the product of two spaces is . 3. The elementary inequality of p. 62: for positive and nonnegative . 4. Lemma 5.3, p. 62: under the fibrewise regularity (5.9), for the RCD factors and their Cheeger forms fixed in §5.1.
Theorem 5.1 shows that is closed under products with no nonbranching condition on the factors, the hypothesis under which Ambrosio–Gigli–Savaré 2014 had obtained it. Theorem 5.2 gives the dimensional version for Dirichlet-form spaces, : a product of spaces of finite dimension has finite dimension, with the bound of the smooth case, while the condition alone loses all dimensional information.
Both results are proved in the paper; none of them, nor the objects they are stated for, has a machine-checked proof. The mission produces a Lean statement of the Cartesian Dirichlet form and of the product structure, the statements of the two tensorization theorems, and the characterization of that drives Theorem 5.1. A formal proof would also check the measure-theoretic steps that the paper takes for granted: the measurability of , the Fubini arguments of Lemma 5.3, and the identification of the domain of the Cartesian form (cited from [Ambrosio–Gigli–Savaré 2014], Theorem 6.18).
The obvious argument works fibre by fibre: apply to each section and to each , and add. This fails as stated, because on does not act on the sections separately: is an average over of the semigroup of applied to , weighted by the heat kernel of , so fibrewise gradient and Laplacian bounds have to be transported through this average. For Theorem 5.2 a second step is not fibrewise at all: before any dimensional estimate, the product has to be shown to be a Riemannian Energy measure space whose intrinsic distance is the product distance, which in the paper goes through Theorem 5.1 and hence through the equivalence of Theorem 4.17.
Functions on are X → ℝ, and membership is MemLp f 2 m; every object is invariant under -a.e. equality. Dirichlet forms take values in and are off . Heat flows are passed as functions pinned by the predicate IsHeatSemigroup. is a predicate on a density. is parametrized by ; is when either factor has . The product is WithLp 2 (X × Y), whose metric is the distance (5.1); the plain type X × Y would carry the max-metric. The second term of (5.2) uses , correcting the printed . Factors are σ-finite.
Theorem 5.2 assumes (MD.exp) for both factors: its proof invokes Theorem 5.1, whose factors must be , which a Riemannian Energy measure space with is only under (MD.exp). In Corollary 4.18, the minimal weak gradient is written as , the identity that (QCh) asserts. Lemma 5.3 carries the RCD and Cheeger-form assumptions established at the opening of §5.1. The elementary inequality retains the printed ; applying it to signed Laplacians requires its all-real extension.
The goal is not met by stating on the product with : that is , a strictly weaker claim; nor by defining the product form through the Cheeger energy of instead of (5.2).
A complete development needs the Cartesian form's domain theorem, a pointwise version of the heat semigroups, Theorem 4.17 of the paper and the converse from [Ambrosio–Gigli–Savaré 2014]. The product layer (sections, Cartesian form, Lemma 5.3) is reusable for any tensorization argument on Dirichlet forms. Proofs of the elementary inequality and of Lemma 5.3 are the natural first contributions.
Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.
Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.
Two buyers source from three suppliers: from its independent supplier , and both from the common supplier . Each supplier is compliant with probability . A non-compliant supplier that passes an audit of effort (probability ) is exposed in public with probability . An independent supplier audited with effort therefore causes damage with probability . The three suppliers offend independently.
If buyer has exposed suppliers, its demand intercept falls from to (by once, however many offend). Each exposed supplier also raises its unit input cost from to . The buyers then play a Cournot game with differentiated products (substitution ). Buyer 's equilibrium profit is , where
The aggregate ex post profit is . Auditing a supplier with effort costs .
Unilateral auditing. Each buyer audits at most one of his two suppliers. is buyer 's expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.
Joint auditing. The coalition chooses efforts on , auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With the buyers' expected profits excluding audit costs, the coalition's profit is
The difference of the buyers' profits is . The cost shares are (eq. (3)). The analysis assumes the scenario
There are thresholds such that, for every , an optimal joint plan
The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying , each buyer earns at least his profit in a symmetric unilateral equilibrium.
The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: beats one independent supplier, and beats no audit for . Lemma OA10: with beats with . Lemma OA11: with beats alone for . The fair shares (3). The case analysis with and . Stability.
The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ( exactly when ). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.
The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).
All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds , are differences of maxima, so the case analysis has to handle ties and the boundary with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.
Params holds with , , , , , and the three positivity conditions of p. 8. Every statement adds (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: is a label, not a damage of .sSup over and . At the profit is a polynomial, so these suprema are attained.Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.
Neutrinos are the only Standard Model fermions whose masses, mixing and electromagnetic properties are still largely unknown. The review of Giunti and Studenikin (Rev. Mod. Phys. 87, 531 (2015)) collects the theory of neutrino masses and mixing, the general structure of neutrino electromagnetic form factors for Dirac and Majorana neutrinos, and the dynamics of neutrino spin and flavor in electromagnetic fields and matter. Most of the review is phenomenology (experimental bounds, astrophysical estimates), but a core of it consists of exact mathematical statements about finite-dimensional unitary matrices, Hermitian matrices and two-level linear Schrödinger equations. Those exact statements are what this mission targets.
Timeline of the results formalized here:
A mixing matrix is a unitary complex matrix whose rows are labelled by flavors and whose columns are labelled by massive states with masses . For a neutrino of energy that has travelled a distance , the plane-wave transition probability (Eqs. (2.35)–(2.36)) is
In the Lean development this is oscProb U m L E l l'. The standard parametrization of Eq. (2.27) and the Majorana phase matrix of Eq. (2.28) are diracMixing and majoranaPhases; the two-neutrino rotation matrix of Eq. (2.38) is twoFlavorMixing.
In matter of constant electron density, the – amplitudes obey with the effective Hamiltonian of Eq. (2.46) (mswHamiltonian), built from the vacuum squared-mass difference , the mixing angle and the charged-current potential with . The effective squared-mass difference of Eq. (2.53) and effective angle of Eq. (2.54) are mswDeltaM2 and mswMixingAngle.
Electromagnetic form-factor matrices (: charge, magnetic, electric, anapole) are Hermitian complex matrices in the space of massive neutrinos; for Majorana neutrinos they are in addition antisymmetric () or symmetric (), Eqs. (3.66)–(3.68).
Finally, the helicity amplitudes of an ultrarelativistic Dirac neutrino with magnetic moment in a transverse field and matter potential obey (Eqs. (6.23), (6.28); spinFlavorHamiltonian), with energy splitting (Eq. (6.31); spinFlavorEnergySplitting).
For every unitary , all masses , every and every ,
with . The number of massive states is left free (the paper uses , and with sterile neutrinos, Sec. II.F).
Eq. (2.37) is the formula used in essentially every analysis of oscillation data; its two-neutrino specializations (2.39)–(2.40) and the matter formula (2.57) are the standard fitting functions for reactor, accelerator and solar experiments. The Majorana constraints (3.67)–(3.70) are the precise statement behind the claim that a measured diagonal magnetic moment would rule out Majorana neutrinos (under CPT). The spin-precession formulas (6.27) and (6.34) underlie the astrophysical bounds on neutrino magnetic moments.
All targets are established results with textbook derivations; none is open. What the mission adds is machine-checked versions with every convention (sign of the phase, ordering , ranges of angles, boundary conditions of the Schrödinger equation) fixed explicitly. Related vacuum-oscillation statements from a different source already exist on the platform under the LipariNeutrino namespace; the present drafts are self-contained and follow this paper's notation and equation numbering.
The algebraic targets require careful bookkeeping of complex conjugation and of the unitarity relations inside double sums over . The dynamical targets (2.57), (6.27), (6.34) are statements about every solution of a linear ODE with a given initial value, so a solution in closed form is not enough: uniqueness of solutions of the (for (6.27), non-autonomous) linear system must also be established in Lean.
Fin n; two-neutrino indices 0,1 stand for , or .Matrix.unitaryGroup.HasDerivAt φ (-(I • H.mulVec (φ x))) x for all real , i.e. , with initial value .Useful reusable infrastructure: uniqueness for linear ODEs in , closed-form exponentials of real symmetric matrices, and algebraic lemmas for unitary matrices.
C. Baumgarten's essay How to (Un-) Quantum Mechanics (arXiv:1810.06981, v2 2025) argues that much of the mathematical formalism usually presented as specifically "quantum" — Heisenberg's equation of motion, commutators, eigenvalue problems, the real Pauli and Dirac algebras — already follows from classical linear Hamiltonian mechanics on an abstract phase space. The physical and philosophical claims of the paper are outside the scope of a formalization, but its argument rests on a compact chain of linear-algebra facts stated in Sections IV–VI (pp. 13–20). This mission formalizes exactly that chain, so that the mathematical part of the argument can be checked independently of its interpretation.
Fix a number of degrees of freedom. A phase-space vector is . The symplectic unit matrix is the Kronecker product
A real matrix is Hamiltonian if it equals with symmetric, skew-Hamiltonian if it equals with skew-symmetric, and symplectic if .
Linear Hamiltonian motion is with Hamiltonian (the paper's Eq. 35, coming from the quadratic Hamiltonian ). A matrix of second moments (in the paper an average ) then evolves by
and the autocorrelation matrix is .
The goal theorem combines the conclusions drawn on pp. 16–17: for Hamiltonian and a symmetric solution of Eq. (40), the autocorrelation matrix satisfies, for every time ,
where is the characteristic polynomial: "the eigenvalues are constants of motion" (after Eq. 51) together with Eq. (48).
The milestones follow the paper's own steps, in order:
The result itself. Each statement is classical linear algebra or linear ODE theory; the paper uses them to argue that Heisenberg's equation and the spectral description of observables arise from second moments of a classical Hamiltonian ensemble. A checked version separates what is a theorem from what is interpretation, and pins down the hypotheses (for example, that only symmetry of is needed for Eq. 48, not positive definiteness).
Formalizing it. None of these statements is new mathematics; the work is to formalize them in the paper's notation (, entrywise matrix derivatives, the matrix exponential) so that they can be reused for later parts of the paper, such as the real Dirac algebra of Sec. VII–VIII.
Most milestones are short calculations. The two steps needing real infrastructure are (i) the uniqueness of solutions of the linear matrix ODE , needed to identify with , and (ii) the dimension counts, which require an explicit basis or an isomorphism with symmetric/skew-symmetric matrices. Going through the Lax invariants alone gives only the traces of powers of , and recovering the characteristic polynomial from them needs Newton's identities; the similarity form of Eq. (51) gives the conservation of the characteristic polynomial directly.
Everything is over . Matrices are indexed by pairs , , , so that is literally a Kronecker product; is allowed. Time derivatives of matrix-valued functions are entrywise HasDerivAt; is Mathlib's power-series NormedSpace.exp. A Hamiltonian matrix is with symmetric (no definiteness); is any symmetric solution of Eq. (40) — positivity is not assumed because it is not used. Eigenvalues of real skew-symmetric matrices are taken over . "Number of linearly independent elements" is the dimension of the real span. No statement is vacuous: all hypotheses are satisfied, for example, by and .
All statements share the definition file UnQM_phase_space and the namespace UnQuantumMechanics.
The virial theorem relates the long-time average of the total kinetic energy of a bound system of particles to the average of the virial of the forces acting on them. It gives the average kinetic energy of systems too complicated to solve exactly, such as stars, planetary systems, galaxies and galaxy clusters. Fritz Zwicky used it to infer the existence of unseen matter, and it enters the derivation of the Chandrasekhar limit for white dwarfs. It does not depend on the notion of temperature and holds for systems that are not in thermal equilibrium.
Timeline (as recounted in the source article):
point particles move in . Particle has a constant mass , position , velocity and momentum ; the net force on it is . The kinetic energy is , the moment of inertia is , and
The time average over a duration is .
When forces come from pair potentials depending only on the distance , the force of on is , , and the total potential energy is . Power-law potentials are ; gravity is .
For a motion with , (continuous forces) that is bounded (positions and velocities bounded for ),
The theorem turns boundedness of a motion into a quantitative relation between averaged energies, without solving the equations of motion; with it gives for self-gravitating systems, the relation used for mass estimates of galaxy clusters. The result is classical and proved in the literature. This mission formalizes the standard derivation: the calculus identities for and , the pair-force algebra under Newton's third law, the gradient computation for distance potentials, and the averaging argument.
The mathematics is elementary; the work lies in the formal infrastructure: product rules for inner products of vector-valued trajectories, the gradient of in , re-indexing a double sum over ordered pairs into a sum over , and the fundamental theorem of calculus for with the required integrability. A tempting oversimplification is to assume that and converge individually; bounded motion does not guarantee this, so the targets are stated as limits of the combined expression.
Space is EuclideanSpace ℝ (Fin 3) and particles are indexed by Fin N. Trajectories are functions ; the equations of motion are hypotheses HasDerivAt (r k) (v k t) t and HasDerivAt (fun s => m k • v k s) (F k t) t. Masses are constant real numbers. Time averages are (interval integral). Pair forces are defined with Mathlib's gradient, with . Power-law coefficients may depend on the pair (symmetric), which contains the article's single constant . Real powers are Real.rpow; collision-freeness is assumed wherever pair distances enter. Boundedness is imposed only for . The hypotheses are satisfiable (for instance by a uniform circular two-body motion), so no target holds vacuously.
The Standard Model of particle physics does not explain the values of its dimensionless constants, nor does it require them to be constant in time. The proton-to-electron mass ratio is one such constant: it compares the scale of the strong interaction (which sets most of the proton mass) with the electroweak scale (which sets the electron mass). A measured change of over cosmic time would signal physics beyond the Standard Model, while a tight null result constrains models with additional scalar fields.
The standard test compares the frequencies of molecular transitions observed in distant galaxies with laboratory values. Different transitions respond differently to a change of , so a relative shift between them cannot be confused with the overall cosmological redshift.
Timeline. Optical studies of molecular hydrogen at redshifts reached (Malec et al. 2010; van Weerdenburg et al. 2011). Ammonia inversion lines, about 100 times more sensitive, moved the field to radio astronomy and gave constraints at the level toward the lensing galaxy of PKS 1830−211 at (Henkel et al. 2009; Kanekar 2011). Jansen et al. (2011) and Levshakov, Kozlov & Reimers (2011) pointed out that methanol transitions have sensitivity coefficients ranging from about to . Ellingsen et al. (2012) gave a first methanol limit from two lines. Bagdonaite et al. (Science, 2013) observed four methanol lines in PKS 1830−211 with the Effelsberg 100-m telescope and derived the limit at a look-back time of about 7 billion years.
A transition with frequency has sensitivity coefficient defined by
or, in infinitesimal form, . Pure rotational transitions have frequency inversely proportional to the reduced mass, hence to , so . Mixed torsion–rotation transitions of methanol have strongly enhanced coefficients (Table 1 of the paper: and ).
Each observed line is assigned a position , a velocity (km/s) on a common scale centred on redshift . If in the absorbing galaxy differs from the laboratory value by , the positions satisfy
up to a velocity offset common to all lines, where is the speed of light. Plotting against and fitting a straight line therefore gives .
The fit is a weighted least-squares fit with weights , where is the 1σ uncertainty of the -th position. With , , , , and , the slope, intercept and slope standard error are , and . The reduced chi-squared is .
The data (Table 1) are four lines: – (, ), – (, ), – (, ) and – (, ). Because A- and E-symmetry methanol behave as separate species that may be spatially segregated, the fiducial fit uses only the three E lines.
With the E-line estimate , its statistical error and the adopted systematic error ,
i.e. to the printed precision.
The result. The authors report the limit as statistically more constraining than previous radio-domain tests of a drifting . Because it uses a single molecular species, it is much less exposed to the main systematic of multi-species comparisons, namely that different molecules sit in different gas at slightly different velocities. The milestones record the internal evidence behind the choice of the fiducial fit: the poor four-line and the A–E velocity separation.
Formalizing it. The physical inputs (sensitivity coefficients, measured positions, the systematic budget) are taken as data. What the mission checks by machine is the chain from those data to the printed numbers: the definition of the sensitivity coefficient and its value for rotational lines, the correctness of the line-fit estimator, and the arithmetic of every reported fit, separation and error combination.
The numerical milestones are exact statements about explicit rational data, but they involve nested sums, quotients and square roots, so a certified proof requires careful interval bounds rather than floating-point evaluation. The paper's numbers are rounded from unrounded measurements: recomputing from the rounded Table 1 entries gives, for example, instead of , and instead of for the four-line fit. Tolerances therefore had to be chosen so that every statement is both faithful to the printed value and true for the tabulated data. The general recovery milestone requires showing that the normal equations are nondegenerate whenever the are not all equal.
Fin n. Velocities are in km/s and km/s.deriv.Reusable pieces: the weighted least-squares definitions and the exact-recovery lemma apply to any straight-line fit with known uncertainties.
In the paper that introduced the AdS/CFT correspondence (hep-th/9711200), Maldacena takes a stack of branes in string or M-theory, sends the string or Planck length to zero while holding the energies of the worldvolume theory fixed, and follows the supergravity solution of the branes through the same limit. The field theory on the branes decouples from the bulk, and the supergravity metric converges, after an overall rescaling, to a product of an anti-de Sitter space and a round sphere. The conjectured duality is between the worldvolume conformal field theory and string/M-theory on that product.
Section 2 of the paper treats D3-branes, whose limit is ; that case, together with the Appendix on Poincaré coordinates for anti-de Sitter space, is the subject of the separate mission Maldacena 1999: the near-horizon geometry of D3-branes is AdS5 × S5. This mission covers the next three cases in the paper:
In each case the paper states the ratio of the sphere radius to the anti-de Sitter "radius", and how both depend on the number of branes.
Anti-de Sitter space. For and , of radius is the hyperboloid
in flat (Appendix, eq. (A.1)). The Poincaré coordinates , with and , are given by , and (eq. (A.2)). In these coordinates the induced metric is
where . In Lean these objects are AdS, poincareEmbedding, ambientForm and minkowskiForm, taken from the published definition file Maldacena1999_Defs; the induced metric of a tangent vector is ambientForm applied to the Fréchet derivative of poincareEmbedding.
Brane metrics. Each brane solution has the form , with the Minkowski metric along the branes and the round metric of the unit -sphere:
The decoupling limits hold fixed (M5), (M2), and , and (D1–D5), while or . The Lean definitions m5Metric, m2Metric and d1d5Metric evaluate these metrics on a tangent vector , where is tangent at a point of the unit sphere and .
With written in terms of by the chain rule, the rescaled metrics converge to
for M5-branes; to
for M2-branes; and to
for the D1–D5 system.
The goal asserts that each limit equals the metric of (induced metric (A.3) plus a round sphere), with radii, in units of or :
These three limits are the geometric input for the paper's conjectures that the six-dimensional theory is dual to M-theory on , the M2-brane theory to M-theory on , and the two-dimensional theory of the D1–D5 system to IIB string theory on . The radii set the regime in which supergravity can be trusted (large , or large ). They also fix which anti-de Sitter isometry group appears (, , ); the paper matches it with the bosonic conformal group of the brane theory.
The paper derives these limits in a few lines each. To our knowledge they have not been formalized. The mission produces machine-checked statements and proofs of the three limits and of their identification with anti-de Sitter geometry, reusing the published Poincaré-coordinate results of the D3-brane mission.
The computation is elementary but full of exponents. Each case needs a change of radial variable, a fractional power of a harmonic function whose constant term is dropped in the limit, and a comparison of the coefficient of with the Poincaré form, which in the M5 and M2 cases requires a constant rescaling of . In Lean, the limits are one-sided limits of expressions built from real powers Real.rpow, and the goal requires a Fréchet-derivative computation on (available from the published theorem Maldacena1999.induced_metric_poincare).
All metrics are evaluated pointwise on tangent vectors; no manifold structure is used. The round sphere is the unit sphere in Euclidean and a tangent vector at is a with . The limits are taken along (resp. ) with , , , , and the tangent vector fixed. For the D1–D5 system only the six-dimensional metric (4.2) is formalized: the compact factor , whose volume is constant in the limit, is not modelled. In the goal the anti-de Sitter coordinate is the paper's up to a constant factor ( for M5, for M2, for D1–D5), so that the limit metric has exactly the form (A.3). All physical parameters are strictly positive. Fluxes, supersymmetry and the duality conjectures themselves are out of scope.
In 1997 Maldacena observed that the low-energy limit of a stack of coincident D3-branes in type IIB string theory can be described in two ways: as four-dimensional super-Yang–Mills theory living on the branes, and as supergravity (ultimately string theory) on the near-horizon geometry of the branes. The paper computes that this near-horizon geometry is five-dimensional anti-de Sitter space times a five-sphere, , with both factors of the same radius , in string units, and conjectures that the two descriptions are dual. This AdS/CFT correspondence became one of the most cited results in theoretical physics (Maldacena 1999; see also Gubser–Klebanov–Polyakov 1998, Witten 1998).
The duality itself is a physical conjecture with no complete mathematical formulation. What the paper does contain is a small body of exact geometric computations on which the conjecture rests: the decoupling limit of the D3-brane metric, the description of AdS as a hyperboloid with its symmetry, the Poincaré coordinates in which the limiting metric is written, and the ordinary differential equation expressing broken conformal invariance of a probe brane. This mission formalizes exactly those computations.
Fix . The ambient space has coordinates and flat metric . Anti-de Sitter space of radius is the hyperboloid (eq. (A.1))
Linear maps preserving form the group , which contains the conformal group of -dimensional Minkowski space.
The Poincaré coordinates (eq. (A.2)) are and for ; on the hyperboloid, , where . Written in reverse, this is a map .
The D3-brane metric (eq. (2.2)) for string coupling , branes and string scale is
where are the worldvolume coordinates and is the round metric of the unit five-sphere. The decoupling limit (eq. (2.1)) sends keeping fixed.
For , , with , and every tangent vector with tangent to ,
which is eq. (2.3): the metric of in Poincaré coordinates plus the round metric of of the same radius.
The goal is the precise sense in which "the near-horizon geometry of D3-branes is with ": the radius formula is what later links the 't Hooft coupling of the gauge theory to the curvature of the string background, and the Poincaré-patch form (A.3) is the coordinate system in which essentially all subsequent AdS/CFT computations are carried out. Milestones 1–4 give a reusable, self-contained account of anti-de Sitter space as a quadric in with its Poincaré chart, useful to any development of Lorentzian geometry. Milestone 6 is the step by which the paper argues that the probe D3-brane action (2.6) is fixed by conformal symmetry.
All of these statements are standard computations in the physics literature; none is open. The value of the mission is a machine-checked version of the geometric content of the paper, stated with the paper's own conventions, not a new result. The duality conjecture itself is outside the scope of the mission.
The computations are elementary but bookkeeping-heavy. The induced-metric identity (A.3) requires differentiating a map from to with arbitrary, so sums over the index sets must be split into the timelike, spacelike and light-cone components; a computation for one fixed does not suffice. The bijection statement needs an explicit inverse and the observation that the hyperboloid equation determines from and . The limit statements require controlling square roots of expressions that blow up like . The ODE characterisation requires a uniqueness argument on an interval, not only verification that the stated function is a solution.
Coordinates of are indexed by with index for , index for and index for ; worldvolume coordinates are indexed by with index timelike. Metrics are represented by the quadratic forms they induce on tangent vectors; the induced metric is expressed through the Fréchet derivative of . The round metric of is the Euclidean norm squared of a tangent vector of the unit sphere in . Square roots and divisions are Lean's total functions; all statements restrict to , , , , , where no junk values arise. The symmetry milestone is stated for the full group , which contains the named in the paper.
No new infrastructure beyond Mathlib's calculus, real analysis and matrix libraries is needed. Contributions of general lemmas about quadrics in pseudo-Euclidean spaces are welcome.
Projective measurement is usually taught together with state update: an observable is measured, a value is obtained, and the conditional state is assigned. These are two different questions. The first is the prediction of the outgoing ensemble from the incoming ensemble and the measured observable alone, before the outcome is known; the second is the incorporation of the outcome once it is known. The technical brief by G. Carcassi for the Assumptions of Physics collaboration (AoP technical briefs) isolates the first question and treats the measurement as a black-box process that only relates incoming and outgoing ensembles, without committing to a mechanism.
Within this view the standard prediction, the nonselective (Lüders) post-measurement ensemble, admits several characterizations that come from different traditions: the algebraic pinching map, the long-time limit of a dephasing Lindblad equation (open quantum systems, see Lindblad 1976), and a closest-point principle, either in Hilbert–Schmidt distance or in quantum relative entropy (Umegaki 1962). The brief's Theorem 1 states that these characterizations select the same process.
Fix a finite index set ; the Hilbert space is and operators are complex matrices. A density matrix is a positive semidefinite matrix with . An observable is a Hermitian matrix with spectral decomposition
where ranges over the distinct eigenvalues of and is the orthogonal projection onto the -eigenspace.
The spectral equilibration process is an unknown map on density matrices. The brief's four conditions on it are:
For every Hermitian and every map ,
The milestones follow the steps of the brief's proof: the block decomposition (eq. 2); the blockwise solution (eqs. 4–5); convergence (eqs. 9–10) and EQ-LIND EQ-MEAS; the equivalence ; preserves density matrices; the Pythagorean identity (eq. 11) and EQ-HS EQ-MEAS; the relative-entropy chain rule (eq. 12); (eq. 13); non-negativity and definiteness of ; and EQ-KL EQ-MEAS.
The result says that "projective measurement" can be specified without reference to wave-function collapse: any of the three dynamical or variational descriptions pins down the same input–output map. Downstream, this justifies treating repeatable measurements as equilibration processes whose outputs are fixed points, and treating the outcome-update step as classical conditioning on a mixture.
The mathematics in finite dimension is classical; this mission asks for a machine-checked proof of the equivalence in Lean 4 with Mathlib. A complete development produces reusable pieces: spectral projections and the pinching map for Hermitian matrices, explicit solutions and asymptotics of a dephasing Lindblad semigroup, and an extended-real relative entropy with Klein's inequality.
The Hilbert–Schmidt part is linear algebra once block-diagonality is in place. The Lindblad part requires uniqueness of solutions of a linear matrix ODE on the closed half-line, to transfer the explicit blockwise formula to an arbitrary solution. The relative-entropy part is the most delicate: it needs the interaction between the functional-calculus logarithm and block structure ( is block diagonal when commutes with ), the support conventions that make take the value , and Klein's inequality with its equality case for matrices, which the development must supply if the library does not already provide it.
Real.log (so , i.e. the logarithm on the support); takes values in the extended reals and equals unless .Contributions of general-purpose lemmas (Klein's inequality, uniqueness for linear ODEs on half-lines, properties of pinching) are welcome as separate theorems.
In 1948 R. P. Feynman published a third formulation of non-relativistic quantum mechanics, alongside Schrödinger's differential equation and Heisenberg's matrix algebra (Feynman 1948). The probability amplitude for a particle to follow a path is postulated to be , with the classical action, and the amplitude to arrive at is the sum of these contributions over all paths from the past. This is the path integral, now a standard tool across quantum field theory, statistical mechanics and probability.
The formulation is claimed to be mathematically equivalent to ordinary quantum mechanics. The key step of that claim is Section 6 of the paper, "The wave equation": the wave function defined by the path integral satisfies Schrödinger's equation. This mission formalizes that step for a particle in one dimension, as the paper does.
Timeline:
Fix , a mass and a potential . For a time step the short-time action between positions (time ) and (time ) is (Eq. 22)
and the normalizing factor is (Eq. 28, principal branch). The one-step path-integral evolution (Eqs. 18, 23) takes a wave function to
Iterating and letting is the path integral (15) of Section 5. The Hamiltonian is . The paper also uses the Gaussian moments of Eq. (26), which are oscillatory; footnote 13 defines them by replacing with and letting :
For every Schwartz function and every ,
that is, for the path-integral evolution, which is Schrödinger's equation (30). This is the content of Feynman's statement that (18), valid to first order in , yields (30).
The goal is the step that connects the path-integral postulates to the ordinary formulation: without it the formulation of Sections 3–5 is not known to reproduce any quantum mechanics. The Fresnel integrals of (26) and the short-time kernel appear throughout semiclassical analysis and in every derivation of path integrals from the Schrödinger equation.
The physics result is classical and its rigorous versions are known (via the Trotter product formula or oscillatory-integral estimates). The work here is the formalization: Mathlib has the complex Gaussian integral and Schwartz functions, but not Fresnel integrals, the free Schrödinger kernel, or the short-time asymptotics of oscillatory integrals. None of the targets is currently formalized on the platform.
Feynman's derivation expands in a Taylor series under the integral and integrates term by term against . Those integrals are not absolutely convergent, and the higher moments do not even exist as improper Riemann integrals, so the term-by-term step is not justified as written. A proof has to control the Taylor remainder against an oscillatory kernel whose width is of order , uniformly as , with a prefactor that blows up like . The naive dominated-convergence argument does not apply, because the kernel has modulus everywhere and does not concentrate in absolute value.
𝓢(ℝ, ℂ), which formalizes the paper's "relatively smooth" that "falls off sufficiently for large ". For such the integral defining is absolutely convergent, so the Lebesgue (Bochner) integral is used.Useful infrastructure: Fresnel integrals, Fourier representation of the free Schrödinger kernel on Schwartz space, and differentiation of oscillatory integrals with a parameter. All are reusable beyond this mission.
A coincident pair of a D-brane and an anti-D-brane in type II string theory carries an open-string tachyon, a mode of negative mass squared. In Sen, hep-th/9805019 it was conjectured that at the minimum of the tachyon potential the negative potential energy exactly cancels the sum of the tensions of the brane and the anti-brane, so that the system decays to a configuration of zero energy density, i.e. the supersymmetric vacuum. The paper formalized here, A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012, gives a short argument for this, and the author says explicitly that it is not a rigorous mathematical proof. The argument follows Gava–Narain–Sarmadi, hep-th/9704006 and belongs to the programme of tachyon condensation. Later work, starting with open string field theory computations, tested the same conjecture numerically.
Work in string units (). Wrap a D2-brane and an anti-D2-brane on a torus with radii and area . Each brane carries one unit of magnetic flux, , with signs chosen so that each carries unit of D0-brane charge. T-duality on both circles gives a dual torus with radii and coupling . On the dual torus the system is described by a gauge theory: a gauge field is a pair of complex-matrix-valued functions of , with field strength . The gauge transform by a matrix-valued is . The background configuration is
subject to twisted boundary conditions with transition functions and . A D-brane with coupling has tension .
With the mass at the classical minimum (two D2-branes with zero field strength on the dual torus, re-expressed through ), for each fixed :
The vanishing of the energy at the tachyon minimum is the basis for identifying stable non-BPS D-branes as tachyonic solitons on brane–antibrane pairs, as discussed at the end of the paper, and it was a starting point for later work on tachyon condensation. The paper's argument is heuristic. This mission makes explicit which steps are mathematics (the gauge-theoretic facts (4)–(8), the gauge covariance used on p. 3, and the algebra (9)–(11) and its limit) and machine-checks them. The physical inputs (the BPS argument that the mass (9) persists as parameters vary, and the identification of the minimum-energy configuration) are recorded as modelling assumptions in the definitions, not proved.
The algebraic milestones (9)–(11) and the limits are elementary. The substantive formal work is in the gauge-theory milestones: computing derivatives of the matrix exponential in (5), the smooth homotopy with flat ends required by (8) (existence rests on the simple connectivity of , but the statement asks for an explicit smooth -valued map with prescribed boundary values and vanishing normal derivative), and the covariance computation of the field strength under a non-unitary, merely invertible .
Coordinates are ; the paper's index is Fin 2 (, ). Matrices are Matrix (Fin 2) (Fin 2) ℂ; partial derivatives are taken entrywise; the inverse is the Mathlib matrix inverse; the exponential is NormedSpace.exp. Radii and couplings are real, with positivity assumed wherever the paper's quantities are physical. The goal cannot be trivialized by division by zero, because it is a statement about the limit of large positive radii. All definitions live in a single definition file under the namespace SenTachyon.
In the 1993 essay Dimensional Reduction in Quantum Gravity (arXiv:gr-qc/9310026), G. 't Hooft argued that, once gravitational collapse is taken into account, the number of quantum states available to a region of space grows with the area of its boundary rather than with its volume. The essay is the origin of what is now called the holographic principle (developed further by Susskind, arXiv:hep-th/9409089). Besides the physical counting argument, the essay contains a small, fully precise mathematical model: a cellular automaton on the cubic lattice whose data on a one-dimensional line determine the data everywhere. This mission formalizes the quantitative estimates and the automaton statements of the essay.
Entropy estimates (eqs. (4)–(11)). In natural units, a region bounded by a sphere of radius has volume and area . A thermal gas of particle species at temperature has energy and entropy with positive constants . It stays outside its own Schwarzschild radius if . A black hole of mass has entropy (eq. (1), additive constant dropped).
Plaquette automaton (eqs. (12)–(19)). Data live on lattice sites. An elementary plaquette has lowest corner and is spanned by two of the unit vectors ; its corners in cyclic order are . On every plaquette a relation is imposed such that any three entries determine the fourth uniquely. The relations may differ from plaquette to plaquette. On the unit cube with corners , , , , , , , , the six face relations are (12a–f). The staircase (eq. (14)) is the sequence
A family of face relations is consistent (eq. (16)) if every choice of extends to data on the cube satisfying all six relations; equivalently, the three values of produced by (12b), (12d), (12f) agree. Linear relations (eq. (17)) have the form , with every invertible mod .
For any family of plaquette relations with the three-determine-the-fourth property, two solutions on that agree on the staircase agree everywhere:
The goal is the essay's concrete mathematical example of dimensional reduction: in a -dimensional lattice model, a one-dimensional set of data carries all the information. Milestone 5 shows that the reduction is sharp in the linear case: no data beyond the staircase are needed, and none of the staircase data are constrained. Milestones 1–2 are the scaling estimates behind the area law . The physical argument around them (black-hole thermodynamics, the Schwarzschild criterion) is taken as modelling input, not formalized. The results are stated in the essay but, as far as is known, have not been machine-checked.
The local step (one cube, Milestone 3) is elementary. The goal needs a global propagation argument. The staircase is a thin zig-zag line, and each application of a plaquette relation fixes only one new site. So the proof has to show that repeated local determination starting from the line eventually reaches every site of , in both directions along the line and in both transverse directions. Layer-by-layer propagation in does not apply directly, because the staircase is not a full layer.
Sites are ℤ × ℤ × ℤ. Data take values in ZMod p for an arbitrary natural number ; the uniqueness statements hold for every . The three-determine-the-fourth property is stated with unique existence () for each slot, which matches "uniquely determined" in the essay. Relations may depend on the plaquette, so no translation invariance is assumed. Consistency (16) is encoded as extendability of the four free values on the unit cube. In Milestones 1–2 the region is a round sphere of radius , so and are expressions in , and the constants are existentially quantified before all physical variables. Contributions welcome: proofs of each milestone, and further faithful statements from the triangular-lattice model (eqs. (20a–f)).
Neutrinos produced by weak interactions are created in flavour eigenstates (, , ), while they propagate as mass eigenstates. When the two bases differ, the flavour content of a neutrino beam oscillates with distance. In ordinary matter this picture is modified: electron neutrinos scatter coherently forward on electrons via the charged current, which adds an extra potential energy to the component only (Wolfenstein 1978). Mikheyev and Smirnov observed that this potential can resonantly enhance the mixing, so that an almost complete flavour conversion is possible even for a tiny vacuum mixing angle — the MSW effect. It is the accepted explanation of the energy dependence of the solar deficit and is relevant for neutrinos crossing the Earth and for supernova neutrinos.
This mission formalizes the constant-density result of Section 8.2 of E. Kh. Akhmedov's lecture notes Neutrino physics (hep-ph/0001264): the two-flavour transition probability in matter of constant density, eq. (95), together with the statements that lead to it and follow from it, eqs. (91)–(98).
Fix the vacuum parameters: the mass-squared difference , the neutrino energy , and the vacuum mixing angle . The matter is described by the Fermi constant and the electron number density , through the charged-current potential (eq. (87))
Write . After discarding all terms proportional to the identity (common phases), the vector of flavour amplitudes evolves by the Schrödinger equation with the real symmetric MSW Hamiltonian (eq. (91))
The derived quantities are the energy gap in matter (eq. (94)), the oscillation length in matter (eq. (96)) and the oscillation amplitude in matter (eq. (97)):
The vacuum oscillation length is (eq. (61)). Distance and time are identified (, units with ).
If solves for all with (a pure is produced at ), then for every
Eq. (95) shows that at constant density the flavour transition has exactly the vacuum form with replaced by ; together with the resonance condition (98) it underlies quantitative discussions of matter effects, from the solar neutrino problem to long-baseline experiments crossing the Earth. The milestones separate the linear-algebra content (diagonalizing a real symmetric matrix) from the analytic content (solving a linear constant-coefficient ODE and the uniqueness of its solution).
The result is textbook material and is proved in the source. This mission adds a machine-checked derivation from the Schrödinger equation itself — including uniqueness of the solution of the initial-value problem, which the source leaves implicit — and reusable Lean definitions for later missions on the adiabatic (variable-density) regime of Section 8.3.
The algebra of eqs. (93)–(97) is elementary. The substantive step for a formal proof is the passage from "the Hamiltonian is diagonalized by a rotation" to "every solution of the ODE with the given initial datum has the stated component": this needs a uniqueness theorem for linear ODEs on (or an equivalent argument). Degenerate parameter values (, ) must be handled, since the Lean statements do not exclude them.
All parameters are real numbers; the state is a function (index , ) assumed differentiable everywhere with derivative , where is the real matrix above viewed as a complex matrix. The probability is the squared modulus . is assumed throughout; the sign of , the value of and the density are unrestricted. Lean's division convention () applies to and when ; in that degenerate case is a multiple of the identity and both sides of the goal are .
A statement that assumed the closed-form solution, or assumed the probability formula as a hypothesis, would be trivial; the goal instead quantifies over every solution of the initial-value problem. Proofs of any milestone, and reusable lemmas on uniqueness for linear constant-coefficient ODEs, are welcome.
Leptogenesis is a class of scenarios in which the baryon asymmetry of the Universe is produced from a lepton asymmetry generated in the out-of-equilibrium decays of heavy singlet neutrinos , which also give the light neutrinos their small masses through the type I seesaw (Fukugita–Yanagida 1986). The review of Davidson, Nardi and Nir (Phys. Rep. 466 (2008) 105) collects the standard results of the field. One of its central quantitative facts is an upper bound on the CP asymmetry in the decays of the lightest singlet , in terms of and the light-neutrino masses. This bound is the origin of the familiar lower bound GeV for thermal leptogenesis with hierarchical singlets (Eq. (5.12) of the review).
Timeline. Casas and Ibarra introduced the orthogonal-matrix parametrization of the seesaw in 2001 (hep-ph/0103065). Davidson and Ibarra derived the bound on the total asymmetry in 2002 (hep-ph/0202239); Hamaguchi, Murayama and Yanagida gave a related bound (hep-ph/0109030). Once flavour effects were recognised (around 2006), attention moved to the flavoured asymmetries , whose bound (Eq. (5.10) of the review) is the goal of this mission.
There are three lepton flavours and three singlets with Majorana masses . We work in the mass basis of the charged leptons and of the . The Yukawa matrix is an arbitrary complex matrix, and is the Higgs vev. The light-neutrino mass matrix (Eq. (2.5)) is
a complex symmetric matrix. It is diagonalized as with unitary and , (Eq. (2.6)). The largest and smallest light masses are and . The Casas–Ibarra matrix is (Eq. (2.11)).
At tree level decays into and with partial rate and total rate (Eq. (4.5)). So the branching fractions satisfy . For hierarchical singlets the flavoured CP asymmetry is (Eq. (5.9))
Eq. (5.10) is the input to the lower bounds on and on the reheat temperature for hierarchical thermal leptogenesis (Eq. (5.12), Sec. 9.4.3), and it shows that flavoured asymmetries are not suppressed for degenerate light neutrinos, unlike the total one (Eq. (5.17)). These are established results. The work here is to formalize them: to state the seesaw quantities precisely and machine-check the linear-algebra steps (Takagi factorization, complex orthogonality, operator-norm bounds) that the physics literature takes for granted. To the captain's knowledge none of these statements has a machine-checked proof.
The goal reduces to an operator-norm estimate for the complex symmetric matrix . That estimate needs the diagonalization , which is a Takagi (Autonne–Takagi) factorization, not a unitary eigen-decomposition: is symmetric, not Hermitian. The obvious move, applying the spectral theorem to , fails because is in general not normal. The milestone-1 existence statement therefore needs its own argument, for example through the Hermitian matrix . The total-asymmetry bound (milestone 4) needs a finer argument than the triangle inequality to produce the difference rather than .
Fin 3); the singlet "" is index .⨆ i, masses i and ⨅ i, masses i over the three diagonal entries. No ordering of the is imposed.IsLightMassDiagonalization m U masses (unitary , , ). It is always satisfiable by milestone 1, so it is not vacuous.In the note Reformulating String Theory with the 1/N Expansion (arXiv:hep-th/9405069), C. B. Thorn argues that stability and causality, which are manifest in quantum field theory but obscure in string theory, would become evident if strings were composite objects built from point-like constituents ("string bits"). The proposal combines the light-cone parametrization of the string with 't Hooft's expansion (G. 't Hooft, Nucl. Phys. B72 (1974) 461): bits are created by the entries of an matrix field , closed strings by the singlet traces , and plays the role of the string coupling.
A load-bearing step of the proposal is that a long closed chain of bits behaves like a continuous string: in the continuum limit with fixed, the finite-energy excitations must be string excitations. Thorn justifies this with the remark (p. 5) that "the low energy excitations of an particle discretized string are the two-body level spacing". This mission formalizes that remark for the harmonic Hamiltonian written in the paper, together with the cyclic symmetry that ties the matrix traces to closed strings.
A discretized light-cone string with bits is described by transverse positions with cyclic identification and Hamiltonian (p. 4)
The potential term is the quadratic form of the cyclic Laplacian , (indices mod ), and the equations of motion are . A normal-mode frequency is an with an eigenvalue of ; write for the set of them. With these are the excitation-level spacings of the chain.
The singlet creation operators are ; since the commute with each other, cyclic invariance of the trace gives the cyclic symmetry of the string wave function.
For all and ,
The goal is the quantitative content of the paper's continuum-limit argument in the harmonic case: the gap of an -bit chain closes like relative to the two-body scale, so at fixed the low-lying spectrum approaches the equally spaced string spectrum. The same spectral facts about the cyclic Laplacian (the spectrum of the cycle graph) are used in lattice field theory and spectral graph theory, so the milestones are reusable outside this mission. The results are classical; the work here is their machine-checked formalization in a form tied to the string-bit Hamiltonian.
The trace and quadratic-form statements are finite algebra. The substance lies in the spectrum: exhibiting real eigenvectors for every needs trigonometric sum identities, and the completeness statement needs an argument that no other eigenvalues exist, which must handle the degenerate pairs . Identifying the least positive value then requires the symmetry and monotonicity of on .
String/M theory appears to admit a very large number of four-dimensional vacua, and M. R. Douglas's 2003 paper The statistics of string/M theory vacua proposes to study them statistically: instead of constructing vacua one at a time, one places a measure on a space of effective theories and computes expected numbers and distributions of vacua. Two concrete mathematical ingredients of that programme are the subject of this mission.
The first is the Bousso–Polchinski counting of flux vacua (Section 3.6 of the paper, following Bousso–Polchinski 2000). Quantized fluxes form an integer vector , and the flux energy is a positive quadratic form in . The number of flux choices with energy below controls whether a small cosmological constant can be realised; the paper evaluates the number distribution (3.13) by replacing the lattice sum with an integral, obtaining a density proportional to .
The second is the Gaussian ensemble of superpotentials (Section 4 and 4.1): a random polynomial superpotential whose coefficients are independent complex Gaussians, with an explicit normalising constant and an explicit count of coefficients.
Fix an integer (the number of independent flux quanta, in the paper) and a constant (in the paper ). For a flux vector the flux potential is
and the flux vacua count below level is
This is the cumulative distribution function of the measure of eq. (3.13). The unit ball in has volume , and the unit sphere has area .
For the superpotential ensemble, a polynomial in variables of degree at most has one coefficient per monomial with ; the paper states there are of them. The coefficients are given the weight , , which the paper says is unit normalised.
This is the precise, integrated form of the approximation in (3.13): integrating from to gives exactly .
The goal makes rigorous the step "replace the sum with an integral" that underlies the Bousso–Polchinski estimate of how many flux vacua lie below a given energy, with the exact constant appearing in (3.13). Milestones 4 and 5 certify the combinatorial and analytic constants of the Gaussian ensemble (4.6) on which the paper's densities (4.7)–(4.10) are built. None of these results is new mathematics: the goal is the -dimensional analogue of the Gauss circle problem at leading order, and the milestones are classical. What the mission adds is a machine-checked version of the precise constants used in the paper.
The goal requires comparing a lattice-point count with a volume. The naive bound, counting unit cubes centred at lattice points, must be controlled uniformly: cubes meeting the boundary of the ball contribute an error of order with , and one has to show that this is . The volume formula for Euclidean balls expressed through the Gamma function, and its transport to the product space with the sum-of-squares form, is further required infrastructure.
Fin J → ℤ; the count uses Set.ncard, whose value on an infinite set would be — milestone 1 rules out that degenerate reading.Fin J → ℝ (not EuclideanSpace), with the quadratic form written out explicitly.DouglasVacua.fluxPotential, DouglasVacua.fluxVacuaCount.