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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
A metric tensor is a coordinate-free object, but every concrete exact solution of Einstein's vacuum equations is written down in coordinates, and the same spacetime appears in the literature in many charts: Schwarzschild in standard, Eddington–Finkelstein, Painlevé–Gullstrand and isotropic coordinates, Kerr in Boyer–Lindquist and ingoing form, and so on. Checking that a chart is a vacuum solution means computing the Ricci tensor of its metric components; checking that two charts describe the same solution means exhibiting a coordinate change and verifying that the metric components pull back. Release I of the Exact Vacuum Atlas (a separate, earlier mission) certified seven such charts (Minkowski ×2, Schwarzschild ×3, Kerr ×2) together with four coordinate relations.
Release II adds the missing method: a proof that the coordinate Ricci tensor used throughout the Atlas transforms as a tensor under any smooth coordinate change, so that a vacuum certificate can be transported along a coordinate relation instead of being recomputed. It then uses this to certify new Schwarzschild charts (Painlevé–Gullstrand, both signs; isotropic, both radial branches, in spherical and Cartesian form) and to give the Painlevé–Gullstrand certificate two distinct proof routes with an audited separation of their specified dependencies; they still share definitions, data and Mathlib.
All objects are coordinate-level data on open subsets of ( in every application):
a metric is a matrix of real functions, a candidate inverse is another such
matrix, and the coordinate Ricci tensor is defined by the usual Christoffel
formulas from partial derivatives of slices (definition bundle Atlas_Core_Basic of release I). A
vacuum certificate for on an open set records eight obligations: open and
nonempty, symmetric, on , and of class on , an explicit
Lorentz frame with (signature ), and all sixteen Ricci
components zero on . A coordinate relation records a smooth bijection with inverse
, a Jacobian matrix whose entries are genuine derivatives, and the pull-back identity
on . Mathlib provides real analysis, matrices and multivariable
calculus. In the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, the project did not find the complete indefinite-metric connection and Ricci definitions required by this development. The registered B3 coordinate definitions supplement that fixed version; this is not a claim about all current or future versions of Mathlib.
ExactVacuumAtlas.Release02.ricci_law)For any dimension , open sets , a smooth map with a genuine Jacobian and a right inverse ( on ), and regular metric data on (symmetric, genuinely invertible, ; no curvature condition), if and on then
The proof goes through the Christoffel transformation with its second-derivative term (the Christoffel symbols are not a tensor), the tensoriality of the matrix curvature (the and terms cancel), and the contraction to the Ricci tensor. The final Ricci theorem does not assume the Ricci transformation law. The intermediate curvature lemma has an explicit connection-transformation premise, which the proved Christoffel transformation discharges in the metric application. The registered Ricci tensor is not redefined.
certificate_transport — a vacuum certificate on , a coordinate relation , the explicit conditions that is open and nonempty, a right inverse of the genuine Jacobian on , and any genuine left inverse of yield a vacuum certificate on (all eight obligations, 4D).pg_route_direct — Painlevé–Gullstrand metric ,
, , certified on (regular-coordinate points with included when ; no global event-horizon statement)
by direct computation (release-II sprint 01).pg_route_transport — the same statement, proved a second time by transporting the
Eddington–Finkelstein certificate of release I along the PG↔EF relation. The independence of this
route is a constant-level dependency-closure audit (no PG table, PG certificate or PG root is reached),
not a conjunction of two proofs.control_direct, control_transport, control_witness — a non-vacuum control family: the
cylinder metric pulled back by (non-affine for , and the identity for ); the sixteen Ricci components
(, , , rest ;
, ) are proved twice (tables, and the transformation law from the
release-I cylinder values), with the nonzero witness at .isotropic_branches — the two radial relations between the isotropic chart
and the standard chart: outer branch () and inner branch
(), both onto .isotropic_main — isotropic Schwarzschild ,
, , certified for every on (both branches transported from the standard certificate and glued; is
Minkowski).isotropic_sph_cart_relation — the spherical ↔ Cartesian isotropic chart relation on the slit chart
( on the spherical side and on the Cartesian side), with and on both sides and on the spherical side, for every real . This is a relation of the specified coordinate data; the vacuum certificates below are restricted to .isotropic_cartesian — the Cartesian isotropic certificate
for every on the natural domain (no axis or slit cut: the slit
certificate is transported along the reflection and the relabelling
and the three domains are glued).pg_main, pg_coverage, pg_std_restricted — the sprint-01 PG roots: both signs; and the
regular data at for ; the PG↔EF relation on the whole domain and the composite standard → EF → PG relation on only.The transformation law is the reusable link between a full certificate in one coordinate representation and a certificate in another. Transport also discharges the required source-domain, inverse-matrix, regularity and Lorentz-signature obligations; a bare table of zero Ricci components alone is not treated as a full certificate.
The law is a long but elementary computation (second derivatives of the Jacobian, Cramer's rule for the
smoothness of the inverse Jacobian, symmetry of mixed partials, index bookkeeping over Fin n); the
isotropic charts need genuine inverse functions with square roots, arccos and a half-angle arctan,
with smoothness and bijectivity on explicit open domains. Nothing is stated at the manifold level.
Coordinate-level statements on open subsets of (the law itself on ). Not claimed: an identification with a Mathlib manifold Ricci tensor in the pinned development; any global, event-horizon or maximal-extension theorem; PG or isotropic vacuum certificates for negative mass; certification of (for this is the excluded degenerate isotropic sphere, while for it is the excluded origin); that the union of the two isotropic branches is a single bijection; that the inner branch is the interior .
Müller, T., Grave, F.: Catalogue of Spacetimes, arXiv:0904.4184v3 (§2.2.3 isotropic, PG); Martel, K., Poisson, E.: Regular coordinate systems for Schwarzschild and other spherical spacetimes, arXiv:gr-qc/0001069; Carroll, S.: Lecture Notes on General Relativity, arXiv:gr-qc/9712019 (§3, transformation of the connection and curvature); release I of the Exact Vacuum Atlas (platform mission on this site).
New material of release II is released under Apache-2.0; the Kerr, release-I and third-party sources keep their recorded origins and licences. A public Git repository is not yet available: every node's source field cites the local release-candidate commit 11fb317259353b71a41d6daed466c495cffd7db4 with file, line range and SHA-256 of the staged file. Environment: Lean v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Local audits: no sorry, no native_decide; axiom closure ⊆ {propext, Classical.choice, Quot.sound}.
n、任意光滑坐标变换（真实 Jacobian J，显式右逆 K）与任意对称、真实可逆、
C^∞ 的旧度规（不要求真空），R'_{ij}(y) = Σ_{ab} J_{ai} J_{bj} R_{ab}(Φ y)。证明经 Christoffel 变换（含二阶导数项 K ∂J）、
矩阵曲率张量性、收缩。最终 Ricci 定理不把待证变换律作为假设；中间联络变换前提由已证明的定理提供；ricciOf 定义未改。CoordRelation + 源域开且非空 + Jacobian 的显式右逆 + 新度规的真实左逆 ⇒ 新证书（八项逐字段），四维。M ≥ 0、ε² = 1，整个 {r > 0, 0 < θ < π}（M > 0 时包含域内 r = 2M 的正则坐标点），第一阶段表格直接计算。P ∧ P。λ ≠ 0 时非仿射，λ = 0 时为恒等映射） β ↦ β + λ sin α 拉回；16 个 Ricci 分量由表与变换律各证一次：
R₂₂ = 1+λ²c²s²、R₂₃ = R₃₂ = λcs²、R₃₃ = s²、其余 0；λ = 1 时 R₂₃(0,1,π/4,0) = √2/4 ≠ 0；λ = 0 为恒等映射。ρ > M/2（M ≥ 0）、内支 0 < ρ < M/2（M > 0），都映到 r > 2M；互逆、真实 Jacobian、拉回均已证。M ≥ 0，域 ρ > 0, ρ ≠ M/2, 0 < θ < π；两支分别由标准证书传递后并域；M = 0 为 Minkowski。ρ > 0, ρ ≠ M/2；球坐标另有 0 < θ < π, −π < φ < π，Cartesian 一侧另有 r_xy + x > 0；fromCart 用 arccos 与半角 arctan；对所有实 M 成立（不推出负质量真空证书）。M ≥ 0，域 ρ > 0, ρ ≠ M/2，无极轴/切口限制：slit 证书经反射与循环重标传递并并域。M = 0 特例，以及 M > 0 时 r = 2M 正则坐标点的覆盖；PG↔EF 在整个域的双向关系；正向为 standard → EF → PG 的合成关系只在 domStd（r ≠ 2M），单独标示。不声称：流形/全局事件视界/最大延拓；PG或isotropic的负质量真空证书；在ρ = M/2处的证书（M>0为排除的退化球面，M=0为排除的原点）；ricciOf 等于 Mathlib 流形 Ricci；两支并域是一个双射；内支是 r < 2M。
The value of a Dirichlet -function at controls class numbers of quadratic fields, the least quadratic non-residue, and the distribution of primes in arithmetic progressions. For a real character modulo the size of is governed by the zeros of near : a real zero close to (a Siegel zero) would make abnormally small, and no unconditional argument rules this out effectively.
Littlewood's bound (1928) states that under the generalized Riemann hypothesis for ,
which is optimal up to the constant. Explicit constants under GRH were given by Lamzouri, Li and Soundararajan (2015).
The mission The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8 formalizes a preprint (OpenAI, 30 September 2026) claiming that every Dirichlet -function is zero-free in . That claim is not yet verified. This mission asks what a zero-free half-plane would give: an explicit Littlewood-type lower bound for under the hypothesis for the single character concerned.
Timeline.
A Dirichlet character modulo is a multiplicative function that vanishes off the units. It is primitive if its conductor equals , and real if all its values are real (they then lie in ). Its -function is
continued meromorphically to , with a pole only for the trivial character. For a primitive character modulo the continuation is entire and .
The hypothesis used throughout is
It concerns one character, not a family, and the half-plane is open. For primitive , GRH for implies .
There are constants and such that for every primitive real character modulo satisfying ,
For the constant is admissible:
For the same and ,
With (Mertens' constant), for every real ,
For every primitive character modulo and every with ,
The result. A zero-free half-plane at a fixed distance from makes the Littlewood bound effective with explicit constants. Through the class number formula it gives explicit lower bounds for class numbers of quadratic fields of large discriminant, and it excludes Siegel zeros for the character concerned. The hypothesis is weaker than GRH, and, if the 7/8 preprint is correct, it holds for every primitive character. In that case the goal and the explicit milestones become unconditional explicit theorems.
Formalizing it. The explicit bounds are proved in the preprint by Daugherty, Ryan and Ward (doi:10.5281/zenodo.23400116, Theorem 2), with constants certified in interval arithmetic. None of the statements here has a machine-checked proof. A formalization would give an independently checked conditional result that composes directly with a Lean proof of the zero-free half-plane. It would also add explicit analytic number theory to Mathlib: the convexity bound, explicit prime-sum estimates, and logarithms of -functions on zero-free regions.
The classical proof of Littlewood's bound under GRH uses the zeros' location on the critical line to bound just to the left of . Under the weaker hypothesis only a fixed strip next to is zero-free, and grows like there. The control must be strong enough that an exponentially smoothed prime sum of length dominates, with every constant explicit and uniform in . The prime sums in turn need explicit, not asymptotic, estimates for .
The -function is Mathlib's DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and "real" is stated as for every . The value is compared through its real part, and the two-sided milestone uses the principal complex logarithm. Mertens' constant is written out as with Mathlib's tsum over primes. The hypothesis is a hypothesis on the single character in each statement, never a family-wide assumption. It is satisfiable, for example under GRH, so the conditional statements are not vacuous.
A complete development needs:
The convexity bound and the prime-sum estimates are reusable well beyond this mission. Contributions toward any of these are welcome.
A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.
The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.
The item space is a compact subset of with restricted Lebesgue measure . There are buyers. Buyer has a budget and a nonnegative integrable valuation density with . The utility of a bounded nonnegative bundle is . An allocation is feasible when almost everywhere. It is pure when each equals the indicator of a measurable set , up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.
A nonnegative integrable price density defines a buyer's affordable bundles by . A market equilibrium is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and . Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, , maximizes weighted log utility over feasible allocations. Its dual program, , minimizes total price minus weighted log multipliers subject to almost everywhere Gao and Kroer, pp. 6–8.
The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector and price almost everywhere, and the equivalence
The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set , proving that is compact and convex and equals the pure utility set . Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula . These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.
The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.
Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.
These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.
The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.
Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.
Lean uses real valued measurable functions on the ambient Euclidean space with measure . It identifies prices and allocations up to almost everywhere equality, as the paper identifies and equivalence classes. Bundles must belong to and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.
The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's objective convention. The maximization over buyers is the finite supremum . Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring everywhere. Corollary 3 explicitly requires each denominator to be positive. Lemma 4 alone assumes the normalizations and , which the paper recalls before its statement.
The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.
In a two-player one-round nonlocal game, a verifier samples a pair of questions, sends one to each of two players who cannot communicate, and accepts or rejects the pair of answers. The players may share an arbitrary quantum state and measure it; the entangled value of the game is the supremum of their acceptance probability over all such strategies. Nonlocal games are the operational form of Bell's theorem, the model behind device-independent cryptography and self-testing, and the engine of the complexity class of languages decidable by a polynomial-time verifier interacting with entangled provers (Cleve, Høyer, Toner, Watrous, 2004, arXiv:quant-ph/0404076).
With classical provers, multiprover interactive proofs decide exactly (Babai, Fortnow, Lund, 1991, doi:10.1007/BF01200056). For entangled provers the lower bounds grew in steps: (Ito, Vidick, 2012, arXiv:1207.0550), (Natarajan, Wright, 2019, arXiv:1904.05870), and finally (Ji, Natarajan, Vidick, Wright, Yuen, 2020, arXiv:2001.04383): every recursively enumerable language, the halting problem included, has a two-prover one-round interactive proof with entangled provers, and the entangled value of a game cannot be approximated by any algorithm. Through the equivalences of Fritz (2012, arXiv:1008.1168), Junge, Navascués, Palazuelos, Pérez-García, Scholz, Werner (2011, arXiv:1008.1142) and Ozawa (2013, arXiv:1212.1700), the theorem gives a negative answer to Tsirelson's problem and to Connes' embedding problem for von Neumann algebras.
Everything below is defined from scratch; the formal development uses exactly these objects.
A synchronous game has a finite question alphabet and a finite answer alphabet , shared by both players, a probability distribution on , and a decision predicate which, on equal questions , rejects every pair of unequal answers .
A synchronous strategy of dimension assigns to each question a projective measurement on : positive semidefinite matrices summing to the identity, each idempotent. Both players use the same measurements, and probabilities are taken in the normalized trace . The value of the strategy is
the acceptance probability when the players measure a maximally entangled state of dimension . The synchronous value is the supremum of over all synchronous strategies of all dimensions. A synchronous strategy is a tensor-product strategy, so , the entangled value.
A game description is a finite object from which a synchronous game is read off: natural numbers fixing and , a finite list of weighted question pairs and a finite list of accepted tuples . The game has proportional to the total weight listed for (the point mass at if the total weight is zero), and accepts exactly the listed tuples, except that unequal answers to equal questions are rejected. Descriptions are coded as natural numbers, so a map from machines to descriptions can be computable.
Turing machines are Gödel numbers of partial recursive functions, an equivalent model of computation; " halts on the empty input" means that applied to is defined.
There is a computable map from machines to game descriptions such that for every machine ,
This is Theorem 12.2 of arXiv:2001.04383 in synchronous form, with the running time of relaxed from polynomial to computable. It leaves the running time and the choice of value unfixed, and it is the weakest statement that already makes the game value uncomputable: no algorithm decides whether a game has synchronous value or at most .
The paper's statement has computable in polynomial time, and both the synchronous and the entangled value satisfy the two clauses. With polynomial time the goal gives for the class of two-prover one-round proofs with completeness and soundness , and with the elementary inclusion this is . These statements need a model of polynomial time and a definition of tensor-product strategies, and will be added as milestones once those definitions are published here.
The result. Approximating to within a constant is as hard as the halting problem. A hierarchy of semidefinite programs converges from above to the commuting-operator value , so the two values cannot coincide for every game: a negative answer to Tsirelson's problem and, by the equivalences cited above, to Connes' embedding problem, open since 1976. On the complexity side, is the exact characterization of the power of entangled provers.
Formalizing it. The theorem is proved and its proof is machine-checked: HaltingGameValue.halting_reduces_to_gameValue in the Lean 4 development vidick/MIPRE-formalization proves exactly the goal above over Mathlib, with propext, Classical.choice and Quot.sound as its only axioms. The development is about 1,200 modules and 410,000 lines, including vendored components and a separate library for the low individual degree test; its blueprint records every statement, the dependency graph and the correspondence with the paper. This mission makes the result a fixed, auditable target: the definitional layer above is written over Mathlib alone, so the goal can be checked from first principles, and the components of the proof whose developments are self-contained are published as milestones with their proofs, to be imported, reused and re-proved. The first milestone, the recursive compression lemma of Marks, Nezhadi and Yuen (Lemma 5.1 of their manuscript; blueprint node lem:recursive-compression), comes with a complete proof over a dependency tree of 22 definition bundles and 60 theorems: a cost model of computation, an efficient universal machine, the s-m-n and Kleene recursion theorems, succinct descriptions.
The obvious approach fails at once: a verifier runs in time polynomial in its input, while a machine may run for arbitrarily long before halting, so no fixed game can check halting by simulation. What makes reachable is gap-preserving compression: a polynomial-time transformation of verifiers such that the compressed verifier, at index , has value when the original verifier at index does, and value at most when the original does. The compressed game is exponentially cheaper than the game it certifies, and a fixed-point argument through Kleene's recursion theorem, in the abstract form of the recursive compression lemma, turns compression into the halting reduction. Compression rests on three components, each with a central ingredient that is a theorem in its own right: question reduction by introspection, in which the players sample their own questions and a Pauli basis self-test built on the quantum low individual degree test certifies that they did; answer reduction, in which the players prove through a probabilistically checkable proof that their answers would have been accepted; and gap amplification by parallel repetition. In each component soundness must hold against strategies of unbounded dimension, where no finite enumeration or compactness argument is available, and the quantitative losses must compose so that the threshold is preserved exactly.
The goal is stated with the synchronous value, projective measurements on with , and the normalized trace in place of a state vector; the real part of the trace is taken in the strategy value, and the synchronous value is the supremum, in , over all strategies of all dimensions (the values lie in ). Game descriptions are interpreted with the fallback distribution above, so that the interpretation is total. Machines are Mathlib's Nat.Partrec.Code and computability is Mathlib's Computable; polynomial time is not fixed by the goal.
No trivializing formalization is available: the game depends on only through , and the two clauses demand values and at most on complementary sets of machines, so no map that ignores its argument, or produces only descriptions of zero total weight, satisfies the statement.
A complete development needs four layers: (i) a model of computation with costs, with polynomial-time maps, an efficient universal machine, the s-m-n and Kleene recursion theorems and succinct descriptions, which is the recursive compression milestone's dependency tree and is reusable in any undecidability argument by compression; (ii) normal form verifiers, conditionally linear samplers, the Pauli basis test and the quantum low individual degree test; (iii) the three transformations, with answer reduction over a PCP decider built from a succinct Cook–Levin theorem and direct parallel repetition in value form, and their soundness; (iv) the halting reduction from compression and the passage from the tensor-product to the synchronous value. Statements and proofs of these components over the shared definitional layer are welcome, as are alternative proofs of the goal from the same definitions, the polynomial-time and entangled-value strengthenings, and the inclusion .
MIPRE/HaltingGameValue.lean, proof MIPRE/MainTheorem.lean) and its blueprint.Impact investing selects securities by a non-financial score, an ESG rating, a carbon intensity, a measure of social benefit, and asks whether such a selection earns an excess return. A. W. Lo and R. Zhang (SSRN 3944367; published in Management Science, DOI 10.1287/mnsc.2022.01168) model the score as an impact factor and study the returns of securities ranked by with the tools of induced order statistics (concomitants), introduced by Bhattacharya (1974) and David (1973).
Section 4.3 of the paper gives an equilibrium reading of the apparent excess return. In a -factor asset-pricing model with no mispricing, an investor who accounts only for the first factor sees the contribution of the omitted factors to security 's return as alpha. If the impact factor is correlated with these omitted factors, ranking by impact selects omitted-factor risk, and the selected portfolio appears to earn an excess return. Empirical studies of sin stocks (Blitz and Fabozzi, 2017) and ESG scores (Madhavan, Sobczyk and Ang, 2021) report exactly this effect. Proposition 5 quantifies it in closed form.
There are securities. For security , is its impact factor and the total net contribution of the omitted factors to its return. Write and , random vectors on a probability space .
Order statistics. Sorting the entries of increasingly gives , the order statistics of . If is the sorting permutation, , and the induced order statistic is the omitted-factor return of the security with the -th smallest impact factor. The order is induced by , never by (display (6), p. 11).
Assumption (A2) (p. 19). The vector is Gaussian with exchangeable first and second moments: , , , , , and for , , , . The paper normalises and and keeps a free premium . The adjusted correlation is
Under (A2), for every rank and every pair of ranks ,
The goal states (27) with the factor on the last term. The paper prints without it. That is a slip: replacing by with multiplies the left side by and leaves every correlation unchanged, so the printed formula fails whenever . With , the correct value is , which is the goal's right side.
The result. Proposition 5 shows that the apparent alpha of the security ranked -th by impact is . A selection rule that looks unrelated to return characteristics still produces nonzero excess returns when it is correlated with omitted priced factors, and the size of the effect is governed by the single number . The authors use this to argue that impact estimates are unreliable until all known factors are accounted for, and that a persistent impact premium may signal a new factor (an "ESG factor" or a "carbon factor"). The variance and covariance formulas give the risk of any portfolio of impact-ranked securities, through the moments of Gaussian order statistics.
Formalizing it. The paper proves (25) in full and states that (26)–(27) "can be proven similarly"; the printed (27) is off by the factor . A machine-checked proof settles the corrected constants. No part of this result, and no theory of induced order statistics, is formalized in Lean or elsewhere to our knowledge. The development needs a usable library on concomitants of Gaussian order statistics, which would serve the rest of the paper (Propositions 2, 4 and 6) and the data-snooping analysis of Lo and MacKinlay (1990), which uses the same tools.
The mean formula looks like linearity of expectation, but is evaluated at a random index that depends on , so is not for any fixed . The decomposition of milestone 1 is what handles this. It requires the full joint Gaussian law of , because uncorrelated is not independent otherwise. It also needs a correction term through the cross-sectional average, because the cross-correlations and make depend on all of . In Lean, the sorting permutation must be shown measurable in , and the moments of the order statistics must be shown finite.
Fin N → Ω → ℝ on a probability space. (A2) is the predicate IsA2: joint Gaussianity of the -vector (Mathlib's HasGaussianLaw on (Fin N → ℝ) × (Fin N → ℝ)), plus the moments (22)–(23) stated as covariances with .IsA2. is free.Fin N): Lean's rank is the paper's . Sorting uses Tuple.sort, which breaks ties by index; ties have probability zero and the statements hold for any tie-breaking rule. Moments are Mathlib's integral, variance and covariance. The milestones use where the page writes in .Tuple.sort as a function of the data; integrability and moments of Gaussian order statistics; moments of a vector independent of read at an -dependent random index. Each of these is reusable well beyond this mission.A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry.
The mission "Plasticity: c₀ and c₀₀" proved, among other things, that a nonexpansive bijection from the unit ball of a space between and onto the unit ball of a space between and is a signed permutation of coordinates whenever the target matches signs (card Plasticity.CUB37).
A scan of unused hypotheses showed that the first step, the normal form, never uses that the target lies in .
This mission records the consequence: the target may be any space between and , because the existence of such a bijection forces it into .
is a linear subspace with and one with , both real with the supremum norm, for arbitrary index sets (definitions Plasticity_SeqSpace).
is a nonexpansive bijection of the closed unit ball of onto that of ; nothing is assumed about its inverse.
The milestone excludes nonexpansive bijections onto balls that the usual extreme-point argument cannot reach: for the ball has no extreme points, yet no ball between and is mapped onto it by a nonexpansive bijection.
The goal is the card Plasticity.CUB37 without its target hypothesis.
The normal form for targets inside is a separate card (Plasticity.SeqSpace.exists_signed_permutation_inward), the proof of Plasticity.CUB37.normal_form with the unused hypothesis removed; the goal then imports the Proved card Plasticity.CUB37.
Many service relationships let a firm pause an agent instead of firing them: a sales representative who brings in no customers for a while is suspended, a contractor is laid off for a season and recalled. Pausing is not free. Every restart carries a switching cost (re-training, re-establishing a territory, setting up the work environment), so a principal who suspends too readily pays for it. Cao, Sun and Tian (Management Science, 2024) study the optimal dynamic contract for this trade-off in continuous time, building on the Poisson-arrival moral-hazard model of Sun and Tian (2018). Their main result (Theorem 2) splits the parameter space into three regimes: never hire, hire and keep the agent working forever, and a control-band contract with suspension episodes of fixed length. This mission covers the first regime under the paper's Condition 1.
A principal earns a revenue per arrival of a Poisson process. Without effort the arrival rate is ; an agent who works, at private cost per unit time, raises it to . Write . The principal's cost rate while the agent works is , every start of work costs , and the principal and the agent discount at rates . Assumption 1 is . The derived constants are
The state of a contract is the agent's promised utility . The paper's verification theorem reduces optimality to a pair of functions: for the working state and for the suspended state. For a function on , with its left derivative, the operators are
and satisfies the optimality condition (20)–(22) if , , on , and , .
The working-state candidate is built from the delay differential equation (25): for , is the function on with
and for . may be convex near ; is the point up to which , and the concavification replaces on by its tangent line at . Condition 1 is " or " with
Under it there is a unique with (Lemma 3). Three hats occur in the paper: of Definition 1 (a payment threshold), of Lemma 3 (used here), and of Proposition 6 (not used here). For , Lemma 4 gives a tangent pair : the line touches at . Finally (K1).
Under Condition 1 and , for the pair of (29),
satisfy (20)–(22).
Propositions 2 and 3 are the analytic certificates behind Theorem 2(i): combined with the verification theorem (Theorem 1), they show that under Condition 1 and the principal's utility from any incentive-compatible contract promising is at most , so never hiring the agent is optimal, and is exactly the switching-cost threshold of that regime. The same objects (, , the tangent pairs) reappear in the low-cost control-band regime (Propositions 6–7), so a formal development of the delay ODE and its concavification is reused there.
The paper proves all these results; none is formalized. The mission formalizes the deterministic half of the guess-and-verify argument. The stochastic contract model (point processes, promise keeping, incentive compatibility), Theorem 1 and the optimality theorems are outside its scope.
The obvious approach, verifying (20)–(22) by direct computation, works for the linear pieces but not for , which has no closed form: (25) is a delay equation solved backwards from in steps of length , and the closed form (EC.52) of the paper holds only on the last step . Every property of used in the goal (monotonicity, the single change of convexity, the comparison in that makes unique) has to be extracted from the equation itself, across the kinks of . On the second branch of , is not a pointwise identity either: it requires , which is where enters.
ℝ → ℝ; every statement quantifies over only. In , is the left derivative (derivWithin f (Set.Iic w) w, the paper's p. 15 convention); in statements about and , derivatives are taken within ; in (25), within .Needed infrastructure: existence and uniqueness for linear ODEs with a terminal condition, extended step by step across a delay; one-sided derivatives of piecewise functions; concavity from sign conditions on second derivatives. Proofs of the milestones, and reusable lemmas about delay equations of this form, are welcome.
Online platforms such as ride-hailing, delivery and marketplace companies routinely test a new policy (a pricing rule, a dispatching algorithm) by switching it on and off over time on a single unit, a city or a market, rather than by randomizing over users. These switchback experiments avoid the interference that user-level randomization creates in two-sided markets, but they face a different problem: a treatment administered at one time keeps affecting outcomes for several periods afterwards (carryover effects). Bojinov, Simchi-Levi and Zhao, Design and Analysis of Switchback Experiments (arXiv:2009.00148, Management Science 69(7), 2023), derive the minimax-optimal design when the carryover lasts at most periods, and then ask how to do inference with it. This mission formalizes the inference half: under the optimal design, the Horvitz–Thompson estimator of the lag- effect is asymptotically normal as the number of epochs grows, which is what justifies the paper's normal-approximation test and confidence intervals.
The result is a finite-population central limit theorem: the potential outcomes are fixed, non-random numbers, and all randomness comes from the experimenter's coin flips. It belongs to the line of design-based limit theorems of Li and Ding (2017), Aronow et al. (2017) and Bojinov et al. (2021). Its probabilistic engine is the central limit theorem of Romano and Wolf (2000) for triangular arrays of -dependent random variables, which goes back to the -dependent central limit theorem of Hoeffding and Robbins (1948).
There are time periods . An assignment path records treatment () or control () in each period. The potential outcomes are real numbers . They are assumed non-anticipating (Assumption 1: depends only on ) and to have -carryover effects (Assumption 2: for , does not depend on ). Assumption 3 bounds them: . Write and for the outcome after consecutive treatments, respectively controls. The lag- causal effect is
A regular switchback design flips an independent coin with success probability at each randomization point , and every period copies the most recent coin. The Horvitz–Thompson estimator weights the observed outcome at time by the inverse probability that the last assignments were all treatments (respectively all controls).
In the -replica experiment , and the optimal design of the paper's Theorem 2 uses fair coins at
The periods split into blocks , , with block sums , and block errors , so that . Assumption 4 (non-negligible variance) requires for some and all large .
For fixed , under Assumptions 1–2, Assumption 3 with one bound for all , and Assumption 4,
The statement fixes no rate and does not require to converge.
Corollary 1, the conservative bound with the unbiased estimator , and Corollary 2(i), that (10) still holds when the design is built for an overestimated order .
Theorem 3 is what turns the optimal design into a usable inferential procedure: together with Corollary 1 it gives the test statistic and its normal -value, a conservative large-sample test of the null of no lag- effect that needs no model for the outcomes. Corollary 2 extends the guarantee to a misspecified carryover order . Lemma EC.1 is a general tool, applicable to any statistic that decomposes into a sum of weakly dependent pieces, such as block designs, time-series bootstraps and spatial experiments.
The paper proves these results. None of them is formalized: Mathlib has the central limit theorem for i.i.d. sequences only, and no central limit theorem for dependent arrays exists on the platform. The work here is to formalize the known proof: the exact second-moment computations of the design, the 1-dependence of the blocks, and a proof of the Romano–Wolf theorem itself, which the paper takes from the literature.
The randomness is a finite set of coin flips and the outcomes change with , so no i.i.d. structure is available: the block errors are neither independent nor identically distributed, and the classical Lindeberg–Lévy theorem does not apply. The obvious reduction, treating neighbouring blocks as independent, fails, because adjacent blocks share a coin. This is why the cross terms appear in (10), and why a dependent-array central limit theorem is needed. The variance normalisation is random-design specific and may oscillate in , so the limit theorem has to be proved with a self-normalisation that does not converge. Lemma EC.1 is the main obstacle: a -dependent central limit theorem for triangular arrays with Lyapunov-type moment conditions, which is not in Mathlib.
A path is a function ℕ → Bool of which only is read; potential outcomes are ℕ → Path → ℝ. The design law is encoded as independent coins at the randomization points, mapped to paths; in the -replica experiment the probability space is the uniform measure on the coin vectors of . Row of the sequence has and potential outcomes Y n. Rows exist in Lean but are degenerate and irrelevant to the limit. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is gaussianReal 0 1. and are explicit constants with an eventual threshold. The estimand, estimator and variance in the goal are the model's definitions, not a hand-written formula in the coins.
Three hypotheses are added to the printed statements, each necessary and disclosed in the item's Formalization Note:
The goal does not assume 1-dependence, the variance formula or any condition of Lemma EC.1; those are milestones, so the goal cannot be discharged by a hypothesis.
A complete development needs:
The last two, Lemma EC.1 and Definition EC.1, are reusable well beyond this mission. Contributions to any milestone, including alternative proofs of Lemma EC.1, are welcome.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic.
The mission "Plasticity: unit spheres covered by finite-dimensional faces" proved that a nonexpansive bijection between unit balls carries every finite-dimensional face of the target ball back onto a face of the same dimension (card Plasticity.Faces.matchesFace_of_finiteDimensional, stated for normed spaces), and that is a linear isometry whenever the target sphere is covered by finite-dimensional faces, for Banach spaces.
That covering theorem was proved through a sphere-preservation theorem whose proof needs completeness.
This mission removes completeness from the covering theorem and its plasticity corollary, by the ending that Angosto, Kadets and Zavarzina (2019) used for polyhedral faces.
and are real normed spaces, not necessarily complete, with closed unit balls and unit spheres .
A sphere face of is a nonempty convex set that is an extreme subset of (definitions Plasticity_Faces).
is a nonexpansive bijection; nothing is assumed about the continuity of .
The result. Completeness plays no role in the mechanism: the face theorem already holds for normed spaces, and the ending needs only the geometry of planes and the Mazur–Ulam theorem. The steps are: maps into ; by induction on the face dimension, is isometric on each scaled preimage face along chords that end at boundary points where it is already homogeneous (Zavarzina's Lemma 2.5, proved here by differentiating one inequality at a point of a plane where the norm is differentiable along a line, which Rademacher's theorem supplies), and two points of a face at equal distances from all its boundary points coincide, so is homogeneous on every ray; then is an isometry of the balls, and its homogeneous extension is linear by Mazur–Ulam.
Formalizing it. The face theorem is a Proved card in the earlier mission; this mission adds the ending, so that the statements are machine-checked in their natural generality.
Real scalars; the face theorem Plasticity.Faces.matchesFace_of_finiteDimensional and the basic facts Plasticity.BallMap.* are imported Proved cards.
New inputs are separate cards: Zavarzina's isometry lemma for homogeneous points (Plasticity.BallMap.norm_map_sub_map_eq_of_map_smul, using Rademacher's theorem from Mathlib for the density of smooth points), two elementary facts about relative boundaries of bounded sets, and homogeneity on preimage faces (Plasticity.Faces.map_smul_of_map_mem_face).
Statements are not to be weakened by assuming completeness, continuity of the inverse or a bound on the face dimensions.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. They proved it for strictly convex spaces, whose unit sphere consists of one-point faces. Angosto, Kadets and Zavarzina (2019) proved it, in the stronger two-space form, when the unit sphere is a union of finite-dimensional polyhedral extreme subsets: then every nonexpansive bijection from the unit ball of any Banach space onto that ball is an isometry. This mission formalizes a theorem that removes the polyhedrality: it suffices that every point of the sphere lies in some finite-dimensional face, of any shape, for instance a round disc. The results come from an unpublished research project on the plasticity problem.
and are real normed spaces with closed unit balls and unit spheres ; the covering and plasticity forms assume them complete. A sphere face of is a nonempty convex set that is an extreme subset of : if a point of lies in the open segment between two points of , both points lie in . Its dimension is that of its affine hull; and are its relative boundary and its extreme points. is a nonexpansive bijection; nothing is assumed about the continuity of .
The result. For a polytope face, the relative boundary is a finite union of smaller polytopes, so an induction on dimension keeps the preimage of the boundary compact; this is the step of Angosto–Kadets–Zavarzina that needs polyhedrality. For a curved face the boundary has a continuum of extreme points, and the inverse map, not known to be continuous, could a priori scatter their preimages. The new step traps the whole boundary preimage in one compact face: the preimage of a relative-interior point is shown to lie strictly between any boundary preimage and another one, by following a path across the scaled boundary, which the induction hypothesis covers exactly. Spaces such as -sums of a Euclidean space with a three-dimensional space whose ball is a cylinder have only finite-dimensional faces, some of them discs, and are covered by the new theorem but not by the polyhedral one or by strict convexity.
Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought.
The covering form ends with the project's theorem that a nonexpansive surjection between unit balls mapping the sphere into the sphere is linear, already formalized (card Plasticity.U10); this is the only step that uses completeness.
No regularity of the inverse map, no strict convexity, polyhedrality or separability is assumed, the face theorem does not assume completeness, and the faces may have any finite dimension. The topology needed is classical but absent from Mathlib: invariance of domain and of dimension, and the impossibility of retracting a ball onto its boundary sphere.
Real scalars. Faces are expressed with Mathlib's IsExtreme, dimensions as Module.finrank ℝ (vectorSpan ℝ C), relative boundaries as intrinsicFrontier ℝ C (definitions Plasticity_Faces).
A ball map is a function F : X → Y constrained on the closed unit ball by Set.BijOn and LipschitzOnWith 1; the preimage of is closedBall 0 1 ∩ F ⁻¹' C.
The plasticity form uses HasPlasticUnitBall (definitions Plasticity_Basic).
Statements are not to be weakened by assuming continuity of the inverse, polyhedrality or a bound on the face dimensions.
Published inputs (the basic facts of Zavarzina's Theorem 2.3, invariance of dimension, no retraction) are separate cards.
Exact vacuum solutions of Einstein's equations are the reference objects of classical general relativity: Minkowski space (flat spacetime), the Schwarzschild solution (1916, static spherically symmetric vacuum) and the Kerr solution (1963, stationary axisymmetric vacuum) are the metrics against which every statement about gravitational fields, black holes and gravitational waves is calibrated. Each of them is written in several coordinate systems, and the catalogue literature (Müller–Grave, Catalogue of Spacetimes, arXiv:0904.4184; Visser, The Kerr spacetime: a brief introduction, arXiv:0706.0622) lists these forms side by side. The verification that a given coordinate expression is Ricci-flat, and that two expressions of the same solution are related by an explicit coordinate change, is routinely delegated to computer algebra and is almost never printed.
Timeline: Schwarzschild (1916) found the static solution; Eddington (1924) and Finkelstein (1958) gave the coordinates
regular across ; Kerr (1963) found the rotating solution in the ingoing form used here; Boyer and Lindquist (1967)
introduced the coordinates of the standard form. A previous Prove2Me mission (Kerr Vacuum Solution Verification in
Boyer–Lindquist Coordinates, root KerrBL.vacuum_Kerr, 21 theorems, all Proved) established the coordinate
Ricci-flatness of the Boyer–Lindquist form; this mission reuses two of its published theorems and two of its definition
bundles unchanged (the remaining nodes stay their platform-side dependencies).
A coordinate point is (in Lean, a function ). A coordinate metric is a matrix of real functions of ; a candidate inverse is another such matrix. The slice derivative is the derivative of at ; on the open domains used here every slice is , so is the genuine derivative. With
(definition bundle Atlas_Core_Basic), the vacuum certificate for a set
asserts: is open and nonempty; is symmetric on ; on ; all components
of and are on ; at every point of there is an invertible matrix with
(Lorentzian signature, bridged to Mathlib's signature of the
quadratic form); and every component vanishes on . A coordinate relation
asserts: on ,
on , maps bijectively onto , is on and on , every entry is the
genuine derivative of the slice , and on . Units
, signature , , .
These definitions form the registered local definition layer of the project: the pinned Mathlib has no Lorentzian metric,
Levi-Civita connection or Ricci tensor, so they are supplied as reviewed coordinate-level definitions on top of Mathlib's
deriv, ContDiffOn, Matrix and quadratic-form signature.
ExactVacuumAtlas.Release01.main)where is with the explicit candidate inverse of
each row, and R1–R4 are coordinate relations with explicit maps: R1/R2 standard Schwarzschild to ingoing/outgoing
Eddington–Finkelstein on with , resp.
(Jacobian determinant ; the logarithm is Mathlib's Real.log, for which when , so one
formula covers both sides of ); R3 Boyer–Lindquist to ingoing Kerr on with
, , , explicit
for all real (three branches of ; Jacobian determinant ); R4 spherical chart
to with the usual map (Jacobian determinant
).
ExactVacuumAtlas.Release01.coverage)For the EF domain contains a point with ; for the Boyer–Lindquist domain contains a point with ; for , the ingoing Kerr domain contains a point with ; at these points all Ricci components vanish. The certified domains are therefore not narrowed to an exterior region.
ExactVacuumAtlas.sigPos_sigNeg_four)A Lorentzian matrix in the frame sense has Mathlib signature , .
The result gives machine-checked coordinate Ricci-flatness for the seven standard forms of the three basic vacuum solutions, on explicit open domains whose conditions do not exclude the interior region of Schwarzschild ( for ), either sign of or negative for Kerr, the regular-coordinate portion of with (EF, ), or the points with at which and (ingoing Kerr); which of these sets are nonempty depends on the parameters, and the coverage theorem gives sufficient conditions. The Lorentzian signature is verified pointwise. The four coordinate relations are proved as explicit maps with explicit inverses and Jacobians, not as abstract existence statements.
Status: every item of the mission has a kernel-checked proof in the project (axioms propext, Classical.choice,
Quot.sound only; no sorry, no native_decide); nothing is open. The mission publishes a finished formalization.
What it does not contain: any statement about manifolds, atlases, event horizons, maximal extensions, causal
structure or global geometry; any classification claim about four-dimensional vacuum metrics; any coordinate-covariance
theorem for the coordinate Ricci tensor; any relation between it and a Mathlib manifold Ricci tensor (which does not
exist in the pinned Mathlib). The catalogue is a finite list of seven coordinate representations of three solutions.
The obvious route, a general tensor-calculus library (connection, curvature, pull-back functoriality) over Mathlib
manifolds, is unavailable: the pinned Mathlib has no indefinite-metric connection or curvature. Each coordinate representation has a complete formal certificate. The development combines direct coordinate
calculations with formally proved parameter specialisations and equality-based reuse: the Cartesian Minkowski,
Eddington–Finkelstein and ingoing Kerr rows are verified by direct coordinate calculations; the Boyer–Lindquist row
reuses the published KerrBL.ricci_flat_Kerr and KerrBL.ginv_mul_g_Kerr; the standard Schwarzschild row takes its
Ricci-flatness from the Boyer–Lindquist result at , and the spherical Minkowski row is transported from the
standard Schwarzschild certificate at , in both cases through proved componentwise equalities of the metric data
on the common domain. No coordinate-covariance theorem is used or claimed. The ingoing Kerr row is the hard case: the metric is non-diagonal (the radial coordinate
vector is null, , while for the covector is not null, since ), the Ricci components are rational functions whose vanishing holds only modulo ,
and every derivative must be a genuine derivative, never a default value of deriv. For R3 the antiderivative of
has three different closed forms depending on the sign of , all covered without restricting the
parameters.
Lean representation: coordinate metrics on as above; ContDiffOn ℝ ∞; Matrix (Fin 4) (Fin 4) ℝ;
Mathlib sigPos/sigNeg for the signature bridge. Conventions committed: , , coordinate order
, EF matrix entry (from ), ingoing Kerr entries read off
with the half-Hessian convention from Visser eq. (E:K1), (no identification). No
trivialising formalization: every domain is proved nonempty with explicit witnesses; the candidate inverse is verified,
never assumed; the Ricci tensor is built from the metric data, not hypothesised.
Reusable infrastructure: the core bundles (Atlas_Core_Basic, Atlas_Core_Certificate, Atlas_Core_Relation), the
diagonal-frame criterion isLorentzian_of_diag, the signature bridge sigPos_sigNeg_of_isLorentzian, and the
closed-form tables. Welcome contributions (not part of this release): Painlevé–Gullstrand, isotropic, Kruskal–Szekeres,
Kerr–Schild and Doran forms; Kasner, pp-waves, Taub–NUT; a coordinate-covariance theorem for the coordinate Ricci tensor.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball of c and, for c₀, under the extra hypothesis that the inverse map is continuous, reducing the general case to a normal form in which the map acts inwardly on each coordinate. This mission formalizes a proof that removes the continuity hypothesis, for c₀(Γ) and c₀₀(Γ) over arbitrary index sets and for nonexpansive bijections between the balls of two spaces sandwiched between c₀₀ and c₀. The results come from an unpublished research project on the plasticity problem.
For a set , is the space of bounded real functions on with the norm ; consists of the with finite for every , and of the finitely supported . A space between and is a linear subspace with , with the supremum norm; its closed unit ball is . A subspace realizes all sign patterns if for every countable and all signs () some has on ; does. A signed coordinate bijection is a map with for a bijection and signs .
The result. Leo's work reduced plasticity of the unit ball of c₀ to excluding the collapse of a coordinate in a normal form; the unit sphere of c₀ is neither strictly convex nor made of compact faces, and the argument here is the base case of the project's results on c₀-sums of finite-dimensional blocks. The two-space statement CUB37 also shows that for an infinite index set Δ no nonexpansive bijection maps the ball of c₀₀(Γ) onto the ball of c₀(Δ).
Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. The development needs two classical topological inputs that Mathlib lacks: the theorem of Freudenthal and Hurewicz that a nonexpansive bijection of a compact metric space is an isometry, and a form of invariance of domain in every finite dimension (from Brouwer's fixed-point theorem).
The ball of c₀ is not compact and its unit sphere has large flat faces, so the classical arguments (compactness, strict convexity, smoothness of the norm) do not apply, and no regularity of the inverse map is assumed. The difficulty is concentrated in excluding that the normal form sends a nonzero coordinate to zero.
Real scalars, arbitrary index sets (no countability or nonemptiness assumed).
is Mathlib's lp (fun _ : Γ => ℝ) ⊤; and are submodules of it (definitions Plasticity_SeqSpace), and a ball map is a function on constrained on ballIn X by Set.BijOn and LipschitzOnWith 1.
CUB35 and CUB36 use HasPlasticUnitBall (definitions Plasticity_Basic) for the submodule types, whose norm is the supremum norm inherited from .
Statements are not to be weakened by assuming continuity of the inverse or countable Γ.
Published inputs (Freudenthal–Hurewicz, Brouwer or invariance of domain) may be added as separate cards and imported by proof sketches.
Sampling from a Gibbs distribution on is a basic task in Bayesian statistics, statistical physics and machine learning. A standard approach simulates the Langevin diffusion , whose invariant distribution is , through its Euler scheme, and averages a test function along one long trajectory. The discretization introduces a bias of the order of the step size, so a single-step-size average with accuracy costs more than steps. Dalalyan (arXiv:1412.7392) and Durmus–Moulines (arXiv:1605.01559) quantified this for strongly log-concave targets; for occupation measures of the Euler scheme the best previous bound was of order (Durmus–Moulines, Bernoulli 2019, denoted [DM19] in the paper).
Egéa and Panloup (arXiv:2109.07753, Math. Oper. Res., 2025) combine Giles's multilevel Monte Carlo idea (Oper. Res. 2008) with pathwise averages. Each level is one long trajectory, not many independent samples. This mission formalizes their result for a uniformly strongly contractive, twice differentiable drift. In that case the multilevel occupation measure reaches accuracy at a cost of order , the order of an unbiased Monte Carlo method.
Let be -Lipschitz and satisfy Assumption : for all , with . Let . The additive diffusion is , driven by a standard -dimensional Brownian motion . Let be its invariant distribution. Its Euler scheme with step is , , with invariant distribution . Write and for the Lipschitz constant of .
Given a first step , steps , horizons , a warm start , and independent Brownian motions , the multilevel occupation measure (7) is
where both schemes of level start at and are driven by . Its cost is .
When is with bounded derivatives, set (Frobenius norm of the Jacobian) and . The constant (19) is
Take , , and . There is a universal constant such that for every with ,
The constant is the same for all , , , , , and .
Under , and dimension-free bounds on , and , the choice , gives .
The milestones follow the paper's proof in order:
The result. Theorem 2.3 gives an explicit algorithm whose cost to reach accuracy on is of order , uniformly over Lipschitz . Under (22) the cost is . Apart from constants depending on and , this is the complexity of a Monte Carlo method without bias, an improvement over the known for single-level occupation measures. Corollary 2.2 of the paper applies it to Gibbs distributions with a potential.
Formalizing it. The theorem is proved in the paper. A machine-checked version needs a formal multilevel estimator over infinite horizons, uniform-in-time strong error bounds for the Euler scheme, and an application of Itô's formula to , none of which exists in Lean. Formalizing also checks the paper's constants. For instance, the printed exponential rate in the contraction behind is , while its proof gives , and the milestone states . No part of this result has been machine-checked.
Two steps resist a direct approach. First, the order-one strong error (Lemma 5.2(ii), Proposition 5.1(ii)). Bounding the one-step error by the Lipschitz constant alone gives order per step, hence order globally; this is Lemma 5.2(i) and the regime, with an extra in the cost. The gain to needs the second-order structure of along the Brownian path, through a martingale term and the Laplacian of . Second, the error must be controlled uniformly over infinite horizons. Every estimate has to combine the contraction with the step-size restriction ; a Gronwall argument on a finite horizon gives constants that grow with time.
For the goal itself, the cost bound (21) is arithmetic once the parameters are fixed. The content is the error bound with a constant that is universal, not merely independent of .
EthierKurtz.SDEState d, and Brownian motions are the published EthierKurtz.IsStandardBrownian.eLpNorm · 2 P, valued in . The schemes are evaluated at grid times, except in and (47), which use the continuous-time scheme.ContDiff ℝ 2 b plus a uniform bound on the first and second Fréchet derivatives.The goal does not assume –, Proposition 2.2 or any variance or bias estimate. It assumes only , Lipschitz and regularity of , , invariance of and the parameter choices. Those results appear only as milestones.
Contributions that would be reusable elsewhere: uniform-in-time moment and strong-error bounds for Euler schemes of contractive SDEs, Itô's formula for a function of Brownian motion, and the general multilevel complexity theorem (Remark 4.1). Proofs of the milestones are welcome independently.
In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.
Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.
Fix a horizon and a payment cap . A standard Brownian motion on is the output. Agents have types . An agent of type receiving a payment rate and exerting effort has running utility and running cost ; is increasing and concave in , is convex in (Assumption 2.2). Effort shifts the drift of through the Girsanov measure (weak formulation). The agent's optimal effort against a sensitivity process is , the inverse of , and denotes expectation under the corresponding measure.
A contract started at time is described in forward form by : the agent's continuation utility is
with and the constraint . The agent's utility is capped by the upper barrier . He quits at the first time reaches the lower barrier , where is his market value and his quitting cost (Assumptions 2.7, 3.1). The relevant domain is
When the -th agent quits at , the principal pays and hires an agent of type at utility (the quitting sequence (5.8)). The principal's value is
and the value of the best new hire at time is .
The family is the minimal continuous viscosity solution of
with boundary conditions
The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that is a genuine real-valued function.
The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.
The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.
The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control is unbounded, so the Hamiltonian can be and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by and Theorem 4.5 instead.
All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is ; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at are progressively measurable for the filtration of . Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.
Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with test functions on , tested on the interior of , with the supremum in the HJB operator never formed; the boundary condition at requires a real right limit compared against every ; carries a σ-algebra and , , are jointly measurable; Assumption 2.7 (ii) is read as ; a modulus of continuity is nondecreasing, vanishes at and satisfies ; generic constants depend only on and are fixed before the model; and take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of , , are out of scope.
A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.
Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.
Mean-variance (MV) preferences, , are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth to a wealth that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity .
A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.
On a probability space live two independent Brownian motions and an independent Poisson random measure with finite Lévy measure and compensated measure . The filtration is generated by . A stochastic factor follows
with . Investing the amount in the risky asset gives the (discounted) wealth
on , with . Write and .
The MMV preference is
The infimum runs either over the Doléans-Dade measures or over all of . A measure in has density , where is the stochastic exponential of with , and .
The optimal utilities from are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable whose wealth has , under for MV and under every for MMV. Both solutions are expressed through the solution of the nonlinear parabolic PDE (20),
Through it also enters Assumption 1. Let be the first jump time after at which . Assumption 1 requires at every jump in up to time .
The same holds when ranges over instead of .
The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave , and that happens exactly when a jump of size can occur before the first jump with . In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value , the variance of the optimal wealth, the efficient frontier) are what applied work uses.
The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.
The obvious argument would show along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in . Remark 7 also notes that membership in alone does not identify the optimal values; both optimal strategies must be found and compared.
Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities , which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.
Peng1990.SMP.Stochastic. The admissible classes , , therefore contain only strategies whose Brownian integrands are in ; all strategies used in the paper qualify.JacodTodorov10.LLN.IsFPoisson with finite and . The compensated integral is the pathwise sum over atoms minus the compensator integral.Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.EReal over the full admissible classes. Measures in are probability measures.A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as ; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.
Sampling from a Gibbs distribution on , or computing integrals against it, is a basic task of Bayesian statistics, statistical physics and stochastic optimization. A standard route is to simulate a diffusion whose invariant law is the target, for instance the overdamped Langevin equation , discretize it with the Euler scheme, and average a function along one long trajectory. Discretization introduces a bias of order of the step size, and the long-time average introduces a variance that decays like the inverse of the horizon, so reaching root-mean-square accuracy with a single Euler scheme costs more than steps.
Egéa and Panloup (arXiv:2109.07753, Mathematics of Operations Research, 2025) adapt Giles's multilevel Monte Carlo idea (Giles 2008) to this infinite-horizon setting: they combine a coarse pathwise average with corrections between coupled Euler schemes of successively halved steps, run over decreasing horizons. Their general complexity theorem (Theorem 2.1) is stated under four abstract assumptions (H₁)–(H₄). This mission formalizes the first concrete instance the paper gives: an additive diffusion with a strongly contractive drift, where the assumptions are verified with explicit dependence on the dimension and the cost is of order .
Let and be the Euclidean norm and inner product on . Let be -Lipschitz and satisfy the contractivity assumption :
with . For this is uniform strong convexity of . Let and let be a standard -dimensional Brownian motion. The additive diffusion started at is ; a probability is invariant for it if for all and Borel .
The Euler scheme with step is , , extended to continuous time by , . A probability invariant for one step of the scheme is its invariant distribution.
The multilevel occupation measure with start , coarse step , levels , steps , horizons and warm-start time is
where level uses its own Brownian motion , independent across levels, and both schemes of a level share it. Its cost is , the number of simulated Euler steps. Write for the Lipschitz constant of and
There is a universal constant such that, for , , the parameters
and every with ,
The constant does not depend on , , , , or ; all dependence on the problem sits in the explicit cost.
The goal gives a complexity of order for approximating by a pathwise average of Euler schemes, within a logarithmic factor of the of an unbiased Monte Carlo method, with constants explicit in , , , . When , the cost is of order . The intermediate results (uniform-in-time strong error of the Euler scheme, Wasserstein bias of its invariant law, step-independent contraction) are standard tools of Langevin Monte Carlo and are reusable on their own.
The results are proved in the paper; none of them is machine-checked. A formal proof would certify both the abstract multilevel argument as instantiated here and the explicit constants. The formal statements also pin three printed slips: the ceiling in (14) (cube of the ceiling, not ceiling of the cube), the first line of (12) (the function of Lemma 5.1 (ii)), and the factor in (15).
The obvious argument controls bias and variance separately for each level. The bias of a pathwise average involves the long-time behaviour of the scheme, and the variance of a correcting level involves the distance between two coupled schemes over an unbounded horizon: both require estimates uniform in time, which fail for a merely Lipschitz drift (the strong error of the Euler scheme grows exponentially on finite horizons). Contractivity is what makes the strong error uniformly in , and the delicate point is to obtain this with constants that do not degrade with or with the step. The complexity bound then requires balancing , the horizons and the warm start so that the long-time bias, the discretization bias and the variances all sit at level , with a universal constant.
is EuclideanSpace ℝ (Fin d) (published EthierKurtz.SDEState); Brownian motions are published EthierKurtz.IsStandardBrownian, one per level, mutually independent as path-valued variables. The diffusion is a pathwise solution of the integral equation with continuous paths; no Itô integral is needed because the noise is additive. Invariance of and is stated through transition probabilities. norms are eLpNorm … 2 in , so an infinite moment is never read as zero. is used in its Kantorovich–Rubinstein form, as an explicit integral, and the clause as the existence of a coupling with that quadratic cost (Mathlib has no Wasserstein distance; optimal couplings exist, so the forms agree). (H₁)–(H₃) are stated at grid times, (H₄) over all . "" is an existential constant quantified before every datum.
Standing assumptions carried as hypotheses: -Lipschitz, , (and where the paper requires it), . Added and disclosed: the §5.1 hypotheses in Lemma 5.2, in Proposition 5.2 (needed by Proposition 5.1), integrability of under , existence of and in Remark 4.1. The goal's (a maximum of a set that need not be an interval) is replaced by the inequality defining it.
The goal assumes only the contractive setting, the diffusion's invariance of and the parameter choices; it does not assume (H₁)–(H₄), a bias or a variance bound, which appear only as milestones, so it cannot be discharged by restating its hypotheses.
A complete development needs: second-moment and Grönwall estimates for the Euler scheme and the diffusion, existence and uniqueness of invariant laws of Feller chains under a Lyapunov condition, independence and variance decompositions for the multilevel estimator, and the abstract Theorem 2.1. The Gaussian-increment and Wasserstein tools are reusable well beyond this mission. Proofs of any milestone, and a Mathlib-style for general laws, are welcome.
A fund manager who tracks a benchmark (a stock index, a price index, the cost of higher education) wants the managed wealth to stay above the benchmark at all times. Under a strict floor constraint the set of admissible strategies can be empty when the benchmark is random. Bo, Huang and Yu (arXiv:2302.08302, Math. Oper. Res.) relax the constraint: the manager may inject capital so that , and pays per unit injected. The problem becomes a consumption–investment problem with a running-maximum cost, of the type studied with viscosity methods by Barron–Ishii (1989) and Bokanowski et al. (2015). The paper obtains instead a classical solution of the associated HJB equation and an explicit optimal feedback control. The reduction from the constrained problem to the auxiliary problem below is due to Bo, Liao and Yu (2021) and is not part of this mission.
A market has risky assets with return vector and invertible volatility matrix ; the riskless rate is . On a filtered probability space satisfying the usual conditions with a -dimensional Brownian motion , write and with . The benchmark is , where is a geometric Brownian motion with drift and volatility driven by , and is the running maximum of , .
A strategy invests and consumes at rate ; the class consists of progressively measurable pairs for which the wealth equation is well defined on every bounded interval. The auxiliary states are the reflected wealth surplus , started at ,
where is the minimal nondecreasing process keeping (the injected capital), and the reflected distance started at . With power utility , , and discount rate , the objective is
The candidate value function is built from a probabilistic representation. On a space with independent Brownian motions , let be a reflected drifted Brownian motion , let be a correlated one with local time , and let be a geometric Brownian motion. With the coefficients of (2.9) and (3.4),
for , and
For model parameters with and there is such that for every : (i) is a classical solution of the HJB equation (4.2) with the Neumann conditions and , with and ; (ii) for every admissible strategy and every ,
with equality for the feedback strategy , along a solution of the reflected feedback system (4.4). The threshold is asserted to exist, not fixed: the paper's formula (4.45) for it depends on and is not self-contained.
The theorem settles two questions about the relaxed tracking formulation: the optimal portfolio–consumption pair exists in feedback form, and the value function is a classical (not only viscosity) solution of an HJB equation with two Neumann boundary conditions. Together with the paper's Lemma 4.4, it shows that the expected discounted capital injection of the optimal strategy is finite, so the relaxed problem is well posed. The dual representation also gives the value in a separated form, three expectations of functionals of reflected Brownian motions, which is what makes the derivatives and the feedback explicit.
The result is proved in the paper; nothing here is open. No part of it is formalized. A formal proof would need Itô's formula for reflected processes, the smoothness of expectations of local-time functionals, and the duality argument; any of the milestones on its own is a self-contained target.
The last term of couples the reflected process with the local time of a second reflected process correlated with it through . Differentiating in directly fails: the local time is not differentiable in its starting point in any pathwise sense, and the correlation prevents conditioning one process on the other. The paper first treats the independent case (Lemmas 3.3–3.4), where the expectation factors through the law of , and then removes the correlation by a homogenization of the Neumann conditions (Proposition 3.5). A second difficulty is the verification step itself: the admissible class is unbounded and the state reflects at two boundaries, so the local martingale terms must be controlled by moment bounds that depend on the growth (4.7) of the feedback.
EthierKurtz.IsStandardBrownian), and every statement holds for every such space. The control problem lives on any filtered space satisfying the usual conditions with an -Brownian motion (published RankBasedSDI.LoadBalancing.UsualConditions, IsFBrownian).skorokhodReg), and as explicit exponentials. The only stochastic integral is , through the published EthierKurtz.HasBrownianItoIntegral with a continuous version required.lintegrals; statements about assert their finiteness. Stieltjes integrals use the Lebesgue–Stieltjes measure of the path. The objective is compared in the extended reals as , which agrees with whenever is defined and never produces ; is computed in so that for .ContDiffOn ℝ 2), the PDE on the open set the paper names, Neumann conditions pointwise on the faces; derivatives are taken within the closed coordinate domains. The suprema in (4.2) are least upper bounds (IsLUB), the consumption supremum over .The definitions of reflected processes, Stieltjes integrals against local times, and classical Neumann solutions are reusable beyond this mission. Proofs of any milestone, and of the deterministic facts (, , (3.9) solving (3.8)), are welcome.
Round-Robin is the simplest procedure for dividing indivisible goods: agents take turns, in a fixed cyclic order, each picking a favourite among the goods still available. When agents have additive valuations and pick truthfully, the resulting allocation is envy-free up to one good (EF1): no agent prefers another agent's bundle once a single good is removed from it. The procedure is used in practice (course allocation, sports drafts, the division of estates) and is the standard baseline in fair division.
The guarantee assumes truthful picking. Round-Robin is not truthful: an agent can gain by delaying a good that nobody else wants. Viewing the reported rankings as strategies turns the mechanism into a game, and two questions follow: does the game have (approximate) pure Nash equilibria, and are the allocations at equilibrium still fair with respect to the agents' true valuations? Round-Robin is the only known fair-division algorithm for more than two agents whose game is known to have equilibria (Aziz, Goldberg and Walsh, ADT 2017), and for additive valuations its exact pure Nash equilibria give EF1 allocations with respect to the true valuations (Amanatidis et al., WINE 2021). G. Amanatidis, G. Birmpas, P. Lazos, S. Leonardi and R. Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research 2025) extend both questions beyond additive agents. This mission formalizes their fairness result for subadditive cancelable valuations, Theorem 4.5.
There are agents and a finite set of goods. Agent has a valuation with that is non-decreasing. The marginal value of with respect to is . A valuation is
Additive, budget-additive () and unit-demand () valuations are subadditive and cancelable.
Each agent reports a preference ranking , a total order on . Round-Robin (Mechanism 1) runs rounds; in each round agents in turn receive the -best good still available. It returns bundles ; the mechanism sees only the rankings. Write for the profile in which agent replaces her ranking by .
For and subadditive cancelable valuations , every -approximate PNE of Round-Robin satisfies: for all with there is with
Fix agents , let be a strict truthful ranking of (it puts before whenever ), let be the good receives in round of , list by allocation time in that run, and split into and , , each renamed by Algorithm 3 (p. 11).
The proof also uses three results of the same paper that are formalized in sibling missions of this series: Lemma 3.3 (p. 8, a pointwise-domination lemma for cancelable valuations), Lemma 4.6 and Lemma 4.7 (p. 19, counting the goods that the deviation can displace), and the parity split of (p. 20). They are not restated here.
The result. Theorem 4.5 says that strategic reporting costs Round-Robin at most a factor in fairness, for a class that contains the additive, budget-additive and unit-demand valuations; at exact equilibria () the allocation is -EF1. Companion results of the paper give the existence of exact equilibria for cancelable valuations (Theorem 3.2), so the guarantee is not vacuous, and show that for two additive agents the right factor is and is tight (Theorem 4.3). Since additive valuations are subadditive and cancelable, the best possible factor for this class lies between and .
Formalizing it. The theorem is proved on paper; no machine-checked version exists. A formal proof requires making precise the coupling of two runs of Round-Robin — the equilibrium run and the run where one agent deviates — which the paper handles in prose. In the course of this formalization a step of the paper's argument was found to need repair (see Formalization scope), so a complete formal proof would also certify the statement itself.
The deviation of agent changes what every other agent receives, so (from the equilibrium run) and (from the deviated run) live in different executions and may share goods. Comparing them good by good requires controlling which goods were still available to at each of her turns in the deviated run; this is the content of Lemmas 4.6–4.7 and the parity split. The tempting step from the marginal comparison (2) to a comparison of singleton values, , via cancelability, fails when is one of : then its marginal value is and (2) carries no information about its singleton value. Algorithm 3 places such shared goods last, where this happens. A two-agent instance with additive valuations and eight goods exhibits the failure. The set inequality of milestone 2 has to be reached another way.
Agents are Fin n with n ≥ 1; goods a finite type M with decidable equality; a valuation is a real function on Finset M, required to be normalized and non-decreasing. Rankings are duplicate-free lists containing every good, most preferred first; Round-Robin is defined step by step (step belongs to agent ), and agents' bundles collect the picks of their steps among the first . The paper's standing assumption (p. 7, justified there by adding dummy goods) is a hypothesis of every theorem; the reduction is not formalized. The hypotheses are those of the page. Algorithm 3 is encoded relationally (every tie-breaking is admitted), and strict truthful rankings admit every order among goods of equal singleton value; both choices make the milestones at least as strong as the paper's lexicographic versions. Milestones 1 and 2 do not assume the equilibrium (the paper does not use it there).
The formal statements rule out the trivializing readings: deviations in the equilibrium hypothesis range over total orders only (not arbitrary lists), is excluded, EF1 is measured with the true valuations and not with the reports, and both subadditivity and cancelability are required of every agent.
On milestone 2. The page derives it through the intermediate claim , which is false in general (see Difficulty); the intermediate claim is therefore not posed. The set inequality itself held in every instance tested (400 000 random two-agent instances with additive and budget-additive valuations, and 26 000 random instances with two or three agents and additive, budget-additive, unit-demand and square-root-of-additive valuations), but the page's derivation of it is incomplete. Theorem 4.5 is not known to be affected.
Needed infrastructure: the Round-Robin execution (allocation sets after each step, the picks, bundles), lemmas relating two runs that differ in one ranking, and Lemma 2.2 (cancelable functions cancel any common disjoint set). The Round-Robin layer is shared with the sibling missions on Theorems 3.2, 3.7 and 4.4 and reusable for any picking-sequence mechanism. Contributions of any of these lemmas, of a repaired proof of milestone 2, or of a counterexample to it are welcome.
Place distinct points on the unit sphere in to minimise the Coulomb energy
Good configurations are easy to find numerically, but proving that one is the global minimum is hard. Rigorous proofs exist for only a few :
The shared lemmas (the distance formula, two-point positivity behind the Delsarte–Yudin bound, and three-point positivity behind the Bachoc–Vallentin and Cohn–Woo bounds) are stated once for reuse, along with well-posedness of each configuration.
Finitely many rotations of the sphere generate a group whose orbits are typically dense. A basic quantitative question is how fast those orbits fill the sphere: after words of length in the generators, how uniformly are the points spread? The answer is controlled by the spectral gap of an averaging operator built from the generators. The question goes back to the Banach–Ruziewicz problem (uniqueness of rotation-invariant finitely additive measures on spheres), was studied by Lubotzky, Phillips and Sarnak in their work on distributing points on (LPS 1987), and was formulated as a conjecture about random generators by Gamburd, Jakobson and Sarnak. It also matters in quantum computing: a spectral gap for a gate set gives efficient approximation of every single-qubit gate by short gate sequences (Sawicki–Karnas 2017).
Timeline.
The tuples with algebraic entries form a Haar-null set, so the conjecture for random tuples remains open.
Let be the group of complex matrices with and , a compact group with its normalized Haar measure (the unique left-invariant Borel probability measure). For the Hecke operator acts on functions by
On it is bounded and self-adjoint, constants are eigenfunctions with eigenvalue , and it preserves the space of mean-zero functions. Writing for the supremum of the spectrum of on , one always has , and (or the tuple ) has a spectral gap when
For , each acts on the sphere by rotations, and is the operator of the source.
For every , if are chosen independently and uniformly (Haar) at random in , then with probability
By Fisher's law, the goal follows once a spectral gap is shown on a set of positive Haar measure.
A spectral gap for means that random walks driven by equidistribute in (and orbits equidistribute on ) at an exponential rate, and that the action of the generated group on is strongly ergodic. In quantum computation it says that a universal single-qubit gate set is automatically efficiently universal. The conjecture asserts that this holds for a typical gate set, not just for the arithmetically special ones covered by Bourgain–Gamburd.
On the formal side, the milestones are proved theorems (Fisher; Bourgain–Gamburd) that have, to the knowledge of this proposal, no machine-checked proofs. Formalizing any of them requires substantial new libraries: Haar measure and harmonic analysis on , ergodicity of on (Goldman), and the arithmetic-combinatorial machinery of Bourgain–Gamburd. The goal itself is an open problem.
Spectral gap is not detected by density alone: every tuple generating a dense subgroup gives an ergodic action, but ergodicity only shows is not an eigenvalue, not that it is bounded away from . Known proofs need either arithmetic structure (automorphic forms, or the algebraic entries used by Bourgain–Gamburd to rule out short relations that come too close to the identity) or rigidity (property (T)). A generic tuple has neither.
Matrix.specialUnitaryGroup (Fin d) ℂ with the subspace topology and its Borel σ-algebra; it is shown to be a compact topological group, and haarSU d is the Haar measure normalized to total mass .Useful reusable contributions include: basic harmonic analysis on compact groups (translation invariance in , self-adjointness of ), the Peter–Weyl decomposition of , conjugation invariance of the gap, and monotonicity of the gap in the generating set.
This mission develops Chapter 10 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the complexity theorem for the Harrow–Hassidim–Lloyd (HHL) algorithm for the quantum linear systems problem (QLSP), in the form of Childs, Kothari and Somma (2017), Theorem 2.
The problem. Let be an Hermitian, invertible matrix with operator norm , condition number (known to the algorithm), and at most nonzero entries in every row and every column. Let be a vector in and , and write , , with indices held in qubits. The matrix is accessed through a black box consisting of the two unitary maps
where is the row index of the -th nonzero entry of column and the entry is written exactly as a -bit string in a fixed encoding. The vector is accessed through a unitary black box with . A use of a black box (possibly controlled, possibly inverted) is one query; the gate complexity is the number of other 2-qubit gates. The goal is to output, with probability at least and with a flag qubit indicating success, a state that is -close in Euclidean norm to .
The theorem. There are absolute constants and , and for every entry encoding constants , , such that for all , all , and there is a single quantum circuit, depending only on and the encoding, which solves every QLSP instance with these parameters, and whose number of queries to and number of uses of satisfy
and which is gate-efficient: its number of 2-qubit gates satisfies
Success means: started in on a flag qubit, output qubits and some number of work qubits, the final state has flag with probability , and the normalized flag- branch is within Euclidean distance of for some unit work-register state .
This is the benchmark against which the later precision improvements (Theorems 3–5 of Childs–Kothari–Somma) and de Wolf's §10.3 singular-value-transformation algorithm are measured.
Formalization Note A -sparse matrix with automatically has and ; these ranges are stated so that the logarithms are positive. The polylogarithmic factors with are written , which is equivalent. The gate-efficiency constants may depend on the fixed exact encoding of matrix entries, because the source treats the entry representation as exact and does not account for its arithmetic; the query constants do not. The source's assumption that runs in time concerns the cost of , which is counted only through . The theorem is vacuous for (the column map cannot exist), where the bound for is stronger anyway. The output may differ from by a global phase, absorbed into the work-register state.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 20 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the Gottesman–Knill theorem.
Let be the -qubit Pauli group. A measurement-controlled Clifford circuit family consists, for each number of qubits , of a sequence of at most operations, a polynomial, each of which is a Pauli gate, a Hadamard gate , the phase gate , a CNOT gate, or the projective measurement of a Pauli with projectors . The next operation is computed from , a string of uniformly random bits ( a polynomial) and the outcomes of the earlier measurements by a classical polynomial-time algorithm. Running on the computational basis state , , produces a random final pure state ; write for the distribution of its density matrix .
A stabilizer description (tableau) is a list with phases that pairwise commute, are independent (none is a phase times a product of the others) and do not generate ; it describes the state with density matrix .
Theorem. For every measurement-controlled Clifford circuit family there is a randomized classical polynomial-time algorithm such that for every and every :
Thus Clifford circuits with intermediate Pauli measurements and classical (randomized) control, started on a basis state, can be sampled exactly by a classical computer; the quantum advantage requires non-Clifford resources such as the gate.
Formalization Note The source says the simulator is "given C"; following its own remark on p.187 that one strictly has to speak of families , the simulator is fixed for the family (chosen before and ) and receives encoded as a bit string. Polynomial time is the Turing-machine notion PolyTimeComputable of this repository, applied to the input followed by a uniformly random string of polynomial length. Distributions over states are compared via density matrices, so the global phase is ignored, as in the source's footnote 3 on p.185.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 7 of Stabilizer Codes and Quantum Error Correction by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Fix an erasure probability . The qubit erasure channel acts independently on each qubit sent: with probability the qubit passes unchanged together with a classical flag , and with probability it is replaced by the maximally mixed state together with the flag , so that the receiver knows which qubits were erased. On qubits the channel is .
A rate is achievable (for quantum codes, equivalently one-way entanglement purification) if for every and there is such that for every there are a number of logical qubits, an encoding quantum channel from qubits to qubits and a decoding quantum channel from the channel output (qubits and erasure flags) to qubits with
where is the entanglement fidelity with respect to the maximally entangled state of two -qubit registers. The theorem states that the quantum capacity of the erasure channel is , in the strong form that the set of achievable rates is exactly
In particular every rate below is achievable (random stabilizer codes), no rate above is (a no-cloning argument), and for the capacity is zero.
Formalization Note The supremum of achievable rates is not written as a real sSup (which would be junk on an empty or unbounded set); instead the achievable set itself is characterized. Because the definition of achievability already has the slack , the achievable set is closed, so the capacity is itself an achievable rate. The author's errata note that the thesis's proof of the upper bound assumes there is no superadditivity when a noiseless channel is added to a zero-rate channel; the theorem itself is the established value (Bennett–DiVincenzo–Smolin).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
A Markov decision process (MDP) is optimized for a transition kernel that, in practice, is estimated from data, and the optimal policy for the estimated kernel can perform poorly under small perturbations of it. The robust MDP approach replaces the single kernel by an uncertainty set of kernels and asks for the policy with the best worst-case expected reward. It goes back to Satia and Lave (1973).
Whether a robust MDP is tractable depends on the shape of the uncertainty set.
Rectangular sets let the adversary choose the transitions out of different states independently, which is conservative when all transitions depend on a few common factors, such as a patient's physiology across health states. Factor uncertainty couples the states, and it is the first coupled model in which an optimal robust policy can still be computed.
There are finite sets of states and actions , with and . The rewards satisfy , is an initial distribution on , and is the discount factor. Fix factors indexed by and coefficients with . A factor matrix has probability vectors on as columns, and it induces the kernel
The uncertainty set is a nonempty convex compact set of factor matrices. It is r-rectangular if , so that each factor is chosen independently of the others.
A stationary policy gives a distribution on at each state. It is deterministic if each is a point mass. Write and . The decision maker's value function and the expected discounted reward are
The policy evaluation problem computes . The policy improvement problem computes . Let
Algorithm VI-PI is the iteration , .
Assume is r-rectangular. Then has a unique fixed point , and
Write . If , then , and the deterministic policy that VI-PI computes at that iteration is -optimal. The test is passed as soon as .
The milestones follow the paper's route to the goal.
Theorem 3.2, the policy-evaluation analogue of the goal (Algorithm VI-PE), is included as a further item.
The theorem shows that factor uncertainty, in which transitions out of different states are coupled, is as tractable as (s,a)-rectangular uncertainty, provided the factors are independent. An optimal robust policy exists among deterministic stationary policies, the robust and nominal problems share a saddle point, and value iteration on a -contraction computes the robust value. The structure is also what the companion mission builds on: the robust maximum principle and robust Blackwell optimality are derived from (5.1) and Theorem 4.2.
The results are proved in the paper. None of them is formalized: no factor-matrix robust MDP exists in Lean. The platform's robust-MDP items for (s,a)-rectangular sets (Nilim–El Ghaoui, Iyengar) and s-rectangular sets (Wiesemann et al.) are other uncertainty models and do not specialize to this one. A formal proof would also check a printed statement, since one clause of Theorem 4.2 needs correcting (see below).
The obvious argument writes a robust Bellman equation state by state and appeals to the contraction principle. Here that argument fails. Under factor uncertainty the adversary cannot choose the transitions out of each state separately, because one factor enters every row with . Minimizing state by state therefore yields kernels that need not come from a single feasible . The decision maker's equation for does not close on its own.
The step that requires care links two dynamic programs, the decision maker's over and the adversary's over , and shows that factor-wise minimization is feasible. That is where r-rectangularity enters. The paper's Appendix A gives an instance in which the factor-wise minimizers are infeasible once a constraint couples the factors.
Fin r (0-based).Fin r → S → ℝ whose values are probability vectors. It is nonempty, convex and compact. Nonemptiness is implicit in the paper and explicit here. is the projection of , and r-rectangularity is a hypothesis (IsRRect). Proposition 3.1, Lemmas 4.3, A.2 and A.3, and both contraction statements are stated without it. Lemma 3.3 is stated with it, since it is false without it.IsLeast/IsGreatest, and Lemma A.2 states the invertibility of , because Lean's matrix inverse is on singular matrices.Reusable infrastructure includes the discounted value of a stationary policy for a stochastic matrix, monotone sup-norm contractions with the standard stopping rule, and minimization of linear forms over compact sets. Contributions to any of these are welcome.
Many engineering and operations problems must guarantee that a system operates safely with high probability, when the uncertain parameters are only partially known. A chance constraint asks that the safety condition hold with probability at least for a tolerance . When the distribution of is itself uncertain, the distributionally robust version asks this for every distribution in an ambiguity set built from what is known: moments, supports, confidence regions. Two problems then arise: computing the worst-case probability (uncertainty quantification), and optimizing a design under the constraint (chance constrained programming).
Hanasusanto, Roitch, Kuhn and Wiesemann (Math. Program. 151, 2015) chart which combinations of ambiguity sets and constraint structures admit exact finite reformulations and which are strongly NP-hard. This mission takes the positive core of that chart: for Markov ambiguity sets (first-order moment information plus a conic support), the worst-case probability is the value of a finite conic program, and an individual chance constraint is equivalent to a finite system of linear conic inequalities.
Timeline. Chebyshev-type bounds for worst-case probabilities under moment information go back to the generalized Chebyshev inequalities of Vandenberghe, Boyd and Comanor (2007), and to the duality theory of moment problems summarized by Shapiro (2001). Wiesemann, Kuhn and Sim (2014) introduced the nested conic ambiguity sets used here to evaluate worst-case expectations. Hanasusanto et al. (2015) applied them to worst-case probabilities of polytopes and to chance constraints, proving Theorem 3 (moment problem reformulation) and Theorem 7 (individual chance constraints over Markov sets), together with strong NP-hardness results, such as Theorem 8, showing that the restrictions cannot be dropped.
Let be the uncertain parameters and an auxiliary random vector. Fix , , , and a confidence set
where , , and is a proper cone (closed, convex, pointed, with nonempty interior); means , and is the dual cone. The Markov ambiguity set is
the case , of the paper's nested set (4).
Two regularity notions enter. is essentially strictly feasible if it contains a point satisfying all non-polyhedral constraints of its description strictly. The Slater condition (S) for requires to lie in the interior of .
For the safety system with rows , , let be the rows that can be violated on . Problem (17) at maximizes over , , and, for , , , subject to , , and, for , , , .
For an individual constraint () write . System (26) asks for , , , with
Under essential strict feasibility of , (S), and ,
Theorem 7 turns an individual distributionally robust chance constraint over a Markov ambiguity set into finitely many linear conic constraints whose size is polynomial in the data. Since and are affine in the design , the chance constrained program becomes a single conic program, solvable with standard software. The paper notes (p. 18) that, apart from the Wasserstein set, all ambiguity sets of its Section 2.3 are Markov sets or intersections of Markov sets with structural ambiguity sets, and Theorem 8 shows that adding a second confidence set already makes the problem strongly NP-hard, so the theorem marks a precise tractability boundary. Theorem 3 underlies the paper's later results and its §5 heuristic for intractable cases.
All five statements are proved in the literature: the paper defers its proofs to an accompanying technical report. None is machine-checked. A formal proof would supply a verified duality theory for moment problems with conic supports, a reusable bridge between semi-infinite constraints and conic certificates, and a verified basis for the paper's hardness results to be stated against.
The sufficiency halves are weak-duality arguments. The converse directions are not: the worst-case probability is an infimum over an infinite-dimensional set of measures, and the conclusion of Theorem 7 requires the dual certificate to be attained, not just approached. Two separate duality steps must both close without a gap and with attainment: the moment problem against its semi-infinite dual, which is where (S) enters, and each semi-infinite constraint against its conic dual over , which is where essential strict feasibility enters. The event is open, so the semi-infinite constraint must also be passed to its closure. Mathlib has neither a duality theorem for moment problems nor conic strong duality with attainment.
The mission covers Markov ambiguity sets only (, ). The general nested case of Theorem 3 is not stated, because the paper does not make (S) explicit for . Symmetry and unimodality information, joint chance constraints and the hardness results are out of scope. The paper's proofs are in a technical report that the mission does not use.
Conventions committed to in Lean:
Fin n → ℝ, the single confidence set is index 0 : Fin 1 of the published DRConvexOpt.Reform.AmbData, and its field c 0 is .μ.real. The local paperAmbiguitySet reuses the published data and confidence-set definitions and requires integrability only of . This makes the expectation condition void when , as the paper states.sInf ∅ = 0.Replacing essential strict feasibility by full strict feasibility, adding to (26), or imposing the -constraints for would each change the theorem and is ruled out. The hypotheses are jointly satisfiable: , , , satisfies all of them, with a nonempty ambiguity set.
A complete development needs conic duality with attainment under partial Slater conditions, Lagrangian duality for moment problems, and the reduction of a measure-valued infimum to finitely supported measures. All three are reusable well beyond this mission, and contributions to any of them are welcome.