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?
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 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.
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.
In celestial holography, scattering amplitudes of massless particles in four-dimensional flat spacetime are rewritten, by a Mellin transform in the particle energies, as correlation functions of operators on the two-dimensional celestial sphere. Soft theorems then become Ward identities of two-dimensional currents. Guevara, Himwich, Pate and Strominger (arXiv:2103.03961) found that the conformally soft graviton modes obtained this way close under the collinear OPE into an infinite-dimensional algebra, and Strominger (arXiv:2105.14346) identified it, after a rescaling, with the wedge subalgebra of , the Lie algebra of polynomial area-preserving (Hamiltonian) vector fields on a two-plane. The review of B. Zhu (arXiv:2606.24285, Section 7.1) summarises this derivation, together with its gauge-theory counterpart, the gluon -algebra, and the action of on it. The review describes the celestial -algebra as a consistency test for any proposed flat-space hologram.
The wedge range is the set of labels with
equivalently: and are both natural numbers. Let be the complex vector space with basis indexed by the wedge range, and define a bilinear bracket on by Eq. (7.8),
where the right-hand side is whenever falls outside the wedge.
Eq. (7.9) realises as the monomial in the polynomial ring , equipped with the Poisson bracket .
The conformally soft graviton modes (, ) obey the commutator (7.5) with factorial coefficients and the gravitational coupling . The rescaling (7.6), , turns (7.5) into (7.8).
On the gauge-theory side, with colour index and Lie-algebra structure constants , the conformally soft gluon modes obey (7.14). The rescaling (7.15), , gives the -algebra (7.16), . The wedge algebra acts on it by (7.17), .
The statements fix, in a machine-checked form, the precise normalisations used in the celestial literature: the wedge range, the rescalings (7.6) and (7.15), and the overall factor in the Poisson realisation, which the review leaves convention-dependent. They form the algebraic base layer for later formalisations of deformations of , its loop algebra , and the gluon–graviton soft algebras. The results themselves are established in the physics literature. The formal work that remains is the combinatorics of the factorial coefficients, the closure of the finite wedge range, and the Jacobi identities.
None of the statements is deep, but each carries bookkeeping that is easy to get wrong. The factorial coefficients of (7.5) and (7.14) must cancel exactly against the rescalings. At the corners of the wedge (, , or ) the target label leaves the wedge, and the structure constant must be shown to vanish there. The Jacobi identity for (7.8) does not follow term by term from the formula; the natural route is through the Poisson realisation, which must first be shown to be faithful.
All objects are over . Labels are rationals, and every label set is carved out by the predicate " and are natural numbers". Vector spaces with a given basis are finitely supported functions on the index set, and brackets are the bilinear extensions of the basis formulas. When the target label of a bracket falls outside the wedge, the bracket is defined to be (milestone 1 shows this only happens when the structure constant already vanishes). Factorials of rational arguments are taken of the truncation to a natural number; on the relevant ranges the arguments are natural numbers, and at the single corner where (7.5) has argument its prefactor vanishes. The operator-level identities (milestones 2 and 5) are stated for an arbitrary complex vector space with an arbitrary bilinear bracket, taking (7.5) resp. (7.14) as hypotheses on the given modes. The colour algebra is given by structure constants on a finite index set , with antisymmetry and the Jacobi identity as the definition of Lie structure constants. The factor uses the convention , and milestone 2 assumes .
The Minimal Standard Model (MSM) — the gauge theory with three generations of quarks and leptons, one Higgs doublet and classical gravity — accounts for almost all laboratory phenomena, but it does not accommodate several empirical facts established since the late 1990s: non-baryonic dark matter, dark energy, neutrino masses and mixings, the baryon asymmetry of the universe, and nearly scale-invariant, adiabatic, Gaussian density fluctuations. Davoudiasl, Kitano, Li and Murayama (Phys. Lett. B 609 (2005) 117) propose the new Minimal Standard Model (NMSM): the most general renormalizable Lagrangian obtained by adding the minimal particle content needed for these facts — two right-handed Majorana neutrinos , one -odd real singlet scalar (dark matter), one real scalar (the inflaton), and a cosmological constant — six new degrees of freedom in total.
Most of the paper's claims are phenomenological (relic abundance, the Higgs-mass window from one-loop running, direct-detection rates). A smaller set are exact mathematical consequences of the model's structure, and this mission collects those.
Neutrino sector (Eq. (4)). In the basis where the right-handed-neutrino mass matrix is real and diagonal, the model has masses and a complex Yukawa matrix . With Higgs vacuum expectation value , the Dirac mass matrix is . The neutral leptons then have the complex symmetric Majorana mass matrix
and the seesaw light-neutrino mass matrix is . The physical masses described by a complex mass matrix are its singular values, the square roots of the eigenvalues of .
Inflaton sector (Eq. (5)). Inflation is driven by the quadratic potential (chaotic inflation). With reduced Planck mass , the slow-roll parameters are and , inflation ends where , the number of e-folds between and is , and the observables are and .
Scalar sector running (Eq. (10)). The singlet quartic coupling obeys the one-loop equation , , where is the Higgs–singlet coupling.
For every , every complex and all , some physical mass of the full matrix vanishes:
This is the paper's statement that with only two right-handed neutrinos "one of the neutrino masses exactly vanishes" (pp. 119, 122).
The vanishing neutrino mass is a sharp, falsifiable prediction of the NMSM: as the paper notes, a positive neutrino-mass signal at KATRIN would require masses for all three neutrinos, and a neutrinoless double-beta-decay signal in near-future experiments is possible only for the inverted hierarchy. Milestone 2 makes precise the paper's parameter count (eleven parameters in Eq. (4) against seven light-neutrino observables): the two-right-handed-neutrino seesaw reproduces every rank- light mass matrix. Milestones 3–6 pin down the closed-form content behind the inflationary predictions, the argument that baryogenesis is required, and the triviality behaviour of the singlet coupling.
These results are textbook-level linear algebra and calculus once stated; the contribution of the mission is a precise, machine-checked statement of exactly which claims of the paper are mathematical theorems and under which conventions.
The goal and Milestone 1 are linear-algebra facts, but they must be connected to the spectral-theorem definition of physical masses (eigenvalues of ), not merely to a determinant. Milestone 2 requires a Takagi-type decomposition of complex symmetric matrices (a rank- complex symmetric matrix is a sum of terms ), which is not available in Mathlib. Milestone 3 requires evaluating a parametric integral and derivatives of the potential. Milestone 6 is an ODE comparison argument from a differential inequality.
All matrices are over , indexed by Fin 2, Fin 3 and Fin 3 ⊕ Fin 2. Physical masses are defined as square roots of the eigenvalues of from Mathlib's spectral theorem for Hermitian matrices; their ordering is Mathlib's and no statement depends on it. Slow-roll quantities use Mathlib's deriv and interval integral; Lean's junk value cannot affect the stated results because the inflaton interval stays away from . The phenomenological results (dark-matter relic abundance, the – GeV Higgs window, the GeV– TeV singlet window, direct-detection rates) rely on numerical integration and are out of scope. The one-loop beta functions are taken as given ODEs; their derivation from the Lagrangian is not formalized.
Shock waves are ubiquitous in astrophysical gases: supernova remnants, stellar winds meeting the interstellar medium, accretion flows onto compact objects, and jets all contain them. Because astrophysical flows are typically highly supersonic and nearly inviscid, the internal structure of a shock is thin compared with the flow, and the shock is treated as a discontinuity. What connects the states on either side is not the detailed dissipative physics inside the shock but the conservation of mass, momentum and energy across it. For a perfect gas these conditions can be solved in closed form, giving the post-shock density, velocity and pressure as explicit functions of the pre-shock Mach number. These formulas are a standard tool, used for example as the boundary condition of the Sedov–Taylor blast-wave solution for supernova remnants.
The formulas go back to Rankine (1870) and Hugoniot (1887–1889). This mission follows the presentation in the Cambridge Part III lecture notes of G. I. Ogilvie, Astrophysical fluid dynamics, J. Plasma Phys. 82 (2016) 205820301 (doi:10.1017/S0022377816000489), §6.3.2 and Example A.13.
Consider a perfect gas with constant adiabatic exponent (for example for a fully ionized monatomic gas). A thermodynamic state is described by the density and pressure ; the specific enthalpy is , the specific internal energy is , and the adiabatic sound speed is .
A normal shock is a planar discontinuity, here taken at rest at , through which gas flows from left to right with velocity component normal to the shock. The upstream (pre-shock) state is and the downstream (post-shock) state is . Writing , the states satisfy the Rankine–Hugoniot relations
expressing continuity of the fluxes of mass, momentum and energy. The Mach numbers are and . A genuine shock is one in which the two states differ; the trivial solution always satisfies the relations.
The specific entropy of a perfect gas is , with , so the entropy jump across the shock is .
For a genuine shock in a perfect gas,
The result itself. The jump formulas determine the post-shock state from the pre-shock state and a single number, the shock Mach number. They show that the compression ratio of a shock in a perfect gas is bounded (by for ) however strong the shock, that a strong shock converts a fixed fraction of the incoming kinetic energy into heat, and, through the entropy jump, that only compressive shocks are compatible with the second law of thermodynamics. The strong-shock downstream state is the input to the self-similar supernova blast-wave solution treated later in the same notes (§7).
Formalizing it. The results are classical and fully proved in the textbook sense; a search of the platform library found no existing formalization of them. The mission produces a reusable Lean vocabulary for one-dimensional perfect-gas shocks (enthalpy, sound speed, Mach number, Rankine–Hugoniot predicate, entropy jump) on which later missions on blast waves, oblique shocks or MHD shocks can build.
The individual steps are algebraic, but the Rankine–Hugoniot system is nonlinear and always has the trivial solution. Eliminating variables leads to a quadratic in the velocity ratio with roots and the shock root, so any derivation must use the hypothesis that the two states differ at exactly the right point; dividing by the trivial factor without that hypothesis is the standard mistake. The sign of the entropy jump is a genuinely analytic statement: it requires showing that a one-variable function of involving logarithms vanishes only at and has a definite sign on each side. The strong-shock statements are limits and need uniform control of the downstream state as .
All quantities are real numbers. The gas is a perfect gas with ; every statement about gas states assumes strictly positive densities, pressures and normal velocities, which matches the source's convention and makes all square roots, quotients and logarithms well-defined (Lean's total functions would otherwise return junk values, e.g. division by zero gives ). Only the normal, non-magnetic shock is treated; the shock is at rest, and the frame change to the upstream rest frame appears only through . The entropy is represented through its jump divided by . The genuine-shock hypothesis rules out the trivial solution, under which the jump formulas would be false for ; it is omitted only from the entropy-jump formula (A 28), which also holds for the trivial solution. The strong-shock limit "" is expressed as at fixed and , and "" as divergence to .
The definitions are collected in one shared file (namespace AstrophysicalFluidDynamics, intended to be reused by later missions on the same lecture notes). Only Mathlib's real analysis (logarithm, square root, limits) is needed. Contributions welcome: proofs of the milestones, and reusable lemmas such as the factorization of the Rankine–Hugoniot system through the trivial root.
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.Gambini and Pullin (IJMPD 23 (2014) 1442023) study quantum fields living on the discrete quantum spacetimes of spherically symmetric loop quantum gravity. Discreteness makes the field equations lattice-like and hence breaks Lorentz invariance. Collins, Perez, Sudarsky, Urrutia and Vucetich (PRL 93 (2004) 191301) argued that in interacting theories such Planck-scale violations feed, through renormalized loop diagrams, into large low-energy violations: a difference of second derivatives of the self-energy that should vanish by Lorentz invariance stays bounded away from zero. Gambini and Pullin argue that two exponential weights — a Gaussian fuzziness factor from the spread of the ADM mass, and a Lorentz-invariant nonlocal interaction factor of the type found in string field theory — make this quantity arbitrarily small.
Because the full self-energy calculation is lengthy, the paper's Appendix A replaces it by a two-dimensional model integral in which rotations play the role of Lorentz transformations and a parameter plays the role of lattice spacing. This mission formalizes the precise mathematical claims made about that model.
For real parameters define the denominator base and the model integrand
The paper's integral (A.1) is . For one has , which is rotation invariant.
(A.1) is only a formal expression: is not Lebesgue integrable on (for it decays like ; for it grows like along the -axis). The mission therefore uses the disk-truncated integral
which regularizes (A.1) in a rotation-invariant way.
The weighted model integral (A.2) is, for weights ,
The first factor models the fuzziness (it acts on one direction only), and the second models the nonlocal interaction (rotation invariant here, Lorentz invariant in the physical case).
"With suitable choices of and one can make the integral as small as desired":
In the paper this model is the only precisely stated mathematical content backing the claim that the two exponential weights restore approximate Lorentz invariance. Formalizing it pins down exactly which statements hold (and in what sense the formal integral (A.1) "vanishes" or "does not vanish"), separating the rigorous content of the toy model from the physical argument it illustrates. The results are elementary real analysis; no machine-checked proofs of them are known to exist.
The main difficulty is that the unweighted integral (A.1) diverges, so both "vanishes" and "does not vanish" need a regularization. The weighted statements need integrability and dominated-convergence estimates on and a change of variables (swapping and ) for the symmetry claims. The divergence to in milestone 2 needs separate upper and lower estimates for the positive and negative parts of on growing disks.
All objects are real-valued functions on with Lebesgue (product) measure. is a Bochner integral over the whole plane; where the integrand is not integrable, the Lean integral is by convention, which is why milestone 3 is included and all weighted statements assume . The disk is the closed Euclidean disk , not a sup-norm ball. The parameter is restricted to (or ) wherever it matters, so that . The sentence in the paper "more precisely one needs and both larger than " is heuristic; only its sufficiency direction along is formalized (milestone 5). No necessity claim is formalized, because a large alone already makes small.
Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance on a set is Hilbertian when can be mapped into a Hilbert space so that becomes the norm distance; for such a , the kernel is positive definite for and (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for : the map sending a measure to its quantile function is an isometry into , and between univariate Gaussians is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for and the -Wasserstein distance on is not Hilbertian (Proposition 8.2, p. 507).
The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar does not even embed into with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.
Let be a set. A function is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every , every and every with ,
A function is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space and a map with for all .
On with the Euclidean norm , let be the Borel probability measures with . A coupling of and is a measure on whose two marginals are and , and the -Wasserstein distance (2.18) is
finite on . For points and a histogram (nonnegative, summing to one) the discrete measure is ; for two histograms , is the set of nonnegative matrices with row sums and column sums , and (2.11).
The configuration of the book's proof consists of the corners , , , of the unit square, the 35 histograms of with entries in , and the centering matrix .
For and ,
A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for or on , , by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.
The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.
The abstract part is short: expanding and using gives milestone 1. The obstacle is the certificate. The book observes that has a positive top eigenvalue (about for and for ), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector for which the quadratic form is provably positive. For the costs involve , the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic to the discrete program (milestone 4) and transporting a counterexample from into (milestone 3), both of which require working with couplings as measures on a product space.
EuclideanSpace ℝ (Fin d); is the published definition WassersteinDRO.Duality.wassersteinDistance (an -valued infimum over all measures with the two marginals, raised to ), converted to a real number. The distance is considered on , the set where it is finite; outside it the real conversion is a junk . The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on and on every smaller set containing those measures.Fin n). Histograms are real vectors; the reduction milestone is stated for every .CompOT.NotHilbertian, duplicating chunk II of the series.Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of , and exact certificates for the grid computation.
Best subset selection with a ridge term, the -regularized least squares problem
is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.
Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, , studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.
Fix a design matrix , a response , parameters and a bound . Write and for for every .
The Big-M formulation (2) is
Its interval relaxation replaces by ; its optimal value is . Eliminating gives the equivalent form (37),
The reverse Huber penalty is for and for , and . The interval relaxation of has the value (6),
Let be the set of minimizers of , and, as in (9),
The comparison runs through the scalar function and through .
The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for and , .
Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small favours the Big-M relaxation and a large favours (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation beats both when , this motivates the paper's choice of as the formulation on which its BnB solver is built.
The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.
The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, , and at the sign of . The passage from coordinatewise inequalities to optimal values is where care is needed. is defined over pairs , and its identification with a minimum of over a compact box requires eliminating and showing attainment. For (11) a pointwise comparison of and on the box only bounds by the box-restricted value , not by , which is an infimum over all of ; the hypothesis is what closes this gap, and dropping it gives a statement the paper does not prove.
All declarations live in the namespace L0BnB.BigMvsPR. Vectors are Fin p → ℝ, is a Matrix (Fin n) (Fin p) ℝ, and is X *ᵥ β. Every norm is an explicit sum: , and is . The reverse Huber penalty is an if on .
Optimal values are real infima (sInf): over the feasible pairs of the interval relaxation, over all of , over the box. For each set of values is nonempty () and bounded below by , so no infimum takes Lean's junk value. is defined as the displayed minimum (6); its identification with the interval relaxation of is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. is the set of minimizers of , as the paper uses it in the proof of (11).
All theorems assume . The paper remarks that Proposition 2 applies for any ; is excluded because and divide by . The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of and is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.
The paper states no bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of ), and of the goal.
Scattered subspaces are a central object of finite geometry. An -subspace of an -dimensional vector space over defines an -linear set of the projective space , and when is scattered this linear set has the largest possible number of points for its rank. Maximum scattered subspaces give rise to maximum rank distance (MRD) codes, to translation caps, and to two-intersection sets and the associated two-weight codes and strongly regular graphs (Polverino 2010; Sheekey–Van de Voorde 2020).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) generalised the notion to -scattered subspaces, which meet every -dimensional -subspace in dimension at most , and proved that such a subspace has dimension at most unless it defines a subgeometry. This mission concerns the extremal case: subspaces attaining , and the way they meet hyperplanes.
Timeline.
Let be finite fields, , and let be an -dimensional vector space over , viewed also as an -dimensional vector space over . A hyperplane of is an -dimensional -subspace.
Fix an integer with . An -subspace of is -scattered if and every -dimensional -subspace satisfies . It is maximum -scattered if no -scattered subspace of has larger -dimension.
Put and suppose . For an -subspace of dimension , let be the number of hyperplanes with . The proof works with the Gaussian binomial coefficients , the -Pochhammer symbols , the elementary symmetric values of , and the sums
If is a maximum -scattered -subspace of of dimension , then for every hyperplane of
The result. Theorem 2.7 says that a maximum -scattered subspace of dimension has only possible intersection dimensions with hyperplanes. Its linear set therefore meets hyperplanes in few sizes, which links these subspaces to sets of few intersection numbers and to codes with few weights. Inside the paper, the upper bound is the input to §3: it shows that the Delsarte dual of a maximum -scattered subspace of dimension is maximum -scattered (Theorem 3.3). That theorem in turn gives maximum -scattered subspaces when does not divide .
Formalizing it. The theorem is proved in the paper, but no machine-checked version exists. Beyond the geometry, the mission produces a library of finite -series facts: Gaussian binomials as rational functions of , the -binomial theorem in both forms, Carlitz's inversion formula, and the elementary symmetric evaluation . Some of these are proved on the platform in a different Mathlib environment, but they are not available in this one. Counting statements about subspaces over finite fields (hyperplanes through a subspace, ordered independent tuples) are also needed and are reusable.
The lower bound is a dimension count. The upper bound is not: the obvious approach bounds from the scattered property alone, but the -scattered condition controls intersections with -dimensional subspaces, and hyperplanes have dimension , which is far larger. No pointwise argument is known; the paper determines the distribution only through its first moments, given by a double count, and then shows that a specific nonnegative combination of the vanishes. The moment identities hold only for (Lemma 5.7 needs each independent vectors of to stay independent over ), and closing the argument requires exact evaluation of a triple -series with signed Gaussian binomials and quadratic exponents.
F, a finite field K with [Algebra F K], and a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V). We take finrank K V, finrank F K and Fintype.card F.IsHScattered.Proofs of any milestone, of standard counting facts for subspaces of finite vector spaces, and of the -series lemmas are welcome.