Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
We investigate entanglement measures in the infinite-dimensional regime. First, we discuss the peculiarities that may occur if the Hilbert space of a bi-partite system is infinite-dimensional, most notably the fact that the set of states with infinite entropy of entanglement is trace-norm dense in state space, implying that in any neighborhood of every product state there lies an arbitrarily strongly entangled state. The starting point for a clarification of this counterintuitive property is the observation that if one imposes the natural and physically reasonable constraint that the mean energy is bounded from above, then the entropy of entanglement becomes a trace-norm continuous functional. The considerations will then be extended to the asymptotic limit, and we will prove some asymptotic continuity properties. We proceed by investigating the entanglement of formation and the relative entropy of entanglement in the infinite-dimensional setting. Finally, we show that the set of entangled states is still trace-norm dense in state space, even under the constraint of a finite mean energy.
This mission is the statement-level formalization of On the quantification of entanglement in infinite-dimensional quantum systems (arXiv:quant-ph/0112064v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 10: no separable ball under a strict mean-energy bound (Proposition 10: no separable ball under a strict mean-energy bound (seed paper result), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
The symmetric traveling salesman polytope is the convex hull of the incidence vectors of all Hamiltonian cycles of the complete graph . Minimizing a linear cost over it is the traveling salesman problem, and polyhedral methods for the TSP (cutting planes, branch and cut, LP relaxations and their integrality gaps) depend on linear inequalities that are valid for and, ideally, define its facets. Known facet classes include the comb, clique-tree, path and crown inequalities; Naddef's survey (Naddef 2007) collects them.
Circulant TSP instances are those whose edge costs depend only on the edge's length around a circle of equally spaced cities. Gutekunst and Williamson (SIAM J. Discrete Math. 2019) showed that the subtour LP has integrality gap exactly on circulant instances; the witnessing family of LP solutions is cut off by several known facets, but not robustly under small modifications. They conjectured an inequality, now called the circlet inequality, that would cut off the whole family. The paper of this mission (arXiv:2012.12363v1) proves that conjecture and shows the inequality is facet defining when . Its coefficients are themselves circulant, a property shared among classical facets only by the crown inequalities of Naddef and Rinaldi (Math. Oper. Res. 1992).
Timeline. 2019: Gutekunst and Williamson characterize the subtour LP gap on circulant instances and conjecture Inequality (2). 2020: Gutekunst and Williamson prove validity (Theorem 3.1) and the facet property (Theorem 5.1) for , and compute the inequality's strength.
Fix cities , edges of , and . The length of the edge is
an integer in . For a vector and , is the total weight on edges of length . A Hamiltonian cycle visits every city once and returns; its incidence vector marks its edges, and
For the circlet coefficients are for odd and for even (for : ), and the circlet inequality is
An inequality is valid for if every point of satisfies it, and facet defining if moreover the face has .
In the Lean development, cities are Fin n, a Hamiltonian cycle is an ordering π : Equiv.Perm (Fin n), its incidence vector is MetricTSP.tourVec π, STSP n is the convex hull of these vectors, lenCount n i x is , coeff n i is and circletForm n x is .
For every positive with :
Every Hamiltonian cycle on cities, , satisfies (2). The proof is by minimal counterexample and runs through the milestones Claim 3.2 (the base case ), Lemma 3.3 (a violating cycle has ), Lemma 3.4 (a minimal violating cycle contains none of three local edge patterns), and the window count with .
Lemma 3.4 is proved by contracting four vertices of a cycle containing one of the patterns and showing the cost drops by at least : Claims 4.1 and 4.2 (symmetries), Proposition 4.3 (surviving edges never get more expensive), Propositions 4.4 and 4.5 (the five contracted edges), and the resulting contraction step.
The dimension (cited on p. 19 from Naddef and Rinaldi, Theorem 3.7), and a family of tight Hamiltonian cycles with linearly independent incidence vectors.
The circlet inequality is a facet of whose coefficients depend only on edge length, so it is invariant under rotation of the city labels. It resolves the circulant TSP conjecture of Gutekunst and Williamson and removes from the subtour LP every member of the canonical family of solutions that witnesses the integrality gap on circulant instances, a class of TSP instances for which relatively little is known. Since any relabelling of the cities gives another valid inequality, it supplies on the order of facets of . The validity proof also gives a self-contained example of a minimal-counterexample argument by vertex contraction, a technique common in polyhedral combinatorics.
The result is proved in the paper; it has not been formalized. This mission produces machine-checked statements of the validity theorem, the facet theorem, and every intermediate result their proofs use, together with a reusable formal model of , edge lengths on a cycle, and facets of polytopes built from tour incidence vectors. The dimension of is a classical cited result that, to the best of current knowledge, has no formal proof either; it is included as a target in its own right.
Validity is not a local statement. A Hamiltonian cycle may use edges of any length, and the coefficients alternate between and with parity, so no edge-by-edge or degree-by-degree bound works: the inequality is tight on cycles that mix lengths , and one other length. The paper's argument needs the global structure of the cycle twice, once to rule out the patterns of Figure 4 in a minimal counterexample (where a parity argument on a four-group quotient graph handles the hardest equality case of Proposition 4.5) and once to count windows. The contraction step requires checking that the contracted object is again a Hamiltonian cycle and tracking costs on two different vertex sets with different moduli and .
For the facet half, exhibiting the tight tours is explicit, but proving the linear independence of incidence vectors for all and proving the dimension of are substantial linear-algebra arguments. The paper's own justification of independence for the first family is inaccurate (a length- edge is shared by two rotations), so a correct argument has to be supplied.
Fin n with 0-based labels; lengths and costs depend only on label differences, so the shift from changes nothing. The contraction results (Propositions 4.3–4.5, the contraction step) use the paper's 1-based labels in ℕ, with integer lengths and costs, and refer to a cycle's edges through the label of each vertex ().Fin n → Fin n → ℝ (ordered pairs); the incidence vector is symmetric with zero diagonal, and affine dimension is the same as in . counts each unordered edge once.Disjunctive.Polarity.IsFacet (extreme, nonempty, dimension one less), and the goal conjoins validity, since a face of codimension one is also cut out by the reversed inequality.We present in this paper a set of routines constructed to compute the rank of a matrix Lie algebra and also to determine a Cartan subalgebra from a given list of elements
This mission is the statement-level formalization of Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica (arXiv:math/0205235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is so(n): BSo ordered basis (so(n): BSo ordered basis, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793) settled a question open since the birth of complexity theory: primality has an unconditional, deterministic, polynomial-time test. The paper's algorithm is elementary - six steps: reject perfect powers; fix a small r; reject trivial factor witnesses; accept small inputs; test the congruence (X + a)^n = X^n + a modulo X^r - 1 for a = 1, ..., ell; accept. The mathematical heart is Lemma 2.1, a generalization of Fermat's Little Theorem to polynomial rings: for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X]. The correctness of the harder direction runs through the introspective machinery of Section 4: for a prime factor p of n with o_r(p) > 1, the numbers of I = {(n/p)^i p^j} are introspective for the polynomials of P = {the products of the generators X, X+1, ..., X+ell}; the residues of I generate a group G modulo r of size t > log^2 n; the images of P generate a group G-cal in the field F = F_p[X]/(h), h an irreducible factor of the r-th cyclotomic polynomial over F_p; Lenstra's lower bound and the Kalai-Sahai-Sudan upper bound on the size of G-cal collide unless n is a power of p, and step 1 excludes prime powers, so n is prime. Section 5 bounds the arithmetic work: O~(log^(21/2) n), unconditionally.
The mission formalizes the paper's mathematical content in Lean 4. The goal statement is Theorem 4.1: the algorithm of the algorithm layer returns PRIME if and only if n is prime. The milestones are the ingredients in attack order: the polynomial Fermat characterization (Lemma 2.1); the lcm lower bound (Lemma 3.1); the existence of a small r with large order (Lemma 4.3); the closure of introspection under multiplication (Lemmas 4.5 and 4.6); Lenstra's injectivity bound (Lemma 4.7); the Kalai-Sahai-Sudan collision bound (Lemma 4.8); and the polynomial work bound of Section 5 (Theorem 5.1, in generous integer form).
The source document is the uploaded paper (annals-v160-n2-p12.pdf in the mission materials).
The formalization is a two-layer development in the namespace AKS. The polynomial layer (AKS_poly) carries the congruences: congruence (1) as an equality in Z_n[X], congruence (2) as divisibility by X^r - 1 in Z_n[X], Definition 4.4's introspection relation over F_p[X], and the set P of products of the generators. The algorithm layer (AKS_alg) carries the arithmetic scaffolding and the algorithm itself: the integer logarithm, the multiplicative order, the lcm of the first numbers, the perfect-power predicate, the search for r, the loop bound, the six-step decision function, the set I and the residue group G, and the work measure of Section 5.
The following choices are disclosed explicitly.
Compile verification by CI substitution. The authoring environment has no local Lean toolchain, so the compile check demanded by the mission is performed by the continuous integration of the repository (Lean 4.33 with Mathlib): all Lean code below was compiled there before this proposal was submitted, and the code attached to the items is byte-identical to the compiled modules.
The theorem drafts carry sorry. The eight theorem statements are submitted as drafts for human review; each proof body is a single sorry marking the work the mission proposes to complete. The compilation therefore succeeds with exactly one "declaration uses 'sorry'" warning per theorem file.
Generous integer encodings of the logarithms. The paper's real-valued log n appears in the algorithm only through the threshold o_r(n) > log^2 n of step 2 and the loop bound ell = floor(sqrt(phi(r)) log n) of step 5. The mission encodes both with logUp n = floor(log2 n) + 1, which is strictly larger than log2 n: step 2 searches for the smallest r with ordR r n > logUp(n)^2, and ell is the floor of the product of the square root of phi(r) and logUp n, encoded exactly as the floor of the square root of phi(r) logUp(n)^2. Both encodings are generous in the directions that preserve correctness: primes pass congruence (2) for every a and r, so a larger threshold and a longer loop never reject a prime; and for the converse the larger threshold and loop only strengthen the group bounds that force composites out. The integer bookkeeping of the final chain - floor(sqrt t) logUp n + 1 at least sqrt t log2 n - is part of the proposed work of the goal, with the generosity supplying the slack.
The algorithm layer transcribes the six steps literally, with computable searches inside provable windows and classical decision where only the extension matters. ordR r a is the least k < r with a^k = 1 (mod r) - the window k < r is faithful because every multiplicative order divides phi(r) < r - and 0 when gcd(a, r) > 1. smallestR n searches the window bounded by the r_exists milestone's bound. aksDecide is stated with classical decision (open Classical, noncomputable): no execution of the test is ever needed, only its extensional behavior. aksWork is a computable schoolbook work measure charging logUp(n)^6 for step 1, r(logUp n + 1) for the searches of steps 2 and 3, and ell r n (logUp n + 1)(r + 1)^2 for the congruence loop of step 5.
The groups are encoded by witness windows, and the two bounds are stated in the paper's forms. G is the Finset of residues modulo r of the numbers of I, encoded by the witness window i, j < r - faithful under the coprimality of n/p and p to r, because both orders then divide phi(r) at most r, so every residue of an I-number is achieved inside the window. Lemma 4.7 is stated in the paper's form: two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h) (the field is AdjoinRoot h; the hypotheses carry h dividing X^r - 1, the primitivity - h not dividing X^k - 1 for 0 < k < r - irreducibility by instance, the introspectivity of I for P, and t at most the size of G). Lemma 4.8 is stated in the collision form: unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2. The cardinality bookkeeping between these forms and the size of G-cal - stars-and-bars for the lower bound with the unique factorization of the generator products, and the root bound of a polynomial over a field for the upper - is carried by Mathlib and is part of the goal's proposed work.
The field F = F_p[X]/(h) is taken with its factor h as an explicit parameter. The statements do not construct h; they carry h dividing X^r - 1, primitivity, and irreducibility as hypotheses (the latter two as Fact-class instances). The existence of h - an irreducible factor of the r-th cyclotomic polynomial over F_p of degree o_r(p), the standard fact of Lidl and Niederreiter cited as [LN] - is part of the mission's proposed work toward the goal.
The "is in P" claim is anchored by an explicit work measure, with the bit-cost correspondence in prose. Milestone 7 bounds aksWork by C logUp(n)^15, a generous integer form of Theorem 5.1's O~(log^(21/2) n) - the generous exponent absorbs the schoolbook charging model and the logUp slack. The correspondence between arithmetic-work measures and Turing-machine bit complexity - the standard O~(m) arithmetic on m-bit numbers of the paper's Section 5 - is carried in prose; a machine-level formalization is out of scope.
Pruned content. The paper's Section 5 refinements (Fouvry's Lemma 5.2 and the O~(log^(15/2) n) of Theorem 5.3, and the Lenstra-Pomerance variant), the conjectures (Artin's, the Sophie Germain density, Conjecture 6.1), and the historical survey of Section 1 are out of scope; the mission carries the unconditional Section 5 analysis only, in generous integer form, and the correctness theorem (Theorem 4.1) as the goal.
Due diligence. Before creating the proposal, the creation script searches the platform for prior definitions and theorems matching the paper's ingredients; the search results are recorded in the repository's results directory for the reviewer.
Definition names and module stems. The two definition bundles are published under names equal to their module stems (AKS_poly, AKS_alg), so that the platform imports Definitions.Def_AKS_* in the theorem preambles resolve, in dependency order poly, then alg (which imports poly).
The mission has ten items: two reference definitions and eight theorem drafts, in the following order.
Reference definitions (the formalization fragment):
AKS_poly: the polynomial layer. Congruence (1) as the equality (X + a)^n = X^n + a in Z_n[X]; congruence (2) as divisibility by X^r - 1 in Z_n[X]; Definition 4.4's introspection relation over F_p[X]; and the set P of products of the generators X, X+1, ..., X+ell.AKS_alg: the algorithm layer. The integer logarithm logUp; the multiplicative order ordR; the lcm of the first numbers; the perfect-power predicate; the six-step decision function aksDecide with its search smallestR and loop bound ell; the set I and the residue group G; and the work measure aksWork.Theorem drafts (milestones in attack order, then the goal):
AKS.poly_fermat: Lemma 2.1 - for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X] (Section 2).AKS.lcm_lower: Lemma 3.1 - the lcm of the first m numbers is at least 2^m for m at least 7 (Section 3).AKS.r_exists: Lemma 4.3 - for n > 1 there is an r with 1 < r at most max 3 (logUp n)^5 and ordR r n > logUp(n)^2 (Section 4).AKS.introspective_closure: Lemmas 4.5-4.6 - introspective numbers are closed under products, and introspectivity is closed under products of polynomials (Section 4).AKS.group_inj: Lemma 4.7 (Hendrik Lenstra Jr.) - two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h), under the primitivity and introspectivity hypotheses, with t at most the size of the residue group G (Section 4).AKS.group_upper: Lemma 4.8 (Kalai-Sahai-Sudan) - unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2 (Section 4).AKS.poly_time: the work bound - there is a constant C with aksWork n at most C logUp(n)^15 for every n, the generous integer form of Theorem 5.1 (Section 5).AKS.prime_iff (the goal): Theorem 4.1 - aksDecide n = PRIME if and only if n is prime (Section 4).Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.
The paper is one of the landmark results of computational number theory: a problem open since the 1960s - an unconditional, deterministic, polynomial-time primality test - solved by elementary means, in a proof whose only ingredients are the binomial theorem, Euler's function, and the root bound of a polynomial over a field. The formal account forces exactly what the prose leaves to convention: the precise ring in which each congruence lives, the precise windows in which the searches find their witnesses, the precise generosity of each integer rounding, and the precise content of the two group bounds. The paper's difficulty lies not in any single deep theorem but in the assembly of many small lemmas under one bound chain; a formalization makes each link explicit and checkable, and the mission's readback discipline gives an independent restatement check of every statement before review.
Milestone 1 is a commutation: the forward direction is the freshman's dream in Z_p[X] plus Fermat's little theorem for the base; the backward direction isolates the coefficient of X^q for a prime q with q^k dividing n exactly and computes its q-adic valuation below k. Milestone 2 is Nair's argument: the product of the primes in (m/2, m] divides the lcm. Milestone 3 is the counting argument: every bad r divides a single product below the lcm of the window, so some r in the window escapes. Milestone 4 is two ring commutations: f^(m m') = f(X^(m m')) along f(X^m)^(m') = f(X^(m m')), and the product rule for introspectivity. Milestone 5 is Lenstra's argument: from a collision in F and introspection, f(Y) - g(Y) acquires the t distinct primitive r-th roots indexed by G, exceeding its degree. Milestone 6 is the pigeonhole of I-hat against G, the non-power distinctness, and the collision equation transported by introspection. Milestone 7 is arithmetic over the windows. The goal assembles: Lemma 4.2's direction is the congruences for primes; the step-4 case is the factor below the square root; and the step-6 case is the chain of Lemma 4.9 - the injectivity lower bound, the collision upper bound, and the integer bookkeeping that the generous encodings close with slack.
Included: the two congruences and the introspection relation; the set P and the set I with the residue group G; the six-step algorithm; and the eight statements - the Fermat characterization, the lcm bound, the small-r existence, the two closure lemmas, the two group bounds, the work bound, and the correctness theorem.
Excluded, as disclosed in items 7 and 8 of section 2: the machine-level bit-cost formalization of "is in P" (carried in prose, anchored by the explicit aksWork measure); the Section 5 refinements (Fouvry's Lemma 5.2, the O~(log^(15/2) n) of Theorem 5.3, the Lenstra-Pomerance variant of [LP1]); the conjectures of Section 5 and Conjecture 6.1; and the historical survey of Section 1.
Every value of a fundamental constant used in science — the fine-structure constant, the Newtonian constant of gravitation, the Rydberg constant — comes from one place: the least-squares adjustment periodically carried out by the CODATA Task Group on Fundamental Constants. The 2022 adjustment (P. J. Mohr, D. B. Newell, B. N. Taylor and E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022) takes 133 input data, determines 79 adjusted constants by weighted least squares with 54 degrees of freedom, applies expansion factors 1.7 and 2.5 to the uncertainties of certain groups of data to reduce all normalized residuals to two or less, obtains a final chi-square of 44.2 with Birge ratio 0.90, treats the sixteen values of the Newtonian constant of gravitation separately (16 data, one adjusted constant, 15 degrees of freedom, chi-square 12.9, expansion factor 3.9, Birge ratio 0.93), and obtains the recommended values from the adjusted constants by propagating their uncertainties and covariances.
The mission formalizes the mathematical skeleton of this process in Lean 4 and audits a representative slice of its output by exact rational arithmetic: the equivalence between minimizers of the chi-square statistic and solutions of the normal equations, the weighted mean as the rank-one case (the situation of the separate adjustment of G), the printed degrees of freedom and Birge ratios, the effect of uncertainty expansion on covariances and correlations, the algebraic laws of relative-uncertainty propagation, the exact derived constants determined by the exact defining values of h, e, k and N_A, and the mutual consistency of the printed uncertainties of the alpha family. The goal theorem packages these into the statement that the 2022 adjustment is self-consistent.
What is being formalized is the statistics and the arithmetic of the adjustment, not any physical measurement: the input data enter only through the abstract structure of a weighted least-squares problem, and the numerical audits compare exact rationals with the digit strings printed in the report's tables.
The source is the 2022 CODATA report in its two identical published versions: J. Phys. Chem. Ref. Data 54, 033105 (2025), doi 10.1063/5.0279860, and Rev. Mod. Phys. 97, 025002 (2025), doi 10.1103/RevModPhys.97.025002. The mission formalizes section XII, "Least-squares adjustment", and the exact and recommended values of Tables XXXII and XXXIII, under the following disclosed conventions.
Twelve conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the least-squares model, the correlations and uncertainty propagation, and the exact rational values — are published as platform definitions (CODATA_lsa, then CODATA_uncert which imports it, and CODATA_values), attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, the two uploaded PDFs are the same paper in its two published versions; citations reference both, and the table numbering follows the Rev. Mod. Phys. version (Tables XXXII-XXXIII, section XII). Third, the observational equations are taken in linear form; the report's observational equations are linear in the adjusted constants to begin with, but the values of the input data, the design matrix entries and the offset vector are interface data, not formalized: the theorems quantify over all weighted least-squares problems of the recorded dimensions. Fourth, the chi-square distribution and the printed probability values (83 percent for the main adjustment, 61 percent for G) are statistical statements about the chi-square distribution; they are printed data of the report and are not constructed, and no probability theory enters the mission. Fifth, the Newtonian constant of gravitation is treated separately, exactly as in the report: a second least-squares structure with sixteen input data and one adjusted constant, its own expansion factor 3.9, and its own Birge ratio; the goal theorem relates the two adjustments only through their common formalism. Sixth, the expansion factors 1.7 and 2.5 of the main adjustment are recorded in the description but not formalized, because the data they modify are interface data; the expansion factor 3.9 of the G adjustment is formalized through the covariance expansion law applied to the abstract covariance matrix of the sixteen values. Seventh, matrix inversion is expressed by two-sided inverse predicates, written entry by entry against the Kronecker delta, rather than through an inverse operator; this keeps the statements elementary and avoids any dependence on matrix inverse lemmas. Eighth, all arithmetic is rational or real: the exact constants are rationals, the derived quantities K_J, R_K, Phi_0, G_0, G_0⁻¹, F, R and the electronvolt are exact rationals, and the printed digit strings are captured by rational rounding intervals; exact quantities carrying a factor of pi (hbar, the Stefan-Boltzmann constant) and quantities with experimental uncertainty outside the audited family (the dalton, the Newtonian constant itself) are excluded because they are not rational. Ninth, the Birge ratios are captured by the rounding intervals [0.895, 0.905) and [0.925, 0.935), which the printed two-digit values 0.90 and 0.93 determine; the true values are sqrt(44.2/54) and sqrt(12.9/15). Tenth, the alpha family audit is an existential: the printed two-significant-digit uncertainties of alpha, 1/alpha, mu_0, eps_0 and Z_0 are jointly reproduced by a single rational relative-uncertainty witness of order 1.6 × 10⁻¹⁰, supplied explicitly by the prover (for example 156/10¹²); this witnesses consistency without asserting the (irrational, distribution-laden) exact relative uncertainty of alpha. Eleventh, the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission. Twelfth, everything is developed against the platform's Mathlib build (0df444a); the compilation check of every item is the repository CI, which builds all definitions and theorem drafts with the same Mathlib version (no local Lean toolchain is available to the drafting agent, and this is disclosed).
Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.
The CODATA adjustment is the mechanism by which the values of the fundamental constants become internationally accepted, self-consistent numbers; every precision measurement and every physical theory that quotes a constant inherits from it. The mission makes the three layers of the mechanism checkable by a proof assistant: the statistics (the least-squares theorem that the adjustment procedure is, by construction, the unique minimum of the chi-square statistic), the data hygiene (the effect of uncertainty expansion on covariances and correlations, and the propagation laws by which the recommended values and their uncertainties are derived), and the arithmetic (an exact rational audit confirming that the printed digit strings of the derived constants and the printed Birge statistics are consistent with the exact defining values and the reported chi-squares). Because the 2019 SI revision fixed h, e, k and N_A exactly, a growing family of derived constants is a pure rational computation; the mission verifies a representative slice of that family to the printed precision.
The milestones are honest and of mixed difficulty. The normal-equations milestone is the mathematical heart: the chi-square statistic is a quadratic form in the adjusted constants, strict positive definiteness of the weight matrix makes it convex, and the equivalence with the normal equations plus uniqueness at full column rank is a complete weighted least-squares existence-uniqueness argument, carried out entry by entry without matrix inverse lemmas. The weighted-mean milestone is a direct computation in the rank-one case, complicated only by the bookkeeping of the two-sided inverse predicate for the one-by-one normal matrix. The Birge milestone is real arithmetic: two subtractions and two square-root bounds, each reducible to exact rational comparisons by squaring. The expansion and propagation milestones are algebra over the reals: square roots of products of positive reals and the cancellation of equal factors; their difficulty is bookkeeping, not ideas. The derived-values and alpha-family milestones are exact rational computations with numerators and denominators up to thirty digits; they are fully decidable, and their difficulty is the size of the arithmetic — the prover must exhibit the witness ur and verify fifteen rational interval inclusions — for which norm_num-style automation is intended. The goal assembles the parts. Nothing in the mission requires mathematics beyond convexity of a quadratic form and exact rational arithmetic, and this is the point: the CODATA adjustment, the most authoritative computation in metrology, is at its core an auditable exact computation.
Every theorem quantifies only over abstract least-squares structures and rational values; no measurement, no physical theory, and no probability distribution enters. The fragment excludes: the 133 input data as concrete vectors and the 79 adjusted constants as concrete quantities; the chi-square distribution and all probability statements; the least-squares fitting of the theoretical expressions (atomic transition frequencies, muonic Lamb shifts, magnetic-moment anomalies); the 2022-versus-2018 value comparisons and the historical narrative; the mises en pratique and the experimental methods; the electroweak and particle-physics input data; the quantities whose exact values involve pi (hbar, the Stefan-Boltzmann constant) or whose values carry experimental uncertainty outside the audited family; and the correlations among the input data as concrete numbers. What is formalized is the statistical skeleton, the covariance algebra, and the exact rational audit of the printed output.
Graph neural networks (GNNs) compute representations of nodes and whole graphs by repeatedly combining each node's state with information from its neighbours. Soon after they became a standard tool, the question arose of what they cannot do. A natural test case is graph isomorphism: given two graphs that are not isomorphic, can the network attach different representations to them? If it cannot, it is hopeless on any task that needs to tell the two graphs apart.
The yardstick for this question is the Weisfeiler–Lehman (WL) test (Weisfeiler and Leman, 1968), a colour-refinement procedure that is a necessary condition for isomorphism. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2) reports, in its historical chapter (Ch. 7, p. 120), the conclusion of Morris et al. (2019) and Xu et al. (2019): any GNN of the three flavours of §5.3 "cannot be more powerful than the WL test". This mission formalizes that claim, together with the surrounding remarks of the book that make it precise.
Timeline. 1968: Weisfeiler and Leman introduce the refinement. 2011: Shervashidze et al. use the WL iteration to build graph kernels. 2017: Gilmer et al. unify many architectures as message-passing neural networks. 2019: Morris et al. and Xu et al. independently prove that message-passing GNNs are bounded by 1-WL, and that injective aggregation attains the bound (the Graph Isomorphism Network). 2020: Corso et al. show that with continuous features injective aggregation needs several aggregators.
A graph has node set and a symmetric, loopless adjacency relation. The neighbourhood of a node is (eq. (11), p. 34); it does not contain .
The WL colour refinement on a featureless graph starts with the same colour for every node and sets
where is a multiset. Colours carry their full history, so colours of nodes of two different graphs can be compared directly. The colour histogram at round is the multiset . The WL test declares two graphs indistinguishable when their histograms agree at every round.
A message-passing layer (eq. (35), p. 79) has a message function , a permutation-invariant aggregator and an update , and updates node features by
A GNN starts from a constant feature and applies layers , with parameters shared by all graphs. Its graph-level output after rounds is a read-out of the multiset .
For every GNN, read-out, depth and pair of graphs , (of possibly different sizes):
The statement fixes no architecture and no feature space: it quantifies over all message, aggregation, update and read-out functions.
If every layer's update is injective, then equal features are exactly equal WL colours (Xu et al.).
The result. The bound says that a GNN's ability to separate graphs is capped by a cheap combinatorial procedure. Every pair of non-isomorphic graphs that WL fails to separate — all regular graphs of the same degree and size, such as and — is also inseparable by every message-passing GNN, whatever its width, depth or training. This limitation motivated the higher-order and subgraph-based architectures discussed later in Ch. 7. The companion result explains why architectures with injective (sum-type) aggregation, such as GIN, are the maximally expressive members of the class, and the max/mean example explains why common aggregators fall short of it.
Formalizing it. The results are proved on paper; to the knowledge of this mission none has a machine-checked proof. The formalization makes explicit what the informal statements leave open: that the comparison needs parameters shared across graphs, that it concerns featureless graphs, which flavour of layer is covered, and in what sense "equivalent to one step" holds. It reuses a published 1-WL colour refinement (WLIdentification), so the GNN results connect to the platform's existing WL statements.
The statements are close to their definitions, and the difficulty is in the bookkeeping rather than in an idea. The comparison is between two different graphs, whose node sets are different types, so the relation between features and colours has to be carried across graphs rather than within one; equalities of colour multisets over neighbourhoods have to become equalities of multisets of messages, and histograms of colours have to become multisets of features. The / example needs the colours of a regular graph at every round and a separate non-isomorphism argument. A tempting shortcut, defining the GNN's features to be the WL colours, proves nothing: the goal quantifies over all GNNs.
Graphs are the published OAI.WLIdentification.Graph (order , Boolean symmetric loopless adjacency on Fin n); the WL test is its neighborColor and neighborHistogram, featureless and with history-carrying colours. The book numbers no theorems, so every item is cited by section, equation and printed page.
Conventions committed to:
Infrastructure needed is light: multiset bijections along equal maps (Multiset.map), induction over rounds, and finite computations on six-node graphs. The induction lemmas relating features to colours across two graphs are reusable for any further GNN-expressivity statement (higher-order WL, subgraph GNNs). Proofs of the milestones, of the companion, and alternative proofs of the goal through the companion are welcome.
A recurrent neural network (RNN) processes an ordered stream while retaining a summary of earlier inputs. The same update rule is applied at every time step, so it is natural to ask whether shifting the input stream simply shifts the resulting sequence of summaries. The answer depends on how the run begins. The first summary is supplied as an initial state, while the first input encountered after a shift can be different. Bronstein, Bruna, Cohen and Veličković use this boundary effect to explain a precise form of temporal translation equivariance for RNNs in §5.7 of Geometric Deep Learning (arXiv:2104.13478v2, pp. 90–93).
The claim matters when the same sequential model is applied to streams presented with different starting times. Without a specified boundary convention, the shared update rule alone does not guarantee that corresponding hidden states agree. The chapter's zero-padding construction makes that convention explicit. Its condition on the initial state can then be stated independently of a particular architecture or training procedure. The book numbers equations but no theorems or lemmas here; the mission's items are cited by section, equation, page, and, for a marginal statement, “side-note.”
Let be the input at time , let be its hidden summary, and let be a shared update map. Given a seed , equation (38) defines a run by
The first processed input is ; is unused. This is the book's time convention, including the named state (Bronstein et al., §5.7, p. 90, equation (38)). The update map is arbitrary: the results concern the recurrence itself, so they do not require the affine layer and activation used as one example in equation (39).
A left shift by steps replaces the input at time with the old input at time . A left-padded input of length is
Here is the zero vector in . The original input begins at time . The two runs being compared use the same update map and the same seed. This is the exact padding convention displayed on p. 93 of the book (Bronstein et al., §5.7, p. 93).
The capstone is the chapter's one-step equivariance claim. For every update map, input sequence, and seed fixed by the zero-input update, one or more zero-padding steps suffice:
The multi-step side note extends the conclusion to every with :
The milestone list also records the book's unpadded boundary counterexample and its observation that a contraction has a unique attracting fixed point. The latter is represented by an already proved, reusable Banach fixed-point theorem rather than a second draft of the same result (Bronstein et al., §5.7, pp. 92–93, equations (40)–(42) and side-note).
The equivariance theorem identifies a checkable condition under which the hidden-state sequence tracks a left-shifted input exactly, including at the first state. It also marks the limit of the informal idea that sharing the same update map across time automatically creates shift equivariance: the unpadded run can fail already at time . The fixed-point condition is therefore part of the mathematical claim, rather than an implementation preference (Bronstein et al., §5.7, pp. 92–93).
The RNN shift statements are targets for machine-checked proofs. The contraction milestone already has a machine-checked proof in the referenced CursoEDO.contraction_fixed_point theorem. A completed development would make the boundary convention and the arbitrary-update-map quantifiers available for later statements about sequential models. The recurrence and padding definitions are reusable whenever a discrete-time state update is compared before and after a shift.
The tempting comparison takes two runs that begin with the same seed, then tries to pair the shifted run's state at with the original run's state at . At the first step, those states have encountered different input histories. Equations (40)–(41) display the mismatch: the original run has applied to its first input, while the shifted run still uses the supplied seed at the corresponding update. For an arbitrary and arbitrary first input, the states need not agree (Bronstein et al., §5.7, p. 92). A shift statement that omits its padding length or seed condition would therefore assert something the chapter explicitly rejects.
Lean represents and as functions on Fin k and Fin m; time and padding lengths are natural numbers. The run uses and consumes at its next update. The padding function returns the zero vector through index and then the correspondingly indexed original input. These definitions cover every finite dimension, including zero-dimensional edge cases, while the unpadded counterexample uses one input and one hidden coordinate.
The target ranges over all update maps and all input sequences; it does not impose a special neural-network parameterization. The seed is any fixed point of , not necessarily the zero state, and the zero-input update need not be the identity map. The formal statements include time and the endpoint . No contraction assumption is needed for shift equivariance itself; contraction enters only the separate existence-and-convergence milestone. The contraction theorem is stated for a nonempty complete metric space, which includes the finite-dimensional real hidden-state spaces used here.
The work requires a small discrete recurrence interface, an exact padding definition, and proofs for the boundary counterexample and shift identities. Those two definitions and the shift results can also support variants with a nonzero padding vector. The LSTM equations of §5.8 have a separate gated state model and are outside this mission's formalization scope. Contributions that keep the full fixed-point hypothesis and the stated boundary cases are welcome.
Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.
This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.
Fix and the ring graph with nodes , arithmetic taken modulo . A signal is a vector with entries in a commutative ring , for instance .
In Lean the index set is ZMod n with [NeZero n], is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.
For every matrix over a commutative ring ,
The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.
With ,
The book prints this with in place of , which is off by a factor for ; the corrected identity is stated. The transform form of the Convolution Theorem, with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.
The goal identifies the space of linear translation-equivariant maps on with the convolutions, an -dimensional space parametrised by the filter . This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.
Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.
The direction "" is a one-line consequence of the commutativity of circulant matrices. The content is "": the equation is an equation between matrices, and it has to be turned into the statement that the entries of are constant along every cyclic diagonal, with the indices handled modulo . The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the -th roots of unity in which is invertible; over a general commutative ring, such as or , the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives used in the exponents and the arithmetic of .
ZMod n with [NeZero n], so and matrices are finite; no lower bound is needed (for , and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val , as on the page.Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on and that on does not commute with .ZMod.dft, and the factor is written out in its statement.No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.
IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore want, for a given target unitary, a circuit of the least possible depth, not merely some circuit.
Amy, Maslov, Mosca and Roetteler (arXiv:1206.0758, IEEE TCAD 2013) gave an exact, depth-optimal synthesis algorithm, MITM-factor, based on a meet-in-the-middle search. With it they found the first -depth-3 circuit for the Toffoli gate and improved circuits for several standard gates. Approximate synthesis methods such as the Solovay–Kitaev algorithm (Dawson–Nielsen) produce short circuits but not optimal ones. The paper is a standard reference for exact, optimal synthesis over Clifford+, and later depth- and -count-optimal search methods start from it.
Fix qubits. is the group of complex matrices with , where is the conjugate transpose. An instruction set is a set of gates closed under inversion. A gate acts on some of the qubits and as the identity on the rest.
A depth-one circuit applies gates of to pairwise disjoint sets of qubits at once. is the set of unitaries of depth-one circuits. A circuit of depth is a sequence of layers , and it implements . Let
so is the set of unitaries implementable in depth , and write .
MITM-factor runs . At step it builds and tests whether ; if so it returns the concatenation of the two witnessing circuits. Otherwise it tests in the same way. If no step succeeds, it returns nothing.
In the Lean development the layer set is a finite set V of unitaries standing for , S V i is , circuits V i is the set of circuits of layers (lists over V), and mitmFactor V U l is the algorithm.
For every finite , unitary and , with :
and a returned circuit lies over , implements , has , and for every circuit over of positive depth implementing . For even the decided range is exactly . If , the counted cost satisfies
The goal fixes no instruction set and no gate. It is the paper's correctness and running-time claim for the search itself.
In attack order:
The result. Searching all circuits of depth at most takes steps. MITM-factor needs only about , up to a logarithmic factor: a square-root saving that made exhaustive depth-optimal synthesis of three- and four-qubit gates feasible. Its correctness is what lets a computer search certify optimality: when the search fails up to depth , no shorter circuit exists. The paper's non-existence statements, such as the absence of shallower circuits for particular gates, rest on this.
Formalizing it. The result is proved in the paper, informally and briefly. No machine-checked version is known to exist. The mission produces a checked statement of what the search decides, which repairs two boundary cases of the printed claim (see Formalization scope), and a cost bound with an explicit constant in place of the . Lemma 1 and the generation step are reusable for any meet-in-the-middle search over a monoid generated by a finite set.
The mathematics is elementary; the difficulty is in stating exactly what the algorithm does. The obvious reading, "the algorithm decides depth at most ", is false for odd : the last step also tests depth and may return a circuit of that depth. "Returns a circuit of minimal depth" is false for , whose minimal depth is never tested. A proof therefore has to track the loop's first success through two interleaved tests per step, and connect sets of unitaries to circuits as lists of layers. For the cost bound, the step from per-iteration costs to the total needs the geometric-sum bound in a form the paper misprints: fails at , .
Unitaries are elements of Matrix.unitaryGroup (Fin n → Bool) ℂ; is the group inverse.
The layer set V is an arbitrary Finset of unitaries. The paper's argument uses nothing about beyond finiteness, and milestone 1 relates , defined over the shared QAlgorithms gate and circuit layer, to this setting. Hypotheses on V appear only where used: closure under inverse for milestone 2, for the cost clause.
Circuits are Lists of layers, implementing their List.prod, head leftmost, as "" on p. 4. The algorithm returns a circuit, not a unitary. The "any circuit" of the pseudocode is a choice of witnesses.
Corrections, each disclosed in the items:
Cost model. The running time is a counted cost, built from the sets the run actually generates:
These are summed over the iterations executed, up to the first success. Logarithms are Real.logb 2. The constant is the mission's explicit form of the paper's .
Trivializing readings are ruled out: the cost is not defined from , which would make the bound an identity about powers, and the goal is not an existence claim about some algorithm with that cost. A circuit-valued output compared against every circuit over prevents a content-free minimality clause.
Not covered: Theorem 1 and Theorem 2 with Lemma 2 (controlled- costs and -depth with ancillas), the -depth variant of §3.1, the pruning of §4, and the computational results of §§5–6.
Welcome contributions: proofs of the milestones, lemmas on circuits and S (for instance ), and a list-based model of the sort-and-search cost.
A Boolean function can react differently to changing one input coordinate and changing several coordinates together. Measuring this difference is a question about the local complexity of total Boolean functions. The Block Sensitivity vs. Sensitivity campaign records exponents that quantify how large this difference can become along families of functions with increasing sensitivity.
This mission records the exact exponent
Its construction is already accepted and public. The mission expresses that result using the campaign's shared definition, so that its value can enter the same record as earlier entries. The logarithmic expression is the target; the displayed decimal is an approximation. No optimality claim is part of this mission.
A total Boolean function on coordinates is a map , defined on every binary input. For an input and a set of coordinates, write for the input obtained by flipping exactly the bits indexed by .
A coordinate is sensitive at if . The sensitivity counts those coordinates, and is the maximum of over all inputs. A nonempty coordinate set is a sensitive block at if . The block sensitivity is the largest number of pairwise disjoint sensitive blocks at that input. The quantity is its maximum over all inputs.
Every block in one block-sensitivity witness is tested at the same input. The blocks are disjoint as coordinate sets; their sizes need not be equal. These conventions are those of the shared foundation mission, rather than complexity measures defined only on selected inputs or on a promise domain.
The goal is the campaign proposition . Explicitly, for every real and every natural number , there must exist a natural number and a total Boolean function satisfying
Both the dimension and the function may depend on and . The sensitivity threshold is essential: a favorable ratio for one bounded example does not establish this statement. For example, choosing successively smaller positive losses and increasing thresholds produces a sequence of finite total Boolean functions with unbounded sensitivity and exponents approaching .
The exact numerator is the natural number
The denominator inside the logarithm is . Both logarithm arguments exceed one. There is no division by a zero logarithm, and the result uses ordinary real powers. The goal does not assume a finite construction certificate or the existence of a suitable labeling as a hypothesis.
The accepted construction theorem also proves the strict comparison
It improves the earlier public exponent, approximately , by approximately . The full proof constructs actual Boolean functions and establishes the asymptotic quantifiers; the numerical approximation alone is not the evidence for the separation.
The complete construction has passed local Lean kernel verification and Prove2Me verification. Its accepted submission is a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. The source uses ordinary checked proofs with the standard axioms propext, Classical.choice, and Quot.sound. Its final statement spells out sensitivity and block sensitivity directly through finite sets. The campaign goal uses the existing shared definitions for those same quantities, and its proof explicitly establishes the equivalence needed to transfer the accepted result.
A lower bound on block sensitivity at one input must be combined with an upper bound on sensitivity over every input. Local calculations that ignore the latter maximum can overstate the separation. Likewise, overlapping sensitive blocks cannot be counted as a disjoint family. These requirements persist through the construction and the passage to arbitrarily large sensitivity.
The exponent also depends on exact integer growth rates. Rounded numerical scores can identify candidates, but they do not establish the final real-power inequality. A complete proof must account for finite construction constraints, the complexity measures of the resulting functions, and the exponent loss allowed in the asymptotic statement. The accepted result includes these steps. This mission records that established result rather than a proposed stronger threshold awaiting construction.
The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Inputs are functions Fin n → Bool, and outputs are Bool. Sensitivity and block sensitivity are natural numbers obtained by finite maxima. The campaign proposition quantifies over positive real losses and natural sensitivity thresholds.
Dimension zero is permitted by the representation, but its sensitivity is zero and it cannot witness any required threshold . Empty block families contribute zero; every counted block is nonempty. There are no hypotheses that can make the target vacuous. The shared definition and finite-certificate references are retained from the campaign template. The only new result recorded here is the improved separation exponent and its exact campaign formulation. Attribution to the original OpenAI development and Robin Kothari/Codex is retained in the accepted construction source; the new construction is credited to yousofy with Codex.
yousofy with Codex, Six shared defect tolerances improve the sensitivity exponent to 2.1308255794, Prove2Me, 2026. Accepted complete construction.yousofy with Codex, Earlier strict exponent checkpoint, Prove2Me, 2026. Public comparison theorem.Newtonian gravitation can be written in two ways. In Newtonian gravitation (NG), spacetime has a flat derivative operator and a scalar potential obeying Poisson's equation, and bodies are pushed off the straight lines of by the force . In geometrized Newtonian gravitation (GNG), also called Newton–Cartan theory, the potential is absorbed into a curved derivative operator whose geodesics are the trajectories of freely falling bodies. This is the same geometrization that general relativity performs. Trautman (1965) proved that the two pictures pass into each other.
Weatherall (2016) asks whether NG and GNG are the same theory. He represents each theory by a category of models and calls two theories equivalent when there is an equivalence of categories that preserves empirical content. The answer depends on the arrows chosen for NG:
This is the gravitational twin of the electromagnetic question "potentials vs. field strengths" treated in the companion missions on Weatherall's Understanding Gauge. The other side of the Newton–Cartan story, the classical limit of general relativity, is described under Significance.
Following Weatherall (p. 3), spacetime is , here in one global chart E = Fin 4 → ℝ with index 0 for time. The classical metrics are (tt) and (hh). Their slices are complete copies of , as Weatherall requires.
A derivative operator is a smooth field of Christoffel symbols Γ x a b c , symmetric in , acting by
It is compatible when and . Curvature uses Malament's sign convention:
Other notation:
geomΓ).gaugeΓ).The objects of the categories are:
IsNG Γ φ): compatible, flat and a smooth potential . The mass density is .IsGNG Γ): compatible satisfying, for some smooth ,The arrows are diffeomorphisms of that preserve and and carry one derivative operator to the other through the transformation law
(IsGNGArrow). NG₁ arrows also preserve (IsNG1Arrow). NG₂ arrows are pairs with , where carries the gauge-transformed pair to (IsNG2Arrow).
ng2_equiv_gng, Weatherall Prop. 6.1)Geometrization , has these properties:
This is exactly the "full, faithful, essentially surjective" route of Weatherall's proof in App. A. These three properties together are equivalent to an equivalence of categories.
geometrization, Prop. 2.1 (Trautman). For flat compatible and Poisson's equation, has these properties:
recovery, Prop. 2.2 (Trautman). Every classical spacetime satisfying (1)–(3) comes from some flat and potential obeying Poisson's equation.gauge_iff, the non-uniqueness remark after Prop. 2.2. A second pair works iff and . Weatherall states the "if" direction and his proof of Prop. 6.1 uses the "only if" direction. The iff is Malament's Prop. 4.2.5. Note that is allowed: the gauge includes time-dependent uniform accelerations (Corollary VI).geom_naturality, the key computation in App. A. A metric-preserving diffeomorphism carrying to carries to iff it carries to .ng1_not_equiv_gng, the NG₁ row of Table 1 (§6, p. 18). No object map NG₁ → GNG preserves empirical content while inducing bijections of hom-sets. Weatherall states this in prose without a proof. The intended argument is that two NG₁ models related by a nonzero gauge share a geometrization but have no NG₁ arrow between them.Assignment questions ask whether every member of a family can be served by a different resource: committees that each need a distinct member as representative, or tasks that each need an admissible worker. The classical answer is Hall's theorem (Hall 1935): a family of sets has a system of distinct representatives exactly when every of its sets together contain at least elements. Operations research needs more than that. Representatives may be allowed to serve several sets within prescribed bounds, some elements may be required to appear, two families may have to be served by one common list, and the representatives may have to meet each class of a partition a bounded number of times.
Chapter II, §10 of Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) derives all of these as feasibility statements for network flows. The section collects results of Hall (1935), Mann and Ryser (1953), Hoffman and Kuhn (1956) and Ford and Fulkerson (1958). Its last results are the common system of restricted representatives theorem and the partition-constrained theorem of Hoffman and Kuhn.
Fix a fundamental set , with the element identified with its index . A family is a list of subsets of indexed by ; two indices may carry the same set. For , the index set is the set of indices of the elements of , and .
A list of representatives is a choice of elements of , where represents . The number of occurrences of is the number of indices with .
For , denotes the index set of when it refers to .
A common SRR for and in which occurs at least and at most times exists if and only if, for every ,
The bounds are integers with ; the instance reads .
In attack order:
for all and .
These theorems are the combinatorial face of the integral flow theorems of the same chapter. The SRR theorem governs many-to-one assignment with quotas, where each resource must be used between a minimum and a maximum number of times. The marginal-element theorems decide when a prescribed set of resources can all be used; Mann and Ryser applied their sufficient condition for this to Ryser's theorem on extending Latin rectangles to Latin squares (p. 62). The common SRR theorem decides when two families can be served by one list, the setting of simultaneous assignment along two classifications. Theorem 10.10 adds quotas per class of a partition of the resources. Corollary 10.4 is König's edge-colouring theorem for regular bipartite graphs, in matrix form.
All of these results are classical and proved. Hall's theorem is in Mathlib and is referenced here. As far as a search of the platform shows, none of the quota, marginal-element, common-representative or partition versions has a machine-checked statement or proof. The mission produces faithful statements of the book's §10 results on a shared set of definitions, and invites formal proofs of them.
Necessity of each condition is a counting argument. Sufficiency is the content, and the natural first idea does not work. Applying Hall's theorem to a family in which each set is repeated according to its bounds handles upper bounds but not lower bounds. The two families of the common problem cannot be treated separately either: an SRR for and an SRR for with the same occurrence counts need not combine into one list, because the identification of positions must respect both families at once. In the book every sufficiency proof passes through an integral feasible flow or circulation, and the cut conditions of the circulation theorem must be reduced case by case to the stated inequalities.
is Fin m and a family is Fin n → Finset (Fin m), indexed from . A list of representatives is a function Fin n → Fin m, an SDR is an injective one, and the occurrence count is a Finset.card. A common SRR is a pair of a list and an Equiv.Perm (Fin n). The index set is X.biUnion S. The occurrence bounds are natural numbers. The page states only , but the bounds count occurrences, and with real bounds Theorems 10.5 and 10.8 are false. Every inequality involving subtraction is evaluated in , so no term truncates at zero. The partition in Theorem 10.10 has nonempty, pairwise disjoint blocks covering . In Corollary 10.2 the maximum runs over all (); the page prints as the last index. In Theorem 10.10 the first union is over ; the page prints .
The trivializing formalizations are ruled out explicitly. An SRR without the occurrence bounds, and a "common SRR" consisting of two unrelated SRRs, are both excluded: the definitions carry the bounds, and a common SRR is one list whose entries each represent one set of each family through the permutation .
Beyond the paper. Two sharpness probes restate Theorems 10.5 and 10.8 with real bounds . Both are expected to be false: with , , and , , the conditions hold while no list of length one contains both elements. Disproofs are the sought outcome.
A complete development needs Hall's theorem (available in Mathlib) and, for the book's route, an integral flow or circulation feasibility theorem; purely combinatorial proofs by induction are equally welcome. The definitions are reusable for the zero-one matrix results of the following sections. Proofs of individual milestones are welcome, in any order.
In the present paper we introduce and study Bosonic Gaussian classical-quantum (c-q) channels; the embedding of the classical input into quantum is always possible and therefore the classical entanglement-assisted capacity C_{ea} under appropriate input constraint is well defined. We prove a general property of entropy increase for weak complementary channel, that implies the equality C_{ea}=C (where C is the unassisted capacity) for certain class of c-q Gaussian channel under appropriate energy-type constraint. On the other hand, we show by explicit example that the inequality C<C_{ea} is not unusual for constrained c-q Gaussian channel.
This mission is the statement-level formalization of Gaussian classical-quantum channels: gain of entanglement-assistance (arXiv:1211.4774v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §3, unnumbered criterion (14): Gaussian c-q iff isotropic K (§3, unnumbered criterion (14): Gaussian c-q iff isotropic K, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets ; higher is better.
For every and every integer , the goal asks for a total Boolean function with and . The shared definition SensitivityCampaign.AchievesExponent expresses this requirement. This is an open proof target.
Using a finite certificate. Choose a total Boolean function , an input , and integers . Prove , , and , then apply SensitivityCampaign.finite_certificate. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Direct proofs of the asymptotic goal are equally welcome. Use exact certified bounds; numerical estimates alone do not establish the target.
Background: OpenAI problem 132 and the campaign proposal.
Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.
The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.
A total Boolean function on coordinates is a map defined at every binary input. At an input , a coordinate is sensitive if flipping that bit changes the output. The sensitivity counts these coordinates, and is the maximum over all inputs.
A sensitive block at is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.
For every real and every integer , establish the existence of a dimension and a total Boolean function such that
The number is an exact finite decimal. The witnesses may depend on both and . This is the campaign proposition , and the main theorem instantiates its template literally.
A supporting finite-family theorem asserts that, for every natural number , there is a finite total Boolean function with
The associated exact logarithmic quotient is approximately . It is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent. The fixed prefactor is independent of , and the lower bound concerns explicit nonempty pairwise disjoint sensitive blocks at the all-zero input.
Any fixed exponent strictly below gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.
The full construction, its actual Boolean functions and the exponent conversion have passed complete local Lean kernel checks with only the standard three axioms. The shared-labeling lemma is separately accepted and publicly Proved. The main theorem currently has a checked reduction on Prove2Me; the larger finite-family dependency still awaits server acceptance after combined submissions exceeded the300-second verification limit. This mission records the exact proved local statement while preserving that server-status distinction.
The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.
A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.
A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.
The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.
The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.
yousofy with Codex, Shared local-lemma labelings: exponent2.1303, Prove2Me,2026. Main statement and proof submissions.Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.
The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.
A total Boolean function on coordinates is a map defined at every binary input. At an input , a coordinate is sensitive if flipping that bit changes the output. The sensitivity counts these coordinates, and is the maximum over all inputs.
A sensitive block at is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.
For every real and every integer , establish the existence of a dimension and a total Boolean function such that
The number is an exact finite decimal. The witnesses may depend on both and . This is the campaign proposition , and the main theorem instantiates its template literally.
A supporting finite-family theorem asserts that, for every natural number , there is a finite total Boolean function with
The natural number indexes distinct finite construction instances; it is not a dimension bound. The fixed prefactor does not depend on . The associated exact logarithmic quotient is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent.
Any fixed exponent strictly below gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.
The main theorem and its reusable finite-family input have accepted proofs and public Proved status. The exact growth-rate lower bound log(201838849)/log(7922), approximately2.13012479519, is also separately accepted. These facts are recorded with source hashes and acceptance receipts in the accompanying proof package.
The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.
A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.
A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.
The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.
The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.
yousofy with Codex, Coupled target and guard profiles: exponent2.1301, Prove2Me,2026. Main statement and proof submissions.A rule that assigns an output bit to every input string can respond differently to changing one bit and changing a group of bits. Sensitivity counts individual changes that affect an output. Block sensitivity permits disjoint groups of coordinates to change separately. Understanding the largest possible difference between these measures is a question about the dependence of Boolean functions on their inputs.
Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. Determining the sharp quantitative relation between sensitivity and block sensitivity remained a separate problem. OpenAI's 2026 result disproved a universal quadratic bound for total Boolean functions. Subsequent accepted results include the 2.075 theorem by Robin Kothari and Codex and the accepted 2.085 certificate developed for yousofy with Codex. This mission records a stronger quantitative target, 2.119.
A total Boolean function is a map
that assigns an output to every length- bit string. For an input and a coordinate set , let denote the string obtained by reversing exactly the bits in .
A coordinate is sensitive at if . Write for the number of such coordinates, and define
A sensitive block at is a nonempty coordinate set with . Let be the largest size of a family of pairwise disjoint sensitive blocks at the same input, and set
Each member of a block family is flipped separately from the original input. The definitions use finite coordinate sets and finite families of blocks.
The main theorem is
Explicitly, for every real and every natural number , there must exist a natural number and a total Boolean function such that
The formal statement is SensitivityCampaign.AchievesExponent (2.119 : ℝ). Both and may depend on and . The decimal denotes the exact rational number displayed above. The claim includes arbitrarily small positive exponent loss and arbitrarily large sensitivity; neither quantifier is optional.
In particular, the statement gives a fixed exponent 2.118 for functions of unbounded sensitivity, strictly above 2.1. The target is a specific checkpoint in the broader problem of determining the optimal separation exponent. It does not assert that the displayed endpoint is attained without exponent loss.
The target extends these earlier quantitative bounds and crosses the campaign's 2.10 checkpoint. It requires the separation to persist beyond every sensitivity threshold, so a favorable comparison confined to bounded sensitivity would not establish the result. It also leaves the exact optimal exponent unresolved.
The new contribution is a certified finite construction and formal proof within the existing nine-predicate framework. The proof retains the generic development and attribution from Kothari and Codex's accepted 2.075 contribution, including its credit to abhishekdpseok's accepted 2.0635 proof and the earlier OpenAI and community work. The new certificate and its assembly were developed for username yousofy with Codex.
The complete self-contained source has passed standalone compilation in Lean 4.33.1, with only the standard axioms propext, Classical.choice, and Quot.sound. Its numerical certificates and source correspondence have also undergone independent checks. Prove2Me accepted the complete proof on 20 October 2026, submission bb3251a4-f00f-4b06-962a-97be2de5db1b. The public theorem and proof record records its verification status. Further work can examine the proof, improve its reusable interfaces, or establish stronger bounds.
The sensitivity bound must hold at every input. A calculation only at an input supporting many sensitive blocks does not control this maximum. Likewise, a collection of output-changing coordinate sets provides the required block bound only when every set is nonempty and the sets are pairwise disjoint.
The asymptotic requirement creates a separate difficulty. Increasing the dimension alone does not force sensitivity to increase, because added coordinates may be ignored. A complete argument must provide witnesses above every prescribed sensitivity threshold. Finally, the exact rational exponent needs rigorous comparisons: an approximate numerical score alone does not prove the stated inequality.
The shared Lean representation is f : (Fin n → Bool) → Bool, using the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to any family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.
The target imposes no normalization on or a distinguished input, and it includes no promise restricting the function's domain. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy . Natural-number complexity measures are cast to real numbers before real exponentiation. Every positive is included, even when is nonpositive.
The complete source imports Mathlib and the unchanged campaign definition. Existing reusable infrastructure includes the complexity measures, coordinate reindexing results, and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger certified bounds are welcome, while preserving totality, global sensitivity, and the unbounded-sensitivity requirement.
A rule that assigns an output bit to every input string can react very differently to changing one bit and changing several bits together. Quantifying that difference is a basic question about Boolean functions in theoretical computer science. Sensitivity measures how many individual bit changes can affect one output; block sensitivity allows disjoint groups of bits to change separately. The question here is how far apart these two measures can grow.
Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. The sharper question about the exponent remained. OpenAI's 2026 superquadratic separation ruled out a universal quadratic bound. The subsequent accepted exponent-2.075 contribution by Robin Kothari and Codex provides the established comparison point for this mission. The target is the stronger quantitative bound 2.085.
A total Boolean function is a map
that assigns an output to every length- bit string. For an input and a set of coordinate positions, write for the string obtained by reversing exactly the bits in .
A coordinate is sensitive at when . Write for the number of such coordinates and define
A sensitive block at is a nonempty coordinate set with . Define as the largest size of a family of pairwise disjoint sensitive blocks at that same input, and set
Each block is flipped separately from the original input. All functions and coordinate sets in these definitions are finite.
The main theorem is the campaign statement
Its full meaning is
The exact formal target and its proof status are recorded here. Both the dimension and the function may depend on and . The decimal denotes an exact rational number. The statement permits arbitrarily small positive exponent loss and explicitly requires arbitrarily large sensitivity. For example, choosing gives exponent 2.084 at every requested sensitivity threshold. This is a concrete checkpoint within the broader problem of determining the optimal separation exponent.
The target raises the established exponent bound from 2.075 to 2.085, with the quantifiers stated above. In particular, it supplies a fixed exponent strictly above 2.075 for a family whose sensitivities are unbounded. This distinction matters: a favorable comparison for one finite Boolean function, without an appropriate asymptotic conclusion, would not establish the target.
The new contribution is an eight-layer numerical certificate within the existing nine-predicate framework. Its foundation comes from Kothari and Codex's accepted 2.075 proof, which retains credit to abhishekdpseok's accepted 2.0635 development and the earlier OpenAI and community proofs.
The complete self-contained proof has compiled successfully in Lean 4.33.1. The certificate and its assembly have also passed independent checks. Prove2Me has accepted the complete proof, submission c6096517-61e7-4f51-bc68-c1521d61eb65, on 20 October 2026. The target record is the reference for subsequent verification status. The separate proof explanation supplies the construction details and exact arithmetic.
The sensitivity estimate must hold at every input. Checking only the input that supports many sensitive blocks leaves that requirement unresolved. Likewise, a collection of output-changing sets is insufficient unless its members are nonempty and pairwise disjoint.
The asymptotic quantifiers impose a further requirement: witnesses must exist beyond every sensitivity threshold. Merely increasing the dimension does not establish this, since a function can ignore added coordinates. Finally, the exact rational exponent requires rigorous arithmetic bounds; a numerical logarithm estimate alone does not prove the formal statement.
The shared Lean representation uses f : (Fin n → Bool) → Bool and the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to a family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.
The target imposes no normalization on or on a distinguished input. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy the required sensitivity threshold . Real exponentiation is applied after casting the natural-number complexity measures to real numbers.
The development uses Mathlib and the unchanged campaign definitions. Reusable infrastructure includes the complexity-measure definitions and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger rigorously certified bounds are welcome contributions. Any stronger target should preserve totality, global sensitivity, and the unbounded-sensitivity requirement.
819ad4c6-aa25-48ca-82e9-c8df39c182c0. Theorem and proof record.f80a3f37-72fa-4d56-a094-3e4d351764f3. Theorem and proof record.Product recalls are frequent and costly. A firm that launches an innovation without thorough quality assurance testing gains time on the market but risks a recall, which brings direct costs (repairs, refunds, legal settlements) and lasting damage to the product's reputation. Testing removes the risk but delays the launch, and while a firm tests, a rival can take the market with its own innovation. Kim, Koenigsberg and Ofek (SSRN 3492105, November 2019; published in Management Science, 2022, doi:10.1287/mnsc.2022.4303) model this trade-off as a two-period game and ask when competing firms test and when they rush to market. Their answer for two identical firms, Proposition 2, is the goal of this mission: depending on the failure probability of an untested product, neither firm tests, both test, or exactly one tests.
Two firms each hold an innovation. The mature product has quality and the innovation quality , with . Production costs nothing. There are two periods, .
Before , each firm chooses its testing decision simultaneously. A firm that tests () sells its mature product at and a fail-proof innovation at . A firm that does not test () launches its innovation at . The untested innovation fails during that period with probability , independently across firms. On failure the firm pays a recall cost , where is a fixed cost, a penalty per unit of first-period revenue and the firm's first-period profit, and at it sells a recalled innovation of quality , with reputation damage .
In each period a new unit mass of consumers arrives, with tastes uniform on . A consumer of taste gets utility from a product of quality at price and buys the product of greatest utility if that utility is nonnegative. Given the two products on offer, the firms set prices; the pricing subgame is the one-period price game, and its equilibrium profit for quality against is written . The testing game is the simultaneous game in which a firm choosing against a rival choosing earns the expected two-period payoff , and an equilibrium is a pure Nash equilibrium of it.
With the cutoffs of the paper's appendix,
and , the interval between the two roots of the quadratic in given by (A.3):
and the two symmetric equilibria never coexist.
Proposition 2 is the paper's main result for competition. It shows that competition changes the testing decision in two directions. A rival's early launch makes simultaneous rushing less costly, because identical products earn nothing in the first period and the revenue-based recall penalty then vanishes. Firms also try to differentiate their timing, which produces the asymmetric equilibrium in which one firm tests and the other does not. Comparing the result with the monopoly benchmark (Proposition 1) gives the paper's managerial conclusions: duopolists may skip a test that a monopolist would run (Corollary 2), and both firms test only when the fixed recall cost is large (Corollary 3).
The proofs in the paper are algebraic and partly omitted ("tedious algebra … available from the authors"). A formal development checks every case of the price equilibria, including the global deviations that the first-order conditions do not cover, and the exact boundaries of each equilibrium region. It also settles the boundary behaviour the paper leaves implicit: the regions are disjoint only off their boundaries. No machine-checked proof of any result of this paper is known.
Most of the work is in Lemma 1. The first-order conditions of the price game give the stated prices, but an equilibrium must also survive non-local deviations: the low-quality firm may undercut to take the whole market, and the high-quality firm may price below the region where both firms sell. Demand is piecewise in the prices, with kinks where one firm's market vanishes and a tie-splitting rule at equal qualities, so each best response is a maximization over several branches. The uniqueness half of the Bertrand bullet needs an undercutting argument. The cutoff characterizations then require sign control of a quadratic in whose discriminant can be negative, and of a denominator in that is negative for small .
All quantities are real numbers. The parameters are a structure with fields , and a predicate bundles the standing assumptions , , , , , . The page writes neither nor ; both are implicit and are made explicit here.
Demand is the Lebesgue measure of the set of tastes in that buy the product, with indifferent consumers counted with weight . A price equilibrium allows deviations to every nonnegative price. The period profit is revenue at the prices computed in the proof of Lemma 1, for the higher quality, for the lower and for equal qualities. It is computed from demand, so Lemma 1's profit formulas are theorems. The untested firm's objective of (A.1) is a positive affine transform of revenue and has the same best responses, so the price game is posed on revenue.
Lemma 1 identifies the unique price equilibrium for each of the two differentiated quality pairs as well as for equal qualities. The payoff is built from the recall events, each failing independently with probability , and from the period profits. Testing decisions are Booleans (true = test). Equilibria of the testing game are pure Nash equilibria with weak best responses, using the published agt_games predicate AGT.IsPureNash.
The cutoffs are written exactly as on p. 37. Every statement that uses requires its denominator to be positive, and every statement that uses requires the discriminant to be nonnegative; when these fail, the corresponding region is empty. The paper calls its regions "mutually exclusive", but at the boundaries a symmetric and an asymmetric equilibrium coexist, so the goal asserts exclusivity only between the two symmetric equilibria.
Trivializing formalizations are ruled out. Defining the payoffs by the four closed forms of the paper's proof, or the period profits by Lemma 1's formulas, would make the milestones definitional and the goal pure algebra. Here both are built from consumer choice.
Not in scope: the monopoly benchmark (Proposition 1, Corollary 1), Corollary 2 (proved only in a limit), the comparative statics of Corollary 4, the conditions and of (A.3), and the extensions of §5. Contributions are welcome on any milestone. Lemma 1's analysis of the vertical-differentiation price game with uniform tastes is reusable for other quality-competition models.
The Pratt–Arrow risk premium is the basic local measure of risk aversion under expected utility (EU): a decision-maker with a twice differentiable utility facing a small zero-mean risk at wealth pays approximately
variance times the index of absolute risk aversion (Pratt 1964; Arrow 1965). It is used throughout portfolio theory, insurance pricing and decision analysis, wherever a risk attitude has to be summarised by one number.
Much of decision theory since the 1980s replaces EU by rank-dependent utility (RDU, Quiggin 1982), which distorts cumulative probabilities by a probability weighting function . Its special case with linear utility is Yaari's dual theory (DT, Yaari 1987). Under these models risk aversion comes from two sources, the curvature of and the curvature of , and the variance alone no longer measures how much a small risk costs. Eeckhoudt and Laeven (arXiv:1612.03347v2, published in Operations Research, 2022) identify the missing measure: the second dual moment, or maxiance, the expected best of two independent draws of the risk. They show that under DT the local risk premium is proportional to the maxiance, and that under RDU it is the sum of a variance term and a maxiance term.
A finite lottery lists outcomes in increasing order with unconditional probability masses . Write and . The masses need not sum to one: the risks below are attached to one branch of a lottery and carry only that branch's mass. An RDU decision-maker with utility and weighting function evaluates a lottery by (4.1):
DT is the case (3.1). The paper assumes that is twice continuously differentiable with , and that is twice continuously differentiable with , , .
For a risk with cumulative distribution and mean , the unconditional variance and maxiance are
and denotes the total unconditional mass. For a probability distribution, (2.1).
Fix , , and initial wealth . Lottery pays with probability and with probability . Lottery takes mass from each branch of and puts the released mass on a middle outcome with . The RDU risk premium is for the that makes the decision-maker indifferent between and , that is, the solution of (4.2). The spread from with to attaches to the middle branch the risk , which takes the values each with unconditional probability . The DT construction with lotteries , , outcomes , premium and risk ( with probability each) is the same with and .
As jointly, with , , the moments of ,
The result. Formula (4.3) shows that, for a small zero-mean risk, an RDU decision-maker's premium splits additively into an EU part (variance times utility risk aversion ) and a DT part (maxiance times probability-weighting risk aversion ). Variance and maxiance appear on an equal footing, so the maxiance is the natural second risk measure for non-EU preferences, as the variance is for EU. The DT index plays the role of the Arrow–Pratt coefficient in the probability plane. The paper builds its global comparative risk aversion result (Proposition 5.1), its examples with Prelec's weighting function and its portfolio application on this local index.
Formalizing it. The result is proved in the paper by Taylor expansion, with "" left informal. This mission fixes the precise asymptotic meaning: a little-o remainder in the joint limit. It also makes definite the claims the paper takes for granted: that the premium exists and is unique, and that the moments of and take the stated values. No part of this development, nor any rank-dependent utility evaluation, is formalized on the platform or, as far as is known, elsewhere.
The obvious argument expands both sides of (4.2) and keeps "the second-order terms". This needs care on two counts. First, the premium is defined only implicitly, so its size has to be controlled before is expanded: the term is negligible only once is known. Second, the two leading terms have different orders, and , and the remainder must be uniformly small relative to their sum in a two-parameter limit. The tempting reading "small variance and small maxiance" (p. 4) with fixed is false: at fixed the dual term carries a relative error of order that does not vanish as . The DT step (3.4) needs the explicit solution (3.3) and the strict positivity of .
All quantities are real. A lottery is a pair of vectors indexed by ; the evaluation (4.1) is the finite rank-dependent sum, with cumulative masses computed from the vector. The sum equals the Stieltjes integral only for outcomes in increasing order, so the premium predicates keep the page's ranges and , which order and . Initial wealth is added to every outcome.
Committed conventions:
A formalization that defined the premium by its Taylor polynomial, replaced by the leading terms, or took the limit in alone would be trivial or false; the goal quantifies over every solution of the indifference and uses the joint limit.
Not formalized: the equivalence of (2.1) with the Stieltjes form, Proposition 5.1 (global comparative risk aversion), the examples of §6, the portfolio application of §7 and the non-binary generalisation of Appendix A.
Needed infrastructure: finite rank-dependent sums, Taylor expansion of functions with little-o remainders (Mathlib's taylor_mean_remainder family and Asymptotics), and the intermediate value theorem. Contributions welcome: proofs of the milestones, and a general Stieltjes-integral version of (4.1) for finitely supported distributions that would let later missions treat non-binary risks.
Mortgage lenders in the United States and Canada can insure a loan against default when it is originated. In the US the guarantee is typically provided by government-sponsored enterprises, in Canada by government-backed mortgage insurers. Such guarantees are usually discussed as risk-sharing devices, or criticized because they weaken lenders' incentives to screen borrowers. Ahnert and Kuncl (Bank of Canada Staff Working Paper 2019-47; published as Government Loan Guarantees, Market Liquidity, and Lending Standards, Management Science, 2024) isolate a different channel. Loans are later sold in a secondary market where buyers cannot tell good loans from bad ones, the lemons problem of Akerlof (1970). Insurance bought at origination changes which loans reach that market, and therefore its price and its liquidity.
The model is deliberately risk-neutral, so insurance has no risk-sharing value. Every effect comes from the interaction of screening incentives, private information at the interim date, and market segmentation between insured and uninsured loans. This mission formalizes the paper's characterization of the liquid equilibrium with loan insurance (Proposition 2, existence and parts 1–2) and the results that the paper's proof uses.
There are dates and a continuum of lenders , each with one loan. A loan pays at with probability , or if the lender screens at , and otherwise. Screening costs lender a private amount , distributed with distribution function supported on . At each lender privately learns the quality of its loan and a liquidity shock , , with . Its utility is , so a shocked lender values interim consumption more.
At a lender may insure its loan for a fee . Insurance guarantees , so an insured loan pays the safe amount . At loans can be sold to competitive outside financiers who do not observe screening, shocks or quality, but do observe insurance. There are therefore two markets, for insured loans at price and for uninsured loans at price .
Write . Lenders use a threshold rule: those with cost screen. The market for uninsured loans is liquid when shocked lenders sell good loans, (condition (2)). A liquid equilibrium (Definition 1) consists of screening and insurance choices, prices and a fee such that:
Without insurance, the break-even price (4) and the marginal lender's indifference (5) characterize the benchmark equilibrium of Lemma 1.
Assume , , and condition (35), which is equivalent to . Then a liquid equilibrium exists in which a share of high-cost lenders insures, with
fee and . Moreover, the price of uninsured loans is higher and the screening threshold lower than in every solution of the no-insurance system (4)–(5):
In attack order:
The result is the paper's positive case for loan guarantees. Insured loans are removed from the uninsured market in two ways. Shocked lenders who insure hold average-quality loans. Unshocked high-cost lenders who insure give up the option to sell their lemons later. Both effects improve the pool of uninsured loans traded, so rises, and the liquid equilibrium survives for smaller liquidity shocks: replaces the benchmark bound . The cost is lower lending standards (). The paper's welfare analysis (Proposition 4) and its regulation results (Proposition 5) start from this trade-off.
On the formal side, the paper's arguments are informal derivative computations and limit arguments in Appendix B. As far as is known, nothing in this model is machine-checked. Formalizing the result requires the equilibrium to be posed as a genuine fixed point: optimality among all screening and insurance choices, with sales chosen optimally, and break-even prices. The closed forms then become theorems, not definitions. The comparative statics in part 3 of Proposition 2 remain open for later work.
The closed forms follow quickly once one assumes the equilibrium structure: screeners do not insure, high-cost lenders are exactly indifferent about insurance, and the marginal screener is indifferent about screening. The work is in deriving that structure from Definition 1 and then exhibiting the equilibrium.
Everything is defined in the namespace LoanInsurance.Liquid, in one definitions file LoanInsurance.Liquid.Model. The conventions are:
Params with fields A, μ, ψ, ν, lam (the paper's ), etaBar () and F. The standing assumptions of §2 form the predicate Standing. The density on is replaced by what the paper uses: is continuous and strictly increasing on , below , and above .A trivializing formalization is ruled out: the equilibrium is never defined by the equations (5), (8) and (33) or by the closed forms. It is optimality among all four choices plus break-even. Neither nor is built into the definition. The goal is an existence statement whose witness must satisfy Definition 1.
A complete development needs elementary real analysis: monotonicity of linear-fractional functions, the intermediate value theorem for the fixed points (6) and (37), and case analysis on . Lemmas about the prices (4) and (33) are reusable across the milestones. Proofs of any milestone, and alternative formulations of Definition 1 that are proved equivalent, are welcome.
Retail chains routinely delegate replenishment decisions to store managers. The manager sees signals the head office does not: local events, weather, the mood of the neighbourhood. The head office (the principal) knows only the probabilities of these demand states. It also cannot observe lost sales directly, because unmet demand leaves no record, so it cannot simply pay the manager (the agent) on the true newsvendor cost. What it can observe is leftover stock and whether the shelf was empty when someone checked.
Alp and Şen (M&SOM 23(1):55–69, 2021) study performance measures built from these observable quantities. Under scheme , the agent is charged for leftover stock and pays a lump-sum penalty if the shelf is empty at the end of the period. One value of aligns the agent's order with the principal's optimal order in every demand state only when all states have the same demand variability (their Corollary 1). The paper's response is early inspection: scheme checks the shelf at an earlier time . Its Proposition 2 shows that with two demand states, a suitable inspection time and one penalty restore perfect alignment, even though the principal does not know the state.
The question belongs to the literature on sales-force and inventory incentives (e.g. F. Chen, Sales-force incentives and inventory management, M&SOM 2(2):186–202, 2000), where the agent's private information about demand is the central obstacle.
There is one period of length and two demand states . The agent knows ; the principal does not. In state , cumulative demand is a Wiener process with drift and standard deviation . So the period demand is and the demand up to time is . Write and for the standard normal distribution function and density, and .
The stock starts at a level and is raised to an order-up-to level . Leftover stock costs per unit and lost demand per unit, so the principal's expected cost is the newsvendor cost
Let be the critical fractile, . The principal's optimal level is .
Under scheme with unit weight on leftover stock, the agent's expected score, eq. (4) of the paper, is
Its derivative in , at , is the function of eq. (9):
In Lean these objects are agentCost, Φ, φ, omega, incentiveM, inspectionLHS and argminFrom in EarlyInspect.Align.Model. The principal's cost is the published InventoryControl.newsboyCost co cu μ σ.
Assume , and . Then there is with
and the penalty
achieves the following with inspection time . For every and both ,
The result shows that when the principal inspects is an incentive instrument in its own right. With end-of-period inspection, one penalty cannot align a manager across states that differ in variability. Moving the inspection earlier changes the stock-out probability differently in each state, and with two states that extra freedom is enough to make the manager's privately optimal order equal the principal's in both. Proposition 2 is the paper's headline claim, stated in the abstract and the conclusion. The paper generalizes its second consequence in Theorem 4: for more than two states, some with yields lower expected cost for the principal than scheme .
The paper states its results without proofs in the journal text; all proofs are in an online appendix. This mission states the goal and the results it rests on as machine-checkable statements. Two of them needed repair. As printed, Proposition 2 is false without a sign condition: in the paper's own case , , with , no exists. Theorem 3's "unique root" holds only on the feasible region . None of these results has been formalized before.
The principal's problem is the convex newsvendor problem. The agent's is not convex. The score adds a decreasing Gaussian tail to a convex function, and its derivative can change sign more than once on the real line. The obvious argument, " by the choice of , hence is the agent's optimum", fails twice. First, a stationary point need not be a minimizer: the agent's choice is the argmin of the score over , and that requires the sign pattern of on all of , which is Lemma 1 and Theorem 3. Second, the same must serve both states, and the condition of §4.2.2 under which the root is unique has to hold at the constructed in each state. The existence of is an intermediate-value argument whose sign condition is exactly the added hypothesis.
All quantities are real. Only the two normal marginals of the demand process are used, so the Wiener process is not formalized. The normal law is the published InventoryControl.newsboyDemand m s (mean , standard deviation ), and is newsboyDemand (t * μ) (Real.sqrt t * σ), with variance . The agent's weight is fixed to , as in Proposition 2. The principal's cost follows the text (leftover , lost demand ), not eq. (1), which prints the coefficients swapped. is characterized by .
The following hypotheses are added and disclosed in the items. appears in Proposition 2 and in milestone 5. and appear in Lemma 1, whose threshold divides by and whose second clause fails for negative . (nonnegative starting stock) appears in Theorem 3 and the goal. Standing hypotheses and appear throughout.
The goal cannot be trivialized by defining the agent's choice as a root of or as . Both choices are stated as sets of minimizers of the expected costs, and these sets are claimed to be singletons, so no vacuous reading is possible. A sorry-free check shows that the goal's hypotheses are satisfiable.
Useful infrastructure includes derivatives of Gaussian expectations of and of Gaussian tails, monotonicity and convexity of and , and the uniqueness of the critical fractile. These are reusable for any newsvendor-type model with normal demand. Proofs of individual milestones are welcome, as are proofs of the remaining results of the paper (Corollary 1, Theorem 3 parts 2–3, Theorem 4) as new statements.
Customers often need several complementary products, such as hardware and software, cars and financing, or jet engines and maintenance, sold by specialist firms that are complementors to one another. A recurring strategic move is for one complementor to launch an integrated system: a single offering that competes with the multi-component system its complementor still helps to supply. The paper's examples are AT&T's bundles of internet and entertainment services after the Time Warner merger, BMW's financing and leasing, Rolls-Royce's "power-by-the-hour" package of engines with maintenance, and Apple's music service competing with Spotify.
Reisinger, Schmidt and Stieglitz (Management Science, 2021) ask when such a move pays, and why it is observed even when the integrated system is neither better than the two-component system nor aimed at a different customer segment. Their answer separates the entrant's incremental profit into a direct effect (market expansion and conversion of customers to the integrated system) and a strategic effect: once an integrated system competes with the two-component system, the rival complementor cuts its component price while the entrant raises its own. The entrant thereby squeezes its complementor's margin. This decomposition follows the direct/strategic-effect analysis of Bulow, Geanakoplos and Klemperer (1985) and Fudenberg and Tirole (1984).
Two complementors and each sell one component of a two-component system with gross utility . Either may launch an integrated system with gross utility by paying an investment . Production costs are zero. The parameter measures substitutability between systems. Inverse demand is linear:
a system that is not offered having quantity zero. The model restricts to an admissible range: if , and if .
The game has two stages. In stage 1 the complementors decide simultaneously whether to launch an integrated system. In stage 2 they set prices. This gives three price subgames: no entry (i), accommodation (ii), in which only enters, and escalation (iii), in which both enter. A price equilibrium of a subgame is a pure Nash equilibrium in which a firm selling two products may change both prices at once. In stage 1, 's benefit of entering when stays out is , and 's benefit of entering when is in is . The thresholds and are the values of at which these vanish.
's incremental profit from entry splits into three parts:
These are the profits from market expansion, from conversion of customers to the integrated system, and from squeezing the complementor.
In the accommodation equilibrium, for every admissible :
Moreover, when there is a threshold such that for every admissible some makes the stage-1 outcome accommodation while
that is, enters although its integrated system loses money. The goal states this existence claim and does not fix the threshold.
The result gives a rationale for entry with an integrated system that is unprofitable on its own terms. The value of entry can lie entirely in the entrant's old business, through the margin it takes from its complementor. This matters for reading platform and ecosystem strategy, where launches of "first-party" hardware or bundles are often judged by their own profitability, and for competition policy, where the same move lowers the rival complementor's price and changes how the gains of the system are divided. Proposition 1, which the goal relies on, also shows that the asymmetric outcome, where one complementor integrates and the other does not, occurs for an intermediate band of entry costs, so the asymmetry arises endogenously between identical firms.
The paper proves these statements with computer-algebra-style calculations on closed forms. As far as is known, none of it is formalized. A complete development checks every equilibrium derivation, including uniqueness of the equilibria under joint deviations, and the inequalities that the paper's appendix treats briefly. The positivity of (Proposition 1 (i)) is argued in the appendix through a monotonicity claim that does not hold as written, and the two displayed formulas listed under Formalization scope contain misprints. The formal record settles these points.
The equilibrium computations are linear algebra, but each is stated as an equivalence: a profile is an equilibrium if and only if it equals the closed form. The "only if" direction needs strict concavity of each firm's two-price profit in both prices jointly. The comparison versus needs the admissible range: the factor is positive only because , and this has to be extracted from a square-root bound. The loss-making-entry claim needs more than 's entry benefit being nonnegative. must also stay out, so has to lie in and above 's integrated-system profit at the same time. That is why the goal depends on Proposition 1 (i), whose central inequality is a polynomial inequality in three variables over a region bounded by a square root. Plugging in boundary values of , as the appendix does, does not by itself establish it.
All objects are over in the namespace SystemSqueeze.Accommodation, in one definition file:
Standing UC UI γ bundles , , and Admissible UC UI γ. Positivity of and are added; the paper uses them without stating them.IsNoEntryEq, IsAccEq and IsEscEq are pure Nash equilibria with joint deviations in a firm's two prices.The equilibrium lemmas are reusable for any linear-demand analysis of this model, including Propositions 2 and 4–8 of the paper, which are not part of this mission. Contributions of proofs for any milestone are welcome, as are alternative proofs of .
Firms reposition their products as consumer tastes drift: car makers redesign models, retailers change assortments, media outlets shift their editorial line. Each move costs money, and competitors respond to it. Ning and Villas-Boas (2020) study when two competing firms should incur a fixed cost to move toward consumers whose preferred position follows a random path. The answer is a pair of repositioning thresholds. The paper characterizes them through a system of two transcendental equations and, for small repositioning costs, derives explicit asymptotic expansions. Those expansions give the paper's comparative statics in volatility, attribute importance and patience.
This mission formalizes that small-cost analysis: Proposition 2 of the paper, together with the chain of identities and limits in its appendix that leads to it.
Consumers have preferences . All consumers share the same position on the repositionable attribute, and they are uniformly spread on the fixed attribute . The position follows a driftless Brownian motion with variance , reflected at and . Two firms sit at the ends of in , and at opposite ends in . A consumer buying from a firm at distance gets utility , so measures how much the repositionable attribute matters. A firm may jump to the other end of the -line at a cost . Firms discount at rate . All these parameters are standing assumptions.
Under price competition, a firm earns the flow profit when both firms are on the same side. When they are on different sides and the firm is at distance from the consumers, it earns
Write . In the symmetric equilibrium, a firm on the far side repositions when its distance reaches a threshold . Firms on the same side reposition at a positive hazard rate on . Value matching and smooth pasting of the value functions
give five conditions (5)–(9). Eliminating leaves the threshold system (14)–(15) in alone. With :
A threshold pair at cost is a solution of (14)–(15) with and . A solution branch is a pair of functions that is a threshold pair for every sufficiently small . The appendix uses the prices and , and their sum .
For every solution branch, as :
The goal fixes no constant. It asserts only the directions and the vanishing relative effect of , so it survives any refinement of the expansions.
In attack order:
The result. Proposition 2 is the paper's main qualitative statement about cheap repositioning. More volatile tastes make firms wait longer before moving: with high the consumers are likely to drift back. A more important repositioning attribute makes them move sooner. In both cases the band , in which same-side firms randomize, widens. Patience, by contrast, drops out to first order. The law also quantifies how strongly repositioning reacts to its cost: a small cost has a large effect on behaviour.
Formalizing it. The result is proved in the paper by an asymptotic computation in its appendix. As far as a search of the Prove2Me catalog shows, none of it is formalized. The mission produces a checked version of every step, in the paper's own notation. Two places need more than transcription. The printed (16)–(17) have right sides that still depend on , so they are restated as two-term expansions. The paper also never states that solutions of (14)–(15) exist for small ; the existence milestone supplies that.
The thresholds are defined only implicitly, as solutions of a transcendental system, and the goal is about every solution branch. Nothing is known in advance about such a branch: not continuity, not uniqueness, not a closed form. The natural first idea, to substitute the expansions (16)–(18) and compare coefficients, assumes what has to be shown. The expansions must be derived from (14)–(15) for an arbitrary branch.
The derivation is delicate because the leading behaviour cancels. The left side of (xii) vanishes to third order at , so the rate of is the cube root of a ratio of small quantities. The gap is of order , one order below the thresholds' own displacement. Clause 4 of the goal needs the leading coefficient to be independent of , and clauses 2–3 need strict inequalities between leading coefficients.
All quantities are real. The parameters are a structure with fields r, σ2 (the variance itself) and δ, and Standing requires all three to be positive. Primes are deriv evaluated at the point, and is the derivative of pid, not a hand-coded formula. Equations (14)–(15) keep the paper's ratio form: since , a vanishing denominator makes them false, not vacuously true. The milestone deriving (14)–(15) from (5)–(9) states the displayed ratios with both denominators nonzero.
Commitments beyond the printed text:
Two readings are ruled out as trivializing. Defining the thresholds by formulas, or assuming (16)–(18) for the branch, would make the goal a computation; the goal instead quantifies over every branch. Stating clause 4 as would be contentless, because both thresholds tend to .
The development needs real asymptotics: Taylor control of near , cube roots as real powers, and filters on . It needs no stochastic calculus, since the value functions enter only through their closed forms. The limit (xviii) and the asymptotic analysis of an implicitly defined branch are reusable beyond this paper. Contributions to any milestone are welcome. Not formalized: the hazard rate (13), the verification that the thresholds form a Markov perfect equilibrium, Propositions 3–6, the asymmetric equilibrium and the limit .
Energy-efficiency and emission standards for products such as vehicles and appliances are set by regulators whose jurisdictions overlap a single manufacturer's markets. The best-known case is United States fuel-economy regulation. California has long been allowed to set stricter vehicle standards than the federal government, and the 2019 dispute between California and the federal administration over a single "50-state" standard put the question of split versus unified markets on the policy agenda. A manufacturer facing two different standards can sell two product versions (a split market), sell one version that meets the stricter standard everywhere (a unified market), or withdraw from the stricter market.
Han, Hu and Dawande (Curbing Emissions: Environmental Regulations and Product Offerings Across Markets, Manufacturing & Service Operations Management, 2022) model this as a game between an environmentally concerned regulator, an environmentally agnostic regulator, and a monopolist. They ask when the market splits, and whether negotiation between the regulators can unify a split market and lower total emissions. This mission formalizes their answer for one negotiation format, the exact global standard (§4.1.1), together with the base-model results it rests on. Citations refer to the authors' accepted manuscript of 28 July 2022, including its Online Appendices.
A monopolist sells in two markets of sizes . Regulator sets a minimum efficiency standard for products sold in . Consumers' valuations are uniform on . A consumer with valuation who buys a product of efficiency at price receives , where is the efficiency bonus, and buys when this is positive. Producing efficiency costs per unit plus a fixed setup cost per product.
Regulator maximizes consumer utility in minus . Here is a benchmark efficiency, is the perceived per-unit environmental impact, and the sum runs over both markets. Regulator maximizes consumer utility in only and therefore sets . The total emissions are .
Given , the firm chooses among three strategies: (differentiated products at and ), (one unified product at in both markets), and (one product at , sold in only). Each product is priced at . A base-model outcome is a standard together with a profit-maximizing strategy of the firm, such that cannot do better with another standard paired with any profit-maximizing response.
In the exact-standard negotiation, and agree on one standard for both markets and a transfer from to . Their total utility is (eq. (4)). The disagreement point is the pair of utilities at the split-market base outcome, and the negotiated pair maximizes the Nash product over the feasible pairs that split the gain equally.
Assume condition (1) of Lemma A.1, where is the larger root of an auxiliary quadratic:
Then a split-market base outcome exists. For every such outcome, the negotiation has a Nash bargaining solution, and every solution has standard
The regulators' total utility at strictly exceeds , and total emissions at are strictly lower than at the split-market outcome.
The result. Proposition 3 shows that, whenever the base model predicts a split market under the paper's sufficient condition, two regulators who negotiate an exact global standard with side payments always reach agreement. The agreed standard unifies the market and lowers total emissions. The negotiated standard coincides with the standard a neutral arbitrator would choose. This makes the exact global standard the benchmark against which the paper compares its other negotiation formats (a baseline global standard, and vertical negotiation with the firm). It also qualifies the policy debate: unification through an exact standard requires the stricter regulator to give up its power to exceed the common standard.
Formalizing it. The proofs in Online Appendix C are short computations in which several steps are "straightforward" or "easy to show". In particular, the existence and use of , the comparison between strategies at the regime boundaries, and the truncated branch of Proposition 2 are argued only briefly. A machine-checked development fixes the equilibrium notion, including how ties between strategies are treated, and verifies every inequality. To our knowledge none of these results has been formalized before.
The algebra of each step is elementary, but the base equilibrium is a bilevel object. optimizes over against a firm response that switches between three regimes at and , and 's utility is a different concave quadratic in each regime. Showing that the split outcome sits at requires comparing the maximum over the regime with the maxima over the and regimes. Only the third term of condition (1), through the implicitly defined , controls the comparison. Simply substituting the closed forms of Lemma A.1 into the negotiation does not prove the goal: the goal quantifies over every split-market base outcome, so the characterization of the base equilibrium must actually be established. The emissions comparison also needs a strict inequality. At the emissions in are equal and only changes, and the case must be excluded using condition (1).
All quantities are real numbers in one parameter record , and every statement assumes the standing assumptions of §3: , , , and . The formalization departs from or adds to the page in these places:
A trivializing formalization is ruled out: the goal does not take the disagreement point from Lemma A.1's closed form or compare two formulas. It reads the disagreement point off an arbitrary split-market base outcome, asserts that one exists, and characterizes the negotiated standard through the Nash-product maximization. A sorry-free verification file checks that the goal's hypotheses hold together at a concrete parameter point (, , , , , , ).
The development needs only real algebra: quadratics, square roots and case analysis over three strategies. The lemmas on piecewise-quadratic best responses, and on the reduction of a transferable-utility Nash bargaining problem to total-utility maximization, may be reused for other regulator–firm models. Proofs of any milestone are welcome. Propositions 4 and 5 (baseline global standard, vertical negotiation) and the unified half of Proposition 2 are outside this mission.