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?
The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a channel can be simulated by teleporting its input through a fixed resource state , then any adaptive protocol using times can be rewritten as LOCC acting on , and every LOCC monotone of bounds the protocol's output.
For the pure-loss channel the natural resource is the Choi state of an ideal Einstein–Podolsky–Rosen state, which is not a normalizable state: it is the limit of two-mode squeezed states and has infinite energy. R. Namiki (arXiv:1603.05292, 2016) observed that this limit can be avoided for lossy channels. Finite-squeezing teleportation, in the Braunstein–Kimble scheme (Braunstein and Kimble, PRL 80, 869, 1998), does not teleport perfectly, but its imperfection is itself a pure loss. Composing it with a second pure-loss channel therefore reproduces the target channel exactly, with a finite-energy resource.
A single bosonic mode is described on the Fock space with number basis . Every operator is handled through its number-basis kernel ; an operator on two modes has kernel , the first index labelling the first mode.
Alice holds a two-mode state ( the signal, a reference) and Alice and Bob share a resource . The unnormalized branch for outcome is the kernel on
For put and , the effective Choi state. For every two-mode density ,
entry by entry, with every series and integral convergent, and . The parameters and the protocol are independent of .
The result. The Theorem shows that one use of a pure-loss channel, on any input including half of an entangled state, is reproduced exactly by LOCC on the finite-energy state . In the paper's §II.C this is the step that would let entanglement-measure bounds for adaptive channel uses be evaluated on a genuine density operator, without the limit that the ideal-EPR argument needs. The relation (24) also makes precise in which sense the realistic teleportation family is not teleportation-stretching in the finite-dimensional sense, yet simulates the channel after an outcome-dependent displacement.
Formalizing it. The result is proved in the paper by a short computation through the Glauber–Sudarshan representation, which is heuristic for nonclassical inputs. No machine-checked version exists. A formal proof requires an argument valid for every density operator, together with all convergence statements. The formalization also records a sign slip: with the paper's own definitions (4), (16), (A4) and , the step in (20) should read . Consequently (20) and (23) hold with in place of , and the correction in (24) is rather than ; a numerical evaluation of the printed (24) for the input gives an error of in the output matrix, against (grid-limited) for the corrected one. The Theorem itself, existential in the protocol, is unaffected.
The obvious route is the paper's: write , compute everything for coherent states, and integrate. For nonclassical states is not a function, or even a measure, so this route is not a proof; passing from coherent inputs to all densities needs a density or continuity argument in trace norm, with interchange of the outcome integral and the infinite Fock series. The Bell projection itself is a contraction against improper vectors, here encoded as an absolutely convergent four-fold series whose convergence for arbitrary trace-class inputs is part of the work. Finally, the composition and the covariance (18) are standard on covariance matrices but must be established on number-basis kernels, where they are identities between infinite series with binomial weights.
QAlgorithms_Papers_Independent_Dependency50_P39; the loss channel is the vacuum-loss kernel of QAlgorithms_Papers_Independent_Frontier30_P21; coherent states use its coherentDensity.Frontier30.P21.coherentOutput and is not posed again.Quantum technologies usually prepare a desired state by isolating a system and driving it with carefully timed unitary operations; coupling to an environment is treated as noise. Dissipative state preparation reverses this view: one engineers the system–environment coupling so that the open-system dynamics itself drives every initial state into a prescribed target state. Because the target is a fixed point that attracts all initial conditions, the preparation needs no initialization and is self-correcting against perturbations that leave the dynamics unchanged.
In 2008 three closely related papers made this programme concrete. Diehl, Micheli, Kantian, Kraus, Büchler and Zoller showed how cold atoms can be driven into condensed many-body states by engineered dissipation (arXiv:0803.1482); Verstraete, Wolf and Cirac showed that dissipative dynamics can perform universal quantum computation and prepare matrix product and PEPS states (arXiv:0803.1447); and Kraus, Büchler, Diehl, Kantian, Micheli and Zoller, Preparation of entangled states by quantum Markov processes (arXiv:0803.1463), gave the general uniqueness criteria and the explicit construction this mission formalizes. The last paper's central claim is that every pure state of qubits is the unique stationary state of an explicitly given Markovian process, and that this process relaxes on a time scale independent of .
A quantum Markov process on a -dimensional Hilbert space is a master equation for a density matrix (a positive semidefinite complex matrix of trace one). In the paper's Eq. (2) the generator, or Liouvillian, is
where is a Hermitian matrix (the Hamiltonian), the are arbitrary complex matrices (the jump operators) and are rates. The solution is . The paper writes , and .
A stationary state is a density matrix with . A vector annihilated by every and an eigenvector of is a dark vector; the set of dark vectors, when it is a subspace (all dark vectors share one eigenvalue of ), yields the dark states, the density matrices with range inside .
For qubits, lowers qubit from to . Given any unitary , the target is , which ranges over all pure states, and the construction of §IV uses the jump operators with rates . The relaxation time is the inverse of the least value of over the nonzero eigenvalues of .
For , any unitary and rates :
Clause (a) allows every Hamiltonian that has the target as an eigenvector; (b) and (c) concern the purely dissipative process , the one the paper solves explicitly.
The result. The goal shows that dissipative preparation is universal for pure states: no pure state, however entangled, is out of reach, and the required jump operators are written down explicitly. Clause (c) states that the time to reach the target is governed by the weakest single coupling and does not grow with the number of qubits. Theorems 1 and 2 are general tools independent of the construction: Theorem 1 characterizes every pure stationary state of every Lindblad generator, and Theorem 2 is a checkable sufficient condition for the absence of other stationary states. The later sections of the paper (stabilizer and graph states, PEPS and the AKLT state, a driven condensate, the -condensate) apply these tools to physically local processes.
Formalizing it. The results are classical and proved in the paper, partly in sketched form ("straightforward", "the same arguments as above"). No machine-checked proof of any of them is known. The formalization supplies complete arguments for the sketched steps, fixes the guards the printed statements omit (listed below), and produces a reusable layer of statements about the spectrum and stationary states of Lindblad generators on finite-dimensional spaces.
The first idea for uniqueness is to show that the target is the only pure stationary state, using Theorem 1. That is not enough: a Lindblad generator can have mixed stationary states even when its pure stationary state is unique (with Hermitian jump operators the maximally mixed state is always stationary, Eq. (4)). Excluding mixed stationary states is the content of Theorem 2, whose proof requires a positivity argument for and a decomposition of along .
For convergence, uniqueness of the stationary state does not suffice either: a purely imaginary eigenvalue would make oscillate forever. Clauses (b) and (c) need the full spectrum of the -dimensional Liouvillian, obtained by reducing to and decoupling into single-qubit problems; in Lean this means relating the eigenvalues of a generator on matrices to those of tensor factors.
The generator, the semigroup (matrix exponential of the Liouvillian as a linear map), and the predicates stationary (density matrix with ), attractive and lazy (nonzero subspace invariant under all jump operators) are reused from the published definition QAlgorithms_Papers_Independent_Dependency50_P16. That layer normalizes the dissipator as ; the paper's rates enter through jump operators , which reproduces Eq. (2) exactly. Operators are complex matrices, states are vectors in , and qubits are indexed by with qubit 1 the most significant bit; is the basis vector of index . Density matrices are positive semidefinite of trace one, and is formed without normalization, so unit norm is assumed where the paper says "state". Convergence is entrywise.
Conventions added to the paper and disclosed in each statement:
A trivializing formalization is ruled out: the target is not fixed to , the jump operators are the conjugated and not , clause (a) quantifies over all Hamiltonians with the target as eigenvector rather than only , and the relaxation time refers to the actual nonzero spectrum of the generator.
A complete development needs: properties of the Lindblad generator under unitary conjugation; positivity arguments for completely positive maps on matrices; the tensor-product structure of matrices over qubit wires; and the spectrum and diagonalizability of a sum of commuting single-site generators. The spectral and stationary-state lemmas are reusable for any finite-dimensional open-system mission. Contributions to any milestone, and alternative proofs of Theorem 2 or of the spectrum, are welcome.
In a system driven away from equilibrium, a force changes a reference state and a dynamics, while a corresponding flux records the transported quantity. Statistical mechanics asks how the mean flux changes under a small force. A second question is whether the matrix of these changes is symmetric when the underlying dynamics admit time reversal. Jakšić, Pillet and Rey-Bellet derive both answers at a fixed, finite observation time from a generalized Evans–Searles fluctuation symmetry for classical dynamical systems in their 2010 preprint, §4. This finite-time statement does not require a large-time limit, a stationary nonequilibrium state, or an asymptotic fluctuation theorem.
The paper first develops the entropy cocycle and its time-reversal properties for a single system. Its Proposition 3.3 gives a scalar finite-time Evans–Searles identity. Section 4 lets the dynamics and reference state depend on a vector of forces and introduces a vector of fluxes. Proposition 4.6, the target here, is the section’s stated finite-time Green–Kubo and Onsager result Jakšić, Pillet and Rey-Bellet, pp. 18–21.
Fix a positive integer and a measurable configuration space . Each force vector determines a continuous-time measurable flow , a probability state , and an entropy-production observable . The evolved states of each system are equivalent to , and the regularity assumption (E1) makes the derivative of the evolved-state density in . The family also has a measurable flux vector satisfying the flux relation almost everywhere. These are the family and flux conventions of §4.1 Jakšić, Pillet and Rey-Bellet, pp. 17–18.
At equilibrium, . Assumption (T1) says only that is invariant under ; no stationarity is imposed on for nonzero . Assumption (T2) gives each -system a possibly different time reversal preserving , reversing the flow, and sending to almost everywhere. For , the -system time average is
and its force derivative at equilibrium is . The equilibrium correlation with indices is . Thus the time-shifted factor carries index .
The generalized Evans–Searles functional is the log-Laplace transform of the actual integrated flux,
with extended real values when the exponential moment diverges. Proposition 4.3 states under (T1)–(T2) Jakšić, Pillet and Rey-Bellet, p. 19.
Proposition 4.2 relates the law of the averaged flux to its reflection for nonzero : . Proposition 4.3 states the equivalent symmetry of . Lemma 4.4 is a calculus statement about a function with that symmetry. These are the three new numbered milestones; the earlier entropy-cocycle results, Propositions 3.1, 3.2 and 3.8, are reused as published references Jakšić, Pillet and Rey-Bellet, pp. 8–12, 19.
The goal is all of Proposition 4.6, at each fixed :
The first clause is the paper’s assumption (T3) as a conclusion. The second is the finite-time Green–Kubo formula and the third the finite-time Onsager reciprocity relation Jakšić, Pillet and Rey-Bellet, pp. 20–21.
The formula determines the first-order response matrix from correlations measured entirely in the equilibrium system. Its triangular weight records a finite observation window. Reciprocity then says that cross-responses agree after exchanging the flux and force coordinates. Both statements are exact at fixed time, so they can be used before an asymptotic transport coefficient is known to exist Jakšić, Pillet and Rey-Bellet, Proposition 4.6 and Remarks 1–2, pp. 20–21.
The paper proves these claims. The formalization task is to express and eventually verify the known result, including the dependent family of states and flows, the extended log moment, and all three clauses of the proposition. The published §3 definitions and cocycle statements provide a reusable base. A checked §4 development would also expose general measure and calculus lemmas for finite-time fluctuation relations. At drafting, these new statements compile as open Lean theorems; compilation does not supply their proofs.
The symmetry is an equality of potentially infinite log moments, while the response matrix uses real derivatives near the origin. Local finiteness must justify passage between those two regimes. The paper’s convention includes five families of continuous partial derivatives, including both orders of mixed differentiation, but does not demand two derivatives. Treating it as ordinary would change the theorem.
There is also a measure-theoretic gap between a time integral of fluxes inside an expectation and an integral of expectations over time. A formal statement must control that interchange and the two-time correlation integral. Stationarity is available only at equilibrium, although both the state and flow vary with in the response derivative. The one-line formula for on p. 20 leaves its state implicit; the first display of the proof on p. 21 and the entropy balance used in (4.30) identify it as the -system state for Jakšić, Pillet and Rey-Bellet, pp. 20–21.
The Lean family uses as Fin N → ℝ with , a measurable type , and one published RegularSystem M for each . That type supplies (F1), (F2), (C), and (E1); the new family supplies the flux relation and almost-everywhere time integrability of each coordinate on finite intervals, so the paper's integrated flux is defined. Observable identities in the flux relation and time reversal are -almost everywhere. The law is the pushforward of under the integrated flux divided by . The log-Laplace transform uses a nonnegative integral and EReal, retaining ; a real conversion occurs only on a neighborhood where finiteness is stated.
The goal requires , since its triangular kernel and time average refer to . Proposition 4.2 requires because otherwise contains a division by zero; Proposition 4.3 includes . To make the correlation and Fubini steps meaningful, equilibrium flux coordinates are assumed in and the -system flux is locally integrable on near . These are labeled analytic hypotheses, not new physical symmetry assumptions. Coordinate partials are derivatives along coordinate lines, with existence as well as continuity asserted for the five families on an open neighborhood.
The target uses the actual log-Laplace transform and the force derivative of the actual time average. It imposes stationarity only at , uses equilibrium correlations, and keeps precisely regularity. The family interface and the calculus and integration lemmas needed to prove the milestones are reusable; contributions that close any of the numbered milestones or the analytic interchange obligations fit this scope.
Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of gauge fields), and in quantum information (averages of quantum channels over random unitaries, twirling, unitary designs). Weingarten first computed asymptotics of such integrals for in 1978 (Weingarten, J. Math. Phys. 19 (1978)); Collins (IMRN 2003) and Collins–Śniady (CMP 2006) gave exact formulas for the unitary, orthogonal and symplectic groups in terms of what is now called the Weingarten function.
The survey of Collins, Matsumoto and Novak, The Weingarten Calculus (arXiv:2109.14890), isolates the single statement underneath all these formulas, valid for every compact group and every finite-dimensional unitary representation. This mission formalizes that statement, Theorem 2.1 of the survey, together with the steps of its proof as written in Section 2.
Let be a compact Hausdorff topological group and its Haar probability measure, the unique Borel probability measure on invariant under left translation. Let with its standard orthonormal basis , and let be a continuous group homomorphism into the unitary matrices. Its matrix elements are , the entry of .
Fix . A multi-index is a function ; the set of them is . The Weingarten integrals of degree are
The tensor power has the orthonormal basis , and the tensor-power matrix has entries . The invariant tensors are
and the Haar average is the matrix . Given vectors , let be the matrix whose columns are their coordinates, its conjugate transpose, their Gram matrix, and, when it is invertible, the Weingarten matrix of .
If is a basis of , then for all
The identity is exact and holds for every compact group, every continuous unitary representation, every degree and every choice of basis; nothing is fixed beyond the data.
Theorem 2.1 reduces a family of analytic problems — Haar integrals of polynomials in matrix entries — to two algebraic ones: find a basis of the invariant tensors of in (classical invariant theory), and invert its Gram matrix. For the invariants come from Schur–Weyl duality and the Weingarten matrix becomes the Weingarten function on permutations; for and the invariants are indexed by pair partitions; for the symmetric group acting by permutation matrices the invariants are indicators of set partitions. Each of these case-specific formulas, surveyed in Sections 3–5 of the paper, is an instance of Theorem 2.1, so a formal proof of the theorem is the common entry point for formalizing any of them.
The theorem is classical and its proof is elementary once stated; it is not open. No machine-checked proof is known to exist in Mathlib or on this platform: Mathlib has Haar measure, unitary groups and Gram matrices (including the equivalence of linear independence with invertibility of the Gram matrix), but not the averaging projection of a representation in matrix form nor the formula for orthogonal projections. The mission produces both as reusable lemmas and the Fundamental Theorem itself.
The argument is short on paper; the formal work sits in three places. First, selfadjointness of needs , i.e. unimodularity of a compact group, which Mathlib does not provide as an instance for non-commutative groups. Second, identifying the image of with the invariant tensors needs both directions: invariant vectors are fixed by , and every vector is invariant, which uses left invariance of inside a matrix-valued Bochner integral. Third, the projection formula needs invertibility of from linear independence and an argument that a selfadjoint idempotent is determined by its image. Commuting the integral with matrix entries and products is routine but must be done with care for the matrix norm chosen.
G →* Matrix.unitaryGroup (Fin N) ℂ, assumed continuous. Indices are 0-based: is Fin N, multi-indices are Fin d → Fin N, tensors are (Fin d → Fin N) → ℂ.[IsTopologicalGroup G] [CompactSpace G] [T2Space G] [BorelSpace G], and is a Haar measure that is a probability measure. Right invariance is not assumed; it is a consequence that solvers must prove.LinearIndependent ℂ a and span (range a) = invariants U d, with the invariant subspace defined from the representation. Without independence Mathlib's matrix inverse returns on a singular Gram matrix, and the statement would be false; it is therefore not a trivializing gap but a necessary hypothesis.Needed infrastructure: matrix-valued Bochner integrals commuting with entries and with matrix multiplication; unimodularity of compact groups; the orthogonal-projection formula. All three are reusable well beyond this mission, and contributions of these general lemmas are welcome.
Classical Hamiltonian mechanics describes an observable by a function on a phase space. Its Poisson bracket gives observables a Lie algebra: the bracket is antisymmetric and satisfies the Jacobi identity. In multisymplectic geometry, a higher-degree differential form replaces the symplectic two-form, and the appropriate observables may themselves be differential forms. This occurs in the geometric description of classical field theories, where quantities associated with spatially extended objects are naturally expressed through forms rather than functions. Baez, Hoffnung and Rogers use this setting to examine the classical bosonic string in their paper, §§1 and 5.
The same paper shows why the usual Lie algebra of observables is too narrow for a 2-plectic space. One bracket of Hamiltonian one-forms satisfies the Jacobi identity but is antisymmetric only up to an exact form; another is antisymmetric but has a Jacobi identity only up to an exact form. Theorem 4.3 packages the first bracket and its exact correction into a hemistrict Lie 2-algebra. The result is known mathematically; the mission is to give its construction a machine-checked statement and proof in Lean for a finite-dimensional vector-space model Baez–Hoffnung–Rogers, §§3–4.
Let be a finite-dimensional real normed vector space. A 2-plectic form on is a smooth three-form with such that implies at each point. The interior product places in the first argument of the form. This is the case of Definition 2.1 in the preprint, p. 6.
A smooth one-form is Hamiltonian when a smooth vector field satisfies
Nondegeneracy makes unique. Write for the vector space of these forms. The hemi-bracket is , where is the Lie derivative. On functions its left and right actions are and . The alternator is the function . These formulas are Definitions 3.1 and 3.3 and the data preceding Theorem 4.3 on pp. 11 and 16–17.
A Lie 2-algebra here has a two-term chain complex , a bracket on its available degrees, an alternator witnessing antisymmetry up to chain homotopy, and a Jacobiator witnessing the Jacobi relation up to chain homotopy. Four further coherence diagrams constrain these homotopies. “Hemistrict” means that the Jacobiator is the identity homotopy, represented by the zero degree-one map Definitions 4.1–4.2, pp. 15–16.
For every 2-plectic , Theorem 4.3 constructs a hemistrict Lie 2-algebra with all components fixed:
The existential goal fixes the carriers and every operation; the Lie 2-algebra structure then requires the chain-map identities, the homotopy identities, and all four coherence equations. The milestones isolate the source statements that supply the main geometric identities: uniqueness of , Hamiltonian exact forms, Proposition 3.6, the bracket’s chain-map behavior, a mixed Jacobi identity, and the third coherence diagram Theorem 4.3 and its proof, pp. 17–18.
The theorem identifies the algebraic structure carried by 2-plectic observables. In particular, it retains the exact-form discrepancy in antisymmetry as an explicit operation instead of losing it by quotienting forms. The paper compares this hemistrict construction with a semistrict construction and then studies their relation; the present result is the first of those two constructions Theorems 4.3–4.6, pp. 17–19.
A formal proof would connect Mathlib’s exterior derivative on alternating forms to a reusable calculus of interior products, Lie derivatives, Hamiltonian vector fields, and higher algebraic coherence. The preprint already proves the theorem. The local proposal supplies statements for its finite-dimensional normed-space case; a proof in Lean and an extension from vector spaces to general smooth manifolds are further work. The current mission does not assert the separate semistrict theorem or the string application.
The obvious attempt to make Hamiltonian one-forms into a conventional Lie algebra fails: for the hemi-bracket, can be a nonzero exact form. The correction must also agree with the bracket on functions and with the Jacobi relation across degrees. A degree-zero calculation alone therefore does not establish a Lie 2-algebra. Its chain-map conditions and four coherence diagrams impose further identities involving the exterior derivative, Lie derivatives and the Hamiltonian vector fields Proposition 3.6 and Definition 4.1, pp. 12, 15–16.
Lean uses with NormedAddCommGroup, NormedSpace ℝ E and FiniteDimensional ℝ E, in place of the paper’s arbitrary smooth manifold . Forms, functions and vector fields are defined on all of , and smoothness means ContDiff ℝ smooth with smooth the degree. This is the disclosed scope cut. The Lean name for the paper’s is Ω; this avoids a notation conflict from the imported definition module.
Mathlib represents a -form as a function into a continuous alternating -linear map. Its extDeriv supplies the exterior derivative, while the published ContWeatherall.grad supplies for functions. Interior product inserts in the first slot. The Lie derivative of a one-form uses its derivative and the derivative of the vector field, so Cartan’s identity is a mathematical assertion rather than the definition of the Lie derivative. The bracket of vector fields uses . The two-term chain complex uses the paper’s ordinary graded tensor-product differential and signed switch. Every formal statement about hamVF restricts its form to Hamiltonian inputs, where nondegeneracy gives a unique vector field; the default value on other inputs has no role in the theorem.
The goal requires all operations to have the paper’s values and requires every Lie 2-algebra axiom. An arbitrary pre-existing Lie 2-algebra or a structure with unconstrained operations would not establish this result. Reusable contributions include differential-form identities and the algebraic two-term interface. The separate semi-bracket construction and general-manifold extension remain outside this proposal.
A quantum channel is a completely positive, trace-preserving linear map between matrix algebras; it models the most general physical transformation of a quantum system. When a group acts on the input and output systems, a channel is -covariant if it commutes with the group action. Covariant channels appear whenever a physical process respects a symmetry: rotation-invariant noise on spin systems, optimal cloning and estimation of spin states, and quantum reference frames for orientation. Because the covariant channels between two fixed representations form a convex set, the first structural question is what its extreme points are; they are the channels from which every covariant channel is obtained by mixing.
For acting irreducibly on input and output, the tensor product of the output representation with the dual of the input one is multiplicity free, so the commutant that controls covariant maps is abelian (Vollbrecht and Werner, 2001, arXiv:quant-ph/0010095). M. Al Nuwairan (arXiv:1306.5321, 2013) makes this concrete. She constructs explicit channels , called EPOSIC channels, from Clebsch–Gordan isometries realized on polynomials. She computes their Choi matrices and shows that they are exactly the extreme points of the convex set of SU(2)-irreducibly covariant channels.
For , let be the space of homogeneous polynomials of degree in two variables . The group
acts on by the representation ,
With the inner product , the canonical basis , , is orthonormal and is unitary. The are the irreducible representations of .
The tensor product is realized as the polynomials in and of bi-degree . On these polynomials act the operators
Real coefficients are defined by the recursion and, for , if , if , and if . For and , the map
is an explicit Clebsch–Gordan isometry. The EPOSIC channel is
For , is the set of the channels with and . The set consists of the quantum channels with for all and all .
The statement has no hypotheses and covers the degenerate cases: for the set is a single channel.
In the order of the paper's argument:
The result shows that the covariant channels between two irreducible SU(2) representations form a simplex. Its vertices are given by closed formulas, so optimization problems over SU(2)-covariant channels reduce to finite-dimensional linear programs over the vertex weights: fidelities, output entropies, capacities restricted to covariant encodings. The explicit Choi matrices make the vertices computable in any basis. The same channels are used later in the paper to compute complementary channels and to exhibit a positive map that is not completely positive.
On the formal side, the mission produces the irreducible representations of on homogeneous polynomials, the polarization operators, and explicit Clebsch–Gordan isometries with their equivariance and isometry proofs. It also produces a Choi-matrix criterion for covariance and the extreme-point characterization. Theorem 2.7, Proposition 1.15 and Proposition 3.9 are cited in the paper from Procesi, from [4] and from Vollbrecht–Werner, and are proved neither there nor, as far as is known, in any proof assistant. Nothing in this mission is machine-checked yet.
That is a covariant channel follows from equivariance of . The real content lies elsewhere.
First, is an isometry only because of the specific constants . The paper derives this from the polynomial identity of Theorem 2.7 and Schur's lemma, and neither is available off the shelf for these polynomial models.
Second, the extreme-point statement needs the full commutant of : the projections onto the irreducible summands must span it. Exhibiting the projections is not enough; one must show there is nothing else, which is multiplicity-freeness of the tensor product. This requires the irreducibility of each and the Clebsch–Gordan dimension count.
Third, matching each EPOSIC channel with a single projection (Proposition 3.13) requires a rank argument. The obvious approach, expanding the Choi matrix in coordinates, gives sums of products of signed binomial coefficients whose non-vanishing is the content of Lemma 3.12.
Every space is represented by coordinates in its canonical orthonormal basis, indexed by Fin (k+1) with 0-based indices. So is the algebra of complex matrices, and adjoints for the inner product above are conjugate transposes. The representation and the maps are computed from the polynomials themselves in MvPolynomial (Fin 4) ℂ (variables , derivatives pderiv), then read off in the canonical bases. The action is the row-vector action of the paper. is indexed with the factor first. The conjugate space has the same coordinates and carries the entrywise conjugate matrices. The coefficients are defined by the recursion, not by any closed formula. The input degree of is an explicit argument, constrained by in every statement.
Channels are maps on matrices given by a finite normalized Kraus family (the published QAlgorithms.IsChannel). The partial trace is the published WildeQIT.partialTraceRight, over the factor. The Choi matrix is with the output factor first. Convex hulls and extreme points are taken over in the space of maps.
No statement replaces by an abstract irreducible representation. None defines through extreme points, Choi matrices or projections, defines by its coefficient expansion, or assumes Schur's lemma, the commutant description or Theorem 2.7 as a hypothesis. Each of these would make the goal or a milestone true by definition.
A complete development needs:
The SU(2) representation layer and the Choi-matrix covariance criterion are reusable beyond this mission. Proofs of the cited results (Theorem 2.7, Propositions 1.15 and 3.9) are welcome as independent contributions.
Operators on copies of that commute with every , unitary, are exactly the linear combinations of permutation operators , (Schur–Weyl duality). Many protocols in quantum information carry a different symmetry: the first systems transform by and the last by the complex conjugate . It is the symmetry of port-based teleportation (Ishizaka–Hiroshima 2008), whose optimal performance is computed from the representation theory of exactly this commutant (Studziński et al. 2017). The commutant of is the algebra spanned by the partially transposed permutation operators : the permutation operators with the transpose taken on the last system.
Studziński, Horodecki and Mozrzymas give an explicit operator basis of an ideal of adapted to the irreducible representations of . Their main structural result, Theorem 9, states that this basis and the partially transposed permutation operators are linear combinations of each other, with coefficients that are irrep matrix elements.
Let and . For , the permutation operator on is . The partial transposition transposes the last system: . The algebra is the span of all , . is regarded inside as the permutations fixing the systems after .
Fix with , and write . For labels , the maps are
The standing data are a family of real orthogonal, irreducible, pairwise inequivalent matrix representations of , of dimensions , and a Schur basis: an orthonormal basis of , where ranges over the multiplicity of , such that . With on the last two systems, the paper defines
and . In Lean these are IrrepFamily, SchurBasis, psi, vOp, EOp, with ptLast for , fPerm for and algA for .
For all , , :
and for every , with ,
The goal is the whole theorem, both directions and the membership in .
Theorem 9 shows that the span the same space as the operators with . That space is the ideal of on which the partial transposition acts non-trivially. Because the multiply like block matrices (Lemma 8 of the paper), the theorem converts questions about into finite matrix computations indexed by irreps of . The later constructions of the paper rest on this: the Gram matrices , the biorthogonal basis and the explicit irreps of . The same formalism underlies the eigenvalue analysis of port-based teleportation (Mozrzymas–Studziński–Horodecki 2018).
The result has a published proof but no machine-checked one. This mission adds that check, together with a reusable Lean vocabulary: the partial transpose on one site of , the embeddings , and Schur-basis data for permutation operators. It also pins down the conventions that the printed text leaves inconsistent (see Formalization scope).
The algebraic manipulations are short on paper; the work lies in the bookkeeping they hide. Lemma 26 requires checking that fixes both of the last two systems, which uses in an essential way. The partial transposition is not multiplicative, so every step that moves an operator through needs the specific invariance of milestone 1. Eq. (86) is the identification of the Schur-basis matrix units with group-algebra elements; it needs completeness of the basis together with Schur's orthogonality relations for real irreps, and it is false without irreducibility and inequivalence. Mathlib has Schur's lemma but no coordinate form of the orthogonality relations for matrix representations, and nothing on partial transposes of tensor-power permutation operators.
Equiv.Perm (Fin m), Equiv.Perm (Fin (m+1)), Equiv.Perm (Fin (m+2)). Systems are 0-based, so systems are indices , and labels are Fin (m+1). Permutation products compose right to left.QAlgorithms.Schur.tensorPermutation. is on the last system only. groupAlg is the represented ; algM spans the with .IrrepFamily m contains real orthogonal matrix representations of of positive dimension, irreducible over and pairwise inequivalent over (p. 7 and Notation 32 of the paper). SchurBasis F d is an orthonormal, spanning family of vectors on which acts by the . Multiplicities may be zero. The family is not required to list every irrep of . Every satisfies (Definition 24).ptLast and on liftPerm. Both are reusable beyond this paper.Wilson's numerical renormalization group (NRG) computes the low-energy states of quantum impurity models, such as the Kondo and Anderson models, by diagonalizing a semi-infinite chain one site at a time and keeping only the lowest multiplets after each step (Wilson 1975; review: Bulla, Costi, Pruschke 2008). Dynamical quantities (spectral functions, Green's functions) at finite temperature require, in addition, the reduced density matrix of each shorter chain, obtained by tracing the full density matrix over the sites that come later. This is the density matrix NRG (DM-NRG) (Hofstetter 2000), made exact with the complete basis of Anders and Schiller 2005.
Symmetries make NRG practical: when the Hamiltonian is invariant under a group, every iteration splits into blocks labelled by irreducible representations, and each multiplet is stored once instead of once per internal state. For non-Abelian groups (SU(2) spin, SU(2) charge, SU(3) channel symmetry) the saving is large, but only if the reduced density matrix can also be handled multiplet by multiplet. Tóth, Moca, Legeza and Zaránd (arXiv:0802.4332) show that it can, for essentially any symmetry: the reduced density matrix stays scalar under the symmetry after each tracing step, and its reduced matrix elements obey an explicit recursion, their eq. (45), whose only group-theoretic input is the ratio of multiplet dimensions.
A group acts on every multiplet through a labelled unitary irreducible representation: a label has a dimension and unitary matrices of size , and states of a multiplet are indexed by an internal quantum number . Distinct labels carry inequivalent representations.
At iteration the new space is spanned by states , where runs over the kept multiplets of iteration (block states, label ) and over the local multiplets of site (label ). The symmetry acts as
Generalized Clebsch–Gordan coefficients are, for each label in a coupling set of , the entries of a matrix that is an isometry, intertwines with , and such that the sum to the identity. The canonical basis (21) is
one canonical multiplet per kept multiplet, local multiplet and coupled label; one writes .
An operator on the new space is scalar if for all . Its reduced matrix elements in the canonical basis are defined by . is the partial trace over the local states of site .
For every scalar : is scalar under ; has reduced matrix elements in the canonical basis; for kept multiplets with and every such family of reduced elements,
and the entry vanishes when . The paper's truncated reduced density matrix of its eq. (38) is one instance of ; the statement fixes no Hamiltonian, energies or temperature.
In proof order: the covariance of the partial trace (40); the invariance of and of (39), (41)–(42); the Wigner–Eckart form of a scalar operator (43); orthonormality, completeness and the transformation law of the canonical basis (21); the Wigner–Eckart form in the canonical basis (44); and the Clebsch–Gordan sum rule that produces the factor when the local states are traced out.
The recursion (45) computes the reduced density matrix of every iteration from that of the next, one number per pair of multiplets, so that all DM-NRG expectation values and spectral functions can be evaluated in the reduced (multiplet) representation. Its only group-dependent input is the dimension ratio ; the Clebsch–Gordan coefficients themselves drop out. This is what lets a DM-NRG code, such as the flexible code the paper describes, handle any number and type of symmetries without symmetry-specific density-matrix code.
The result is proved in the paper, in a few lines of physics notation that rely on the Wigner–Eckart theorem and on Clebsch–Gordan orthogonality. It has no machine-checked proof. The mission states it as a theorem about invariant matrices, unitary representations and Clebsch–Gordan isometries; its milestones include a Wigner–Eckart theorem for scalar operators on a space of labelled multiplets and a Clebsch–Gordan sum rule, both stated for an arbitrary group and reusable for other symmetry-adapted tensor-network and many-body computations.
The physics proof cites the Wigner–Eckart theorem; formally this is Schur's lemma in two forms: an equivariant map between inequivalent irreducible representations vanishes, and an equivariant endomorphism of an irreducible representation is a scalar. Neither is a hypothesis here, so both must be derived from irreducibility in its invariant-subspace form. The dimension factor is the second form applied to the partial trace of , together with a trace count. A direct computation from the definition of the canonical basis does not give (45): the Clebsch–Gordan coefficients are arbitrary matrices subject only to the three stated conditions, so no closed formula for them is available, and the dimension ratio appears only through the representation-theoretic argument. The bookkeeping is also non-trivial: internal quantum numbers of different multiplets live in different index types even when their labels coincide, and the tilde sum pairs canonical multiplets built with the same local multiplet.
One abstract group with labelled irreducible unitary representations replaces the paper's product of eqs. (17)–(18); the product case is an instance, with the generalized Clebsch–Gordan coefficients of p. 4 as products. Irreducibility is Mathlib's Representation.IsIrreducible, inequivalence the emptiness of Representation.Equiv. The coupling is multiplicity-free, one Clebsch–Gordan matrix per label triple, exactly as (21) is written; with outer multiplicities (as in SU(3)) the printed (45) would need a multiplicity index. Operators on the new space are matrices indexed by (block, local) pairs, block first, and the partial trace over the site is the published WildeQIT.partialTraceRight; Clebsch–Gordan matrices are indexed local first. All index sets are finite. Internal quantum numbers of multiplets with equal labels are compared by their numerical value. No fermionic sign factors appear: the space is the tensor product in the ordering of (21), and (45) carries no sign.
The statement does not assume Schur's lemma, the Clebsch–Gordan sum rule, or a block form of ; the reduced matrix elements in (45) are not free parameters but any family satisfying the Wigner–Eckart identity for , whose existence is part of the goal. The Wilson chain, the complete basis and density matrix (32)–(38), the Green's function (46)–(48), the numerics of §V and the SU(2) appendix are outside the mission.
A complete development needs a usable Schur's lemma for matrix representations (Mathlib provides the module-theoretic version), Kronecker-product and block-diagonal matrix algebra, and partial-trace identities. Lemmas on partial traces of Kronecker products and on Wigner–Eckart for block-diagonal representations are reusable beyond this mission; contributions of either kind are welcome.
Operators made from a complex matrix and its conjugate occur in the non-chiral sector of gauge theories. Their correlation functions involve many possible pairings of matrix entries, and those pairings become difficult to organize as the number of entries grows. Kimura and Ramgoolam use the walled Brauer algebra to label these operators and to describe their two-point functions in a basis adapted to both the tensor symmetries and the mixed fundamental–conjugate representation. The result targeted here is the orthogonality relation for that basis in the reduced two-matrix quantum mechanics Kimura and Ramgoolam, §7.1, p. 29.
The question is concrete: can the algebraic labels of an operator determine whether its state has zero inner product with another state, without expanding every matrix entry? Equation (7.12) says yes for the paper's symmetric branching operators. It is a known result in the cited paper. This mission asks for a machine-checked formalization of its precise tensor-space content, including the complex Gaussian covariance and the permutation sums on which the two-point function depends.
Let , with basis indexed by . The mixed tensor space has a basis labelled by a pair of index tuples: an -tuple for the legs and an -tuple for the conjugate legs. Its operators are finite complex matrices; is their ordinary matrix trace. The group permutes legs within each block. It is represented by matrices , using the already published tensor-permutation definition used here.
A contraction pairs the th leg with the th conjugate leg. The image of the algebra generated by all such contractions and the permutations is denoted . This is the represented Brauer algebra used in the paper's tensor-space traces §3.2, pp. 8–9. The map exchanges the input and output indices of the conjugate block. In coordinates it is the partial transpose on that block; this matches the reflection shown in Figure 6 §3.3, pp. 11–12.
The paper's symmetric branching operators are denoted . Here labels a Brauer representation, an irreducible representation of , and range over its multiplicity . These operators belong to the represented Brauer algebra, are invariant under conjugation by every , and obey the matrix-unit product . The relation comes from their orthonormal-vector definition in (7.3) §7, pp. 27–28.
For two independent complex matrices , put
Each matrix entry has independent real and imaginary parts of variance . This Bargmann–Fock Gaussian realization gives and reproduces the oscillator normalization of (7.8) p. 28.
The goal is the orthogonality identity of (7.12), with the scalar written as a tensor-space trace:
The paper writes the last factor as after invoking mixed-tensor Schur–Weyl duality. The trace version is the equality reached just before that last step in (7.13) p. 29. The mission's milestones cover the unit covariance (7.8), the Wick permutation formula of Figure 3, the trace sum in the second line of (7.13), symmetry preservation (3.37), the collapse in the third line of (7.13), and the trace-pairing identity (3.20).
The formula assigns orthogonal states to different branching labels and multiplicity indices. It also fixes their norms by an explicit finite-dimensional trace. This makes the representation labels useful for organizing non-chiral two-point functions, rather than merely counting or naming operators §7, pp. 27–29. Without the Wick-to-trace identity, the same claim remains an expanding sum of matrix-entry pairings for each degree.
The paper proves the identity diagrammatically; this mission has no machine-checked proof of it yet. A completed formalization would give reusable finite-matrix interfaces for contractions, partial transpose, Gaussian polynomial states, and permutation-indexed Wick sums. The complex covariance and Wick results can be reused independently of the particular Brauer family. The represented algebra and branching interface can support later formalization of the paper's projectors and finite- examples.
The central obstacle is the passage from a Gaussian expectation of products of matrix entries to a sum of traces indexed by . A direct expansion of the state polynomials creates many indices, and each Gaussian pairing must match the direction of the matrix entries and the inverse permutation in the tensor action. The and matrices are independent, so pairings cannot cross their blocks. After that conversion, the partial transpose and permutation symmetry must agree on the same index convention. A transposed covariance or reversed inverse produces a plausible looking expression with the wrong contractions.
The Lean model uses finite matrices throughout, permits , and uses ordinary unnormalized traces. The index type is a pair of functions from and to ; its second component represents the conjugate legs. is the concrete partial transpose, and is the image subalgebra generated inside the matrix algebra. The oscillator vacuum inner product is the Gaussian integral above, with two independent matrices and unit complex variance. It is defined from the measure, not from the Wick permutation formula. The measure's pushforward map is continuous. Matrix-entry polynomials have finite Gaussian moments, so the integral does not rely on Lean's default value for a non-integrable function.
The branching labels are abstract types, but each valid must satisfy Brauer membership, the paper's symmetry and matrix-unit relations, and the adjoint relation derived from (7.3). Indices are natural numbers with explicit range conditions . No completeness axiom, positivity condition, or lower bound on is added. These declarations exclude a trivialized inner product defined as the target permutation sum. The coefficient and the four-dimensional, normal-ordered version (7.16) are outside this mission. Contributions to the Gaussian Wick conversion, the partial-transpose trace identity, and the symmetric branching calculation are all in scope.
Positive linear maps on complex matrix algebras provide tests for quantum entanglement: applying such a map to one part of a bipartite state can expose a state that cannot be written as a mixture of product states. The distinction between ordinary positivity, positivity with an auxiliary matrix system, and complete positivity is therefore substantive. Collins, Osaka, and Sapra study an explicit two-parameter family that makes these distinctions visible through inequalities in the parameters. Their paper identifies the exact region where a map from three-by-three matrices to nine-by-nine matrices is 2-positive but fails to be completely positive. This is the stated main result of their 2018 paper, rather than an open conjecture.
Write for the algebra of complex matrices. A matrix is positive semidefinite, written , when it is Hermitian and has no negative eigenvalues. A complex-linear map is positive when implies . It is -positive when the same condition holds after the identity map on is tensored with . It is completely positive when it is -positive for every . A map is completely copositive when its composition with transpose on the source is completely positive. These are the paper's definitions on page 2.
Let be the unnormalized Bell vector, and let denote its rank-one projector. For real and , the family on page 3 is
The transpose belongs to the first tensor factor. The mission concentrates on . Its Choi matrix is . For this finite-dimensional setting, the Choi criterion relates complete positivity to ; it does not define complete positivity. The paper also identifies an equivariance property: unitary conjugation of the input corresponds to conjugation of the output by a matrix associated with the same unitary.
For , define two boundary curves and a cubic root:
The goal is Theorem 3.9, page 10:
The left endpoint of the first interval is included and the right endpoint is excluded. The milestones record the paper's earlier criteria for positivity, complete positivity, and 2-positivity, together with its general equivariance criterion and the computation for this family. Their inequalities are separate targets; none is built into the definitions of these map properties.
The goal gives an exact, parameter-level example of 2-positivity without complete positivity. It identifies all such members of this family on , including the boundary cases, rather than only exhibiting one map. The surrounding results locate the positive and completely positive regions and give a criterion for testing -positivity of equivariant maps. Together, they provide a compact source of concrete maps with different strengths of positivity, as described in Sections 2 and 3 of the paper.
The mathematical result was proved in 2018. This mission seeks a machine-checked account of the stated criteria, with the family, Choi matrix, Bell projector, and positivity predicates exposed as reusable declarations. A finished proof would connect elementary matrix positivity and tensor products to explicit real-algebraic parameter bounds. It would also make each boundary independently inspectable. The Lean theorem statements here are draft targets with sorry; they are not existing machine-checked proofs of the paper.
Testing only yields ordinary positivity, not 2-positivity. Testing only the Choi matrix addresses complete positivity, which is stronger than the desired property. The 2-positive condition quantifies over every positive semidefinite matrix in ; the paper's criterion reduces that universal condition under equivariance to positivity of a specific block matrix. The block matrix has parameter-dependent eigenvalues, including roots of a cubic. This makes a simple comparison of the two square-root boundary curves insufficient: the smallest cubic root supplies an additional lower bound on . The endpoint also needs attention because the case descriptions for complete positivity meet there.
The Lean model uses Matrix (Fin n) (Fin n) ℂ for and Fin n × Fin n for the output tensor indices, with the first coordinate corresponding to the transposed factor. The paper's one-based is Matrix.single 0 0 1. Positive semidefiniteness is Mathlib's Matrix.PosSemidef. The shared QAlgorithms.idTensorSuperop applies a map blockwise with the auxiliary index first, and the published QAlgorithms.Entanglement.IsCompletelyPositive quantifies over all auxiliary sizes. Size zero is harmless for that quantifier because the corresponding matrix type is empty. The paper's appears on the general-family results; the main goal fixes .
The Bell projector is unnormalized, matching the paper's . The two square roots have positive radicands on the real parameter range. The cubic root is defined as the infimum of its real root set; the odd-degree cubic has a nonempty, finite set of real roots, so this is its least root. The proof development needs reusable facts about unitary conjugation of positive matrices, Kronecker products, Choi matrices, and positivity of the parameterized block matrix. Direct calculations of the boundary inequalities are also welcome. Defining -positivity by the block criterion, complete positivity by Choi positivity, omitting the transpose in , or treating as an arbitrary parameter would make the targets lose their intended content.
An agentic system may make several slow API calls in sequence: the answer to one call determines what to request next. A speculator can guess the current answer while the real call is running and start likely next calls early. When a guess is correct, the system can reuse a pending result; when it is wrong, it discards that result. This can shorten a run if concurrent calls do not interfere and incorrect calls have no lasting side effects. Ye and coauthors introduce this execution scheme for language-model and tool-using agents in Speculative Actions, §2.
The paper's Proposition 1 quantifies the expected latency of one-step speculation with exponential call times. Its proof in Appendix A states a stochastic timing model and computes a finite-horizon runtime ratio and its limit. The first author's existing Prove2Me mission, Speculative Actions: Cost-Latency Analysis for Agentic Speculation, contains proved algebraic identities for expressions named specTime and seqTime. Those expressions encode the values claimed for the expectations. This mission supplies the missing connection between random executions and those expressions, while reusing the published algebra.
There are real API calls, numbered through . The real-call latency of step is with exponential rate . At a speculation window during step , a speculator has latency with exponential rate . It produces candidate next calls. Each candidate independently matches the actual next call with probability , so a hit means that at least one of the candidates matches. The hit probability is
All latencies and branch-correctness indicators are mutually independent. Proposition 1 assumes and Assumption 1 gives ; as a probability, . Assumption 2 permits concurrent API calls and reversible or side-effect-free pre-launching. The theorem also treats state transitions and construction of API parameters as having negligible duration. These conditions and the exponential laws are stated in §2 and Proposition 1.
The sequential runtime is . The speculative runtime follows Appendix A's timing rule. At a window without a hit, the current step costs . At a hit, the block comprising steps and costs , and step opens no window. The last step cannot open a window. This is the model used in the paper's proof of Proposition 1, Appendix A, pp. 14–15. Its precise timing rule matters: reading Algorithm 1's awaits literally gives a different timeline, as does waiting for validation before accepting an early next-step result.
Let be the expected number of hits in potential windows, with a hit consuming the following window. The paper gives , , and
The new milestones identify the expectation of the sequential runtime, the saving from one correct speculation, and the expected hit count. The total-saving identity is
Here is the expectation of the random count defined by the execution model. The previously published expression SpecActions.specTime has this same algebraic form; proving equality with the integral of the random runtime is the new step. The closed form for and the algebraic ratio are linked as published milestones.
For every integer , the goal is the Proposition 1 ratio for the actual expectations:
The same goal states convergence of this random-runtime ratio as to
The horizon condition protects the denominator: at , the sequential runtime is zero. The number of branches may be zero; then and the ratio is one for positive horizons.
The formula describes how breadth , branch accuracy , and the two latency rates affect expected completion time, both for a finite sequence of calls and in a long run. It makes the expected benefit of extra branches a quantity that can be compared with their resource cost. The paper uses the time expression again in its cost–latency discussion, including Theorem 5, p. 20.
The author's existing mission has machine-checked proofs for the recurrence's closed form and for algebraic identities involving specTime and seqTime. It does not prove that those expressions are expectations of a random execution. Completing this mission adds that probabilistic interpretation and a reusable model of independent calls, branch indicators, skipped windows, and runtime. The proposed stochastic theorems remain open; their statements compile, while the published reference results are already proved.
The main issue is the dependence created by skipping a window after a hit. Hit indicators at different windows are independent, but the number of opportunities actually used is determined by earlier outcomes. Treating the hit count as an ordinary binomial count gives the wrong recurrence. Likewise, multiplying a mean saving by the number of potential windows ignores that skipped windows cannot hit. A formal proof must relate the random execution and hit count while preserving the independence between correctness indicators and latencies.
Lean represents all primitive random variables on one probability space. An index type separates speculator latency, real-call latency, and each of the branch indicators at every window. IsSpecModel requires measurable variables, their exponential or real-valued Bernoulli laws, and mutual independence. A hit is an existential statement over the branch indicators. The runtimes and hit count are recursions on a finite horizon, and expectation is the real Bochner integral. The model has an explicit construction on a product probability space, so its hypotheses are satisfiable.
Windows start at index zero: a -step run has potential windows. The theorem keeps the paper's and conditions, and specifies . It adds wherever a runtime ratio is divided by its sequential denominator. Concurrency without interference and negligible non-call work are represented by the timing recurrence. The claim concerns integrals of those random runtimes; defining an “expected runtime” directly by the paper's closed form would omit the target of this mission.
The definition layer and hit-probability, baseline, saving, hit-count, and total-saving milestones are available as separate contributions. Mathlib supplies exponential probability measures, product measures, independence, and integration; the published SpecActions definition and algebraic theorems are referenced. Work on the probabilistic bridges, integrability, and the final composition is within scope.
Firms with several products often put most of their marketing behind one. The resulting product can become the line's flagship even when another product has a higher unit markup. He, Ke, and Zhang give a supply-side model in which this allocation follows from the relation between consumer taste dispersion and the cost of raising a product's perceived utility. Their main proposition says that a concave transformed marketing cost favors concentrating effort on one product. This mission formalizes that proposition and the fixed-effort claims that support it. He, Ke, and Zhang, A Model of Product Line Marketing, 2021 SSRN version, §2 and Online Appendix C.
The question is operational: a firm chooses marketing effort across its product line while sales move through a multinomial logit choice model. Spending on one product changes its share and also takes sales from the firm's other products. Concentrating marketing effort therefore cannot be inferred from looking at a single product's markup in isolation. The paper's marketing effort allocation index provides a way to compare products at a given total effort. He, Ke, and Zhang, §2.1, pp. 12–15.
A firm sells products. Product has base utility and markup . Consumers either buy one product or select an outside option with utility normalized to zero. A Gumbel taste shock has scale . The firm raises product 's utility by , where is the common lower bound, and pays . The paper assumes the cost is strictly increasing, convex, and continuously differentiable on feasible utility increases. The logit choice formula gives product a share proportional to , with in the denominator for the outside option. He, Ke, and Zhang, §2, pp. 7–9.
Equation (7) uses a nonnegative effort multiplier . A marketing effort allocation, or MEA strategy, is the vector with every . Its total marketing effort, or TME, is . In these coordinates the firm's program (8) maximizes
over every feasible . The first term is revenue and the second is marketing cost. A strategy is concentrated in Definition 1 exactly when one multiplier is positive and all the others are zero. In particular, the zero allocation is a separate case. The transformed cost is . He, Ke, and Zhang, pp. 10–11, equations (7)–(8), Definition 1, Proposition 1.
For positive total effort , product 's MEA index is , where
It equals the revenue when all is assigned to product . This is Definition 2 and the sentence immediately following it. He, Ke, and Zhang, p. 12, Definition 2, equation (9).
The goal is Proposition 1 with its implicit edge cases made explicit. If is concave on , an optimum exists, some optimum is concentrated or zero, and pairwise distinct products have no mixed optimum:
The milestone list follows the source's fixed-effort results. Lemma 3 bounds a weighted ratio by its largest component ratio and characterizes equality. The index interpretation and equation (C–9) connect that inequality to revenue. Lemma 4 concerns revenue at fixed TME, while Lemma 5 concerns cost at fixed TME. Proposition 2 restricts which products can receive positive effort at a profit optimum. Claim 1 and Lemma 6 address tied MEA indices at a positive optimal TME. He, Ke, and Zhang, Online Appendix C, pp. 40–43.
The proposition identifies a class of marketing cost functions under which the firm can choose a single flagship product without giving up optimal profit. Under a distinct-product condition, it characterizes every optimum up to the possibility of zero total effort. The MEA index separately identifies which products can carry positive effort at an optimum. These statements let a solver study effort concentration and product selection within one common optimization model. He, Ke, and Zhang, Propositions 1–2, pp. 11 and 14–15.
The paper proves these results on paper. This mission asks for machine-checked proofs of the model-specific statements, including the edge cases left implicit in the printed wording. It also establishes reusable finite-sum facts, especially the ratio inequality and its equality condition. No machine-checked proof of this paper's marketing-effort theorem is claimed here.
A larger markup does not always make a product the best flagship. Revenue depends on every product's logit attraction and on the outside option, while cost depends on the entire allocation. Maximizing revenue at a fixed total effort therefore does not by itself solve the firm's original problem, whose total effort is also chosen. Ties in the MEA index create another difficulty: at a fixed total, several products can share effort without changing the revenue, so a concentration statement about every optimum needs a separate condition. He, Ke, and Zhang, §2.1 and Online Appendix C.
Products are indexed by Fin n; the book's indices are relabeled from zero. All monetary, utility, and multiplier quantities are real numbers. Strategies range over all nonnegative vectors, and optimality compares profit against every such vector. The outside-option attraction is . The cost assumptions apply on , and transformed-cost concavity applies on , the ranges reached by feasible allocations. The formula is used only for , so its terms never rely on Lean's default value for division by zero. Since , every logarithm in the objective has a positive argument.
The goal includes existence of an optimum so that its statement about all optima has content. It distinguishes zero effort from Definition 1's concentrated allocation: zero effort can be optimal. Pairwise distinct are required for the assertion about every optimum; identical products can support mixed optima. The paper says an optimum is “generically unique” but does not define a generic set or prove uniqueness of the optimal total effort under a specified genericity condition, so that phrase is outside this goal. Lemma 3 separately requires a positive total weight; Claim 1 restricts its rational curves to nonconstant ones. The printed proof of Lemma 6 has a gap for constant tied index curves, noted for reviewers. He, Ke, and Zhang, Definition 1, Proposition 1, Online Appendix C.
The development needs finite sums, real exponentials and logarithms, elementary calculus, and convexity and concavity on intervals. Its model definition is paper-specific; the ratio bound and rational-curve identification are useful beyond this setting. Contributions to any of the stated milestones, including their explicit boundary cases, are in scope.
In this paper, we show the equivalence of the set of unitaries computable by the circuits over the Clifford and T library and the set of unitaries over the ring , in the single-qubit case. We report an efficient synthesis algorithm, with an exact optimality guarantee on the number of Hadamard and T gates used. We conjecture that the equivalence of the sets of unitaries implementable by circuits over the Clifford and T library and unitaries over the ring holds in the -qubit case.
This mission is the statement-level formalization of Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates (arXiv:1206.5236v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact single-qubit H/T synthesis characterization (Theorem 1 (abstract seed): exact single-qubit synthesis characterization, PDF p. 2). 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Public and healthcare services — driver's licence offices, emergency rooms, testing sites — are spread over a region, and customers choose for themselves which facility to visit. A customer weighs two costs: the travel distance to a facility and the expected wait once there. The wait depends on how many other customers chose the same facility. The resulting division of the region is therefore an equilibrium rather than a geometric given, and it can differ from the division a central planner would impose. Deciding when selfish choices are socially efficient, and how a provider should spend a fixed service budget across facilities, is a basic question in spatial queueing and service-system design.
J. G. Carlsson, X. Peng and I. O. Ryzhov (SSRN 4794156, later published in Manufacturing & Service Operations Management, 2024) model each facility as an M/M/1 queue and show three things. The decentralized equilibrium is an additively weighted Voronoi diagram. Locally optimal centralized partitions are also weighted Voronoi diagrams, with weights given by a gradient. And if the service rates are chosen to minimize total social cost, the decentralized equilibrium is exactly the planner's partition. The last statement is Theorem 6 of the paper and the goal of this mission.
A closed convex region carries a normalized demand : a probability measure on , absolutely continuous with respect to Lebesgue measure (the measure of the paper). Customers arrive at aggregate rate . There are facilities at points . A continuous metric gives travel distances . Facility serves at rate .
A partition of is a family of measurable sets covering whose pairwise intersections are -null. The area of is , the fraction of demand it holds. If facility serves the fraction , its expected waiting cost, scaled by , is
A decentralized demand equilibrium (1) under rates is a partition in which no customer prefers another facility:
For weights , the weighted Voronoi cell of facility is . The equilibria are the diagrams whose weights solve , condition (3).
The social cost (15) of rates and a partition is
minimized subject to the budget , where .
A general partitioning problem (9)–(12) minimizes over partitions. It carries a regularity condition: for , the law of with has a density.
Let be a local optimum of (15) with every area . Then a decentralized equilibrium under exists, and every such equilibrium satisfies
Since a global optimum is a local optimum, the best attainable social welfare is reached by decentralized customer behaviour once the rates are set correctly.
The result separates two sources of inefficiency in spatial service systems. When the rates are fixed badly, decentralized choice can be far from socially optimal: in the paper's §4.2 example, customers crowd a high-capacity facility while a nearby one is underused. Theorem 6 shows that the inefficiency is not in the customers' behaviour but in the capacity allocation. With the rates of (17), a square-root rule in the areas, the planner gains nothing by dictating assignments. Theorem 4 is of independent interest for computational geometry. It identifies the Voronoi weights of a locally optimal partition with the gradient of the area cost, which makes nonconvex area costs tractable.
None of these results has a machine-checked proof. The mission produces formal statements of the paper's chain, from the semi-discrete inner problem (Lemma 6) through the first-order condition (Theorem 4) to the identification (Theorem 6), and invites proofs of each. The rate step is closely related to Kelly's square-root capacity allocation (Kelly 1979, Theorem 4.1), which is already proved on the platform and is included as a referenced item.
The weighted Voronoi part and the algebra of (16)–(17) are elementary. The weight lies in Theorem 4 and Lemma 6. The obvious argument moves a small amount of demand from one cell to another and compares costs to first order. It shows only that no pair of cells can be improved. It does not give a single vector of weights consistent across all cells, and that is what Lemma 6 asserts: the existence of dual constants for a semi-discrete transport problem. Existence of such constants requires the regularity condition and positive areas, and fails without them. Theorem 5 must also cope with a cost that is nonconvex and differentiable only at positive areas, and with a joint neighbourhood in rates and partitions.
Lean works in EuclideanSpace ℝ (Fin n) with ν : Measure. Partitions are families Fin K → Set (E n) of measurable subsets of , covering , with -null pairwise intersections. Areas are (ν A).toReal. The waiting cost is real-valued: every equilibrium, feasibility condition and equilibrium-weight condition carries the stability conjunct , replacing the paper's . Under the goal's rates no equilibrium of the paper is lost by this. A local optimum means: for some , no feasible competitor with and for all is cheaper. Identities between partitions, and the pointwise conclusions of Lemma 6 and Theorems 4–5, hold up to -null sets. A null modification of an optimum is still optimal, so the pointwise readings are false.
Added hypotheses, each disclosed in the item: every (resp. ) is -integrable; the areas of the optimum in Theorems 5–6, and the prescribed areas in Lemma 6, are positive. The paper's positive intensity is dropped, and Theorem 4 asks only for continuous and differentiable at . Both changes weaken the hypotheses. The regularity condition is a push-forward measure absolutely continuous with respect to Lebesgue measure. The maps are continuous, so this condition is not vacuous.
A trivializing formalization is ruled out. The goal does not assume the optimum satisfies the Voronoi condition with weights (16), which would be Theorem 5. It quantifies over every decentralized equilibrium under and asserts that one exists.
Welcome contributions include semi-discrete optimal-transport duality (Lemma 6), nonatomic exchange arguments for partitions, and measure-level facts about weighted Voronoi diagrams. All of these are reusable well beyond this paper.
KellyReversibility.Allocation.optimal_capacity_allocation.The periodic-review inventory problem asks how much stock to order in each of periods when demand is random, unmet demand is backlogged, and both leftover stock and shortages are charged. When the demand distributions are known, a backward dynamic program computes an optimal policy, and the optimal policy is a base-stock policy: in each period, order up to a fixed target level (Zipkin, Foundations of Inventory Management, 2000). In practice the distributions are rarely known; what is available is data, or a simulator that produces demand scenarios.
Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) asked how many sampled demand scenarios suffice to compute a policy whose expected cost is provably within a factor of optimal, with a sample size that depends on , the confidence , the horizon and the cost parameters, but not on the demand distributions. For the single-period newsvendor problem they proved such a bound for sample average approximation (their Theorem 2.2). For the multiperiod model they designed a new algorithm and proved the bound that this mission targets (Theorem 3.5 of §3.3).
Periods are indexed (the paper counts from ). The demand of period is a real random variable with law and finite mean, possibly negative. Demands of different periods are independent but need not be identically distributed. Orders arrive immediately, there is no ordering cost, and unmet demand is backlogged. Raising the inventory to in period costs, at the end of the period, with .
The algorithm (§3.3, p. 835). Given and , put , and . The paper states:
In stage , consider the function defined above with respect to the previously computed base-stock levels (where ). Use the black box to generate independent samples of the demands and compute . Note that in each stage, the algorithm is using an additional samples that are independent of the samples used in previous stages.
For , , independent demand laws with finite mean, and , the levels computed by the algorithm satisfy
Here is the expected cost of the computed policy and is the optimal expected cost. The constants are those of the paper; the goal fixes the algorithm, not a class of algorithms.
Hoeffding's inequality (Theorem 3.4) enters through Lemma 3.5; Concentration.hoeffding_two_sided is included as a reference item.
The theorem gives sample sizes that grow polynomially in , , and , and are uniform over all demand distributions with finite mean. The analysis shows that a sampled dynamic program need not lose control of convexity: the upper base-stock invariant keeps every stage a convex problem, and relative errors made in later stages multiply rather than compound through the recursion.
The result has been proved on paper since 2007. As far as a search of the platform shows (October 2026), none of its lemmas has a machine-checked proof; the platform has single-period newsvendor material from other papers, and a two-sided Hoeffding inequality. A formalization would supply a finite-horizon stochastic inventory dynamic program and its shadow version as reusable objects, a one-dimensional bridge from approximate first-order optimality to relative error (Lemma 3.3), and an end-to-end checked sample-complexity bound for a multistage stochastic model.
The naive argument estimates each stage's minimizer by sampling and adds up the per-stage errors. It fails twice. First, once a later stage uses an approximate level, the earlier stage's cost-to-go is no longer that of an optimal policy and need not be convex, so "the minimizer" may not exist and its sampled estimate has no guarantee. Second, an additive error in a later stage's cost can be amplified by the earlier stages. The paper's invariant, which requires each computed level to lie above the true shadow minimizer, controls both, and the formalization has to establish this invariant from samples with high probability. Measure-theoretically, the costs are nested expectations of infima, a one-sided derivative must pass through an expectation over a demand path, and stage-wise events must be combined although earlier levels are random.
HasDerivWithinAt on . Probabilities of events are measures of sets, which are outer measures on non-measurable sets.The symmetric traveling-salesman problem asks for a cheapest cycle through all vertices of a complete graph with real edge weights. Every exact method for it rests on lower bounds, and the most widely used one comes from Held and Karp's two papers of 1970–71 (Held & Karp 1970; Part II, 1971). Their bound is built from 1-trees, a slight variant of spanning trees that can be computed greedily, and is improved by perturbing the edge weights with vertex penalties .
The 1970 paper answers the natural question about this bound: when is the best 1-tree bound equal to the optimal tour weight? Its answer ties the combinatorial bound to the classical subtour-elimination linear program of Dantzig, Fulkerson & Johnson (1954): the best bound is the value of that linear program, and it closes the gap exactly when the program has an integral optimum. This identification, "Held–Karp bound = subtour LP value", is used throughout the later literature on TSP relaxations and integrality gaps.
Let be the complete undirected graph on the vertex set , , with an arbitrary real weight on each edge ; no sign, metric or integrality condition is imposed. The weight of a subgraph is the sum of its edge weights. A tour is a cycle through every vertex exactly once. A 1-tree is a tree on the vertex set together with two distinct edges at vertex .
For a real vector the transformed weights are . The gap function is
Write for the weight of a minimum tour under , and, indexing the 1-trees by with weight and degrees ,
Vectors live on the edges of , with and degree at vertex . The integer program (3) asks for degree at every vertex, the subtour constraints for every nonempty proper subset , and integrality; its feasible points are the tours. Its rewritten form (3′) has (i) degree at , written ; (ii) ; (iii) ; (iv) the subtour constraints; (v) ; (vi) ; (vii) integrality. The paper denotes (ii)–(v) by . The linear program (4) is
This is the abstract's headline, " precisely when a certain well-known linear program has an optimal solution in integers", stated in the paper's own form.
The result. Theorem 2 says that the best lower bound obtainable from 1-trees with vertex penalties equals the optimal value of the subtour linear program. The bound can therefore be computed either combinatorially, by ascent over with minimum-spanning-tree computations, or by linear programming, and any statement about the integrality gap of the subtour LP is a statement about the Held–Karp bound. Corollary 1 is the exact criterion for when the bound is tight: the gap closes precisely when the LP has an integral optimal solution, in which case that solution is an optimal tour. Theorem 1, a description of the 1-tree polytope by linear inequalities, is the polyhedral fact underneath.
Formalizing it. The results are classical and proved on paper. As far as the platform's catalog shows, none of them is machine-checked. The published Part II mission (HeldKarp.Ascent) formalizes the ascent method and the bound tour weight; this mission adds the polyhedral side: the subtour LP, the 1-tree polytope, and the equality of the bound with the LP value. A complete development yields a reusable statement of LP-based lower bounds for the TSP on general real weights, which existing metric-TSP items do not cover.
Lemma 1, the identity , Lemma 2 and the tour correspondence are finite bookkeeping over graphs and edge sums. The substance is Theorem 1. The paper proves it as a special case of Edmonds' theorem on matroid base polytopes (§6, p. 1157), applied to the 1-tree matroid; formalizing that route requires the base-polytope theorem for a matroid that Mathlib does not provide. The printed specialization also has a gap (finding F3): the list of spans of the 1-tree matroid on p. 1157 omits the single edges , so the system it lists has a non-1-tree vertex already for . Theorem 1 itself is unaffected, because (3′) contains , but a proof that follows the page sentence by sentence will fail at that step. Theorem 2 rests on linear-programming duality for a program with equality constraints, which has to be available in the form the argument uses, and on Theorem 1; attainment of both the maximum and the minimum is part of the statement and has to be proved, not assumed.
Vertices are Fin n; the paper's vertex is 0 : Fin n and vertex is the last element lastV n. Weights are a function c : Sym2 (Fin n) → ℝ on unordered pairs, so symmetry is built in and the diagonal is never used. Tours, 1-trees, the weight of a subgraph and (oneTreeBound) are the published definitions HeldKarp_Ascent_IsOneTree and HeldKarp_Ascent_oneTreeBound of the Part II mission. The new definitions are HeldKarp_Gap_GapFunction (transformed weights, minimum tour and 1-tree weights, the gap) and HeldKarp_Gap_SubtourLP (edge vectors on the type Edge n of unordered pairs with , degrees, the programs (3), (3′) and (4), optimality, incidence vectors).
Conventions committed to:
These choices rule out the trivializing formalizations: with the gap is identically while (4) is infeasible; with allowed every program is infeasible; with (ii)–(iii) as inequalities Theorems 1 and 2 fail; with optimality among integer points only, the right side of Corollary 1 always holds; and defining as would empty milestone 2.
A complete development needs finite sums over Sym2, simple-graph trees and cycles, extreme points of polyhedra (Set.extremePoints), and linear-programming duality. The 1-tree polytope description and an LP duality statement with equality constraints are reusable beyond this mission. Proofs of any milestone, alternative routes to Theorem 1 that avoid matroids, and a formal account of the §6 matroid theorem are all welcome.
A Markov decision process (MDP) with the average cost per unit time criterion models a controller who runs a stochastic system indefinitely and cares about long-run cost rather than any finite horizon: inventory control, queueing control, and maintenance are standard examples. The basic questions are whether an optimal policy exists, whether it can be taken stationary (a fixed measurable rule ), and whether it is characterized by an average cost optimality inequality (ACOI).
For uncountable state spaces the classical answer is Schäl's (Math. Oper. Res. 18, 1993), under weak continuity of the transition probabilities, compact action sets, and a uniform bound on the relative discounted values. Hernández-Lerma replaced compactness by inf-compactness of the cost in the action, but under setwise continuity; Feinberg and Lewis (Math. Oper. Res. 32, 2007) allowed noncompact actions under weak continuity, at the price of inf-compactness of the cost in state and action jointly plus a local boundedness condition. That joint inf-compactness excludes bounded costs on unbounded state spaces, the setting of Ross and of Dynkin and Yushkevich. Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 37(4), 2012) remove both restrictions.
The state space and action space are Borel subsets of Polish spaces. Each state has a nonempty Borel set of available actions; the graph is Borel and has a measurable selector. Choosing at costs (bounded below, measurable) and moves the system according to a transition probability . A policy is a sequence of randomized, history-dependent decision rules concentrated on ; the set of stationary policies consists of Borel maps with .
For the discounted cost is and the average cost is . Optimal values are infima over all policies: , , and . Put , the relative discounted value , and .
The assumptions are:
The candidate relative value function is the joint lower limit
and the candidate optimal actions are .
Under (W*) and (B̲) there is with
and for it for all . Moreover (a) is finite and lower semicontinuous; (b) each is nonempty and compact and is Borel; (c) every selecting from is average cost optimal and satisfies the inequality; (d) some selects from the minimizer sets of ; (e) under (Wu), is inf-compact.
In the paper's order: Theorem 1 (the inequality with implies optimality), Lemma 2 (inf-compactness in the action), Lemma 3 (lower semicontinuity of the minimal value and a Borel minimizer), Lemma 4 (a Fatou lemma for weakly converging measures, already on the platform as Schäl's Lemma 2.3(ii)), Theorem 2 (i), (iv)–(vi) (the discounted problem under (W*)), Lemma 6 (semicontinuity of , and the auxiliary ), Corollary 1, and Lemma 7, the ACOI itself. Schäl's inequality is referenced as an existing platform item.
Theorem 3 gives stationary average-cost optimal policies for weakly continuous MDPs with noncompact action sets and costs that need not be inf-compact in the state, which covers bounded costs on unbounded state spaces and inventory models whose holding costs do not grow without bound. Assumption (B̲) asks only for a finite lower limit of as , weaker than Schäl's uniform bound. The approach was extended to partially observable MDPs and to later work on the average cost optimality equation, which builds on exactly these objects.
The theorem is proved in the literature; nothing here is open mathematically. What the mission adds is a machine-checked proof of the full chain from measurable selection and semicontinuity through the vanishing-discount limit, for Borel spaces and history-dependent randomized policies. Reading the proofs closely has turned up three printed statements that are false as written (see Beyond the paper); a formal development settles exactly which hypotheses each step needs.
The obvious route takes a limit of discount-optimal policies as . With noncompact such a sequence need not have any limit point; (W*)(ii) supplies one only when the costs along it stay bounded, and that has to be extracted from the relative values. The second obstacle is that is controlled only through its lower limit at each point, so is a joint lower limit in and passing it under requires a Fatou-type lemma for weakly converging measures rather than dominated convergence. Finally, selecting a Borel from the sets requires a uniformization theorem for Borel sets with -compact sections (Arsenin–Kunugui), which Mathlib does not have.
The spaces are types with a separable metrizable topology whose Borel -algebra is standard Borel (by Lusin–Souslin, exactly the Borel subsets of Polish spaces up to homeomorphism). The model reuses the published definitions FeinbergLiang_ACOE_MDP (policies, path measures via Ionescu–Tulcea, discounted and average costs) and SchalAvg_AvgOpt_Model (action sets, admissible policies, , , , , , Assumption (G)). Conventions:
HasSelector.Optimal values are infima over all admissible (randomized, history-dependent) policies, not over stationary ones. is the fixed function (21), never a free parameter. All four equalities of (10) are stated for every . (W*), (Wu) and (B̲) constrain and on only. A statement that ranged over a smaller policy class, left free, kept a single equality, or imposed continuity on all of would be a different and easier theorem.
A complete development needs: semicontinuity and inf-compactness calculus for -valued functions; lower semicontinuity of under weak convergence for lower semicontinuous ; the Arsenin–Kunugui uniformization theorem; discounted dynamic programming on Borel spaces; and an Abelian/Tauberian comparison of with Cesàro averages. The first three are reusable well beyond MDPs. Contributions to any milestone, or to these libraries, are welcome.
Beyond the paper. Three corrected variants are posed beside the faithful statements, which stay as printed. Lemma 2, corrected: as printed it assumes only (W*)(ii) (and (iii)), but without lower semicontinuity of a level set such as need not be compact; the variant adds (W*)(i). Lemma 3, corrected: can fail because may be identically for some ; the variant asserts lower semicontinuity only. Corollary 1, corrected: the joint limit need not exist (a one-action example with an indicator cost); the variant uses the lower limit, which is what the proof computes and what Lemma 7 uses. A misprint in the proof of Lemma 3 (p. 598, for ) does not affect its statement.
A convex optimization problem can be handed to a semidefinite programming solver only after its constraints and objective have been written as linear matrix inequalities (LMIs): conditions of the form , where is affine in the decision variables and in auxiliary variables , and means positive semidefinite. A large share of modern engineering optimization is built this way, in robust control, structural design, and statistics and machine learning (nuclear-norm and spectral-norm regularization, eigenvalue optimization). Modeling tools such as CVX and YALMIP rest on a catalog of functions known to admit such a description.
Lecture 4 of A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), builds that catalog for the semidefinite cone. Its central entry is a general rule: a convex function of a symmetric matrix that depends only on the eigenvalues, symmetrically, is expressible by LMIs whenever the underlying function of a vector is. This covers the largest eigenvalue, sums of the largest eigenvalues (Ky Fan, 1949), Schatten norms and powers of the determinant at once. The tool behind it is the theory of majorization (Hardy, Littlewood and Pólya, 1929; Rado, 1952) together with Birkhoff's theorem on double-stochastic matrices (1946).
For a symmetric real matrix , denotes its eigenvalues counted with multiplicity in nonascending order, . is the sum of the largest. For a vector , is the sum of its largest entries, and is the convex hull of the coordinate permutations of . A function is symmetric if permuting the coordinates of its argument leaves its value unchanged. A matrix is double-stochastic if its entries are nonnegative and every row and column sums to .
A function is semidefinite representable (SDr) if there is a map , affine in with values in the symmetric matrices, such that
For a matrix (), the singular values are , and .
Let be symmetric and SDr with representation . Then for every symmetric matrix and real ,
FamousTheorems.birkhoff_von_neumann.A strengthened variant of the goal states that (4.2.3) remains exact when the ordering constraint is removed.
The result itself. Proposition 4.2.1 reduces semidefinite representability of a spectral function on , a space of dimension , to semidefinite representability of a symmetric function on . The extra cost is scalar variables, ordering inequalities, Ky Fan constraints (each an LMI of size by 18.c) and one trace equation. The representation is explicit, so a modeling language can generate it mechanically. Proposition 4.2.2 does the same for functions of singular values, which covers the nuclear norm and the operator norm of rectangular matrices. Fact (D) is the variational description that makes convex (Davis, 1957; Lewis, 1996).
Formalizing it. All results here are classical and proved in the book, partly through exercises (4.14–4.16 for the goal). None of them is formalized on Prove2Me beyond Birkhoff's theorem, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix. A related proved platform item, Matrix.IsHermitian.sorted_eigenvalues_le_add_of_re_dotProduct_le, is a Weyl-type inequality that implies (A) when its slack is zero. Mathlib has sorted eigenvalues of Hermitian matrices (eigenvalues₀) but no Ky Fan sums, no majorization theory and no notion of semidefinite representation. This mission produces them.
The forward direction of every representation is a choice of witness. The content is in the converse: from an arbitrary feasible point of the LMI system one must recover the inequality for the eigenvalues. For (4.2.3) this means showing that partial-sum domination plus equal totals places inside the convex hull of the permutations of the witness . The obvious coordinatewise comparison fails, because is not dominated entrywise by . The hard half of the majorization principle (Exercise 4.15) is this step, and it does not follow from convexity of alone. In Proposition 4.2.2 the witness only dominates the singular values in partial sums, with no equality of totals, so majorization alone does not suffice there.
Vectors are Fin m → ℝ (0-based indices) and matrices Matrix (Fin m) (Fin m) ℝ. Symmetric means Matrix.IsHermitian and means Matrix.PosSemidef, which includes symmetry. is Mathlib's antitone IsHermitian.eigenvalues₀; it is applied only to symmetric matrices. Functions with values in are EReal-valued and never , and only order comparisons with real numbers are made on them. A representation is an explicit affine map with symmetric coefficient matrices. In Proposition 4.2.2 the function , given on only, is extended by outside . The singular values are written as , which equals . Typos on the page are corrected and listed in the items: for in 18.c, and and in Proposition 4.2.2.
The claim " is SDr" admits a trivializing formalization: asserting that some LMI system projects onto the epigraph, with no control over its shape or size, says nothing beyond convexity. Every statement here instead pins the representation down as the book's explicit system (4.2.2), (4.2.3) or (4.2.4), quantified over every symmetric matrix and every real .
Beyond the paper. One strengthened variant is posed: Proposition 4.2.1 with the constraint removed from (4.2.3) (finding F1). The evidence is that never exceeds the sum of the largest entries of , so the remaining constraints already express majorization. The variant is not a milestone, and the book's statement stays the goal.
A complete development needs:
Majorization, the Ky Fan representation and fact (A) are reusable well beyond this chapter, for instance in eigenvalue optimization and the analysis of interior-point methods. Contributions of these as standalone results are welcome.
An information designer can change what others know without choosing their actions. When several designers disclose information at once, each designer's experiment affects the incentives faced by agents who receive messages from all of them. The resulting strategic problem appears in competing disclosures, advice, and mediated decisions. Koessler, Laclau, and Tomala study this interaction in a finite-state model and ask whether the designers and agents can play consistently at every continuation of the game. Their working paper proves an existence result for this general model before examining special splitting, corporation, and multi-period games.
The existence question has a specific obstacle. After seeing the designers' experiments, agents may have several optimal continuation behaviors. A designer's payoff can jump as those behaviors change with the experiment profile. The paper's Example 5 shows that some ways of selecting an agent equilibrium at each profile yield an induced game between designers with no approximate equilibrium. The continuation behavior must therefore be part of what the equilibrium chooses; a fixed arbitrary rule cannot be presumed adequate. The paper invokes the equilibrium-selection result of Simon and Zame (1990) for this step. The example and the proof are in the working paper, pp. 6–7 and 21–23.
Let be a nonempty finite set of designers and a nonempty finite set of agents. Designer holds a component of the state, drawn with a common prior on . The prior is general: its coordinates may be dependent. Agent chooses an action in a nonempty finite set , and the action profile lies in . Designer and agent receive real payoffs and respectively. The primitive model appears in §2, p. 5.
Designer can send agent a message in a finite set . The designer's full message profile is . A statistical experiment is a rule : at each value of the designer's state component it specifies a lottery on full message profiles. The designers choose their experiments simultaneously from . Each agent observes the whole experiment profile , but later sees only his own messages . The signal , uniformly distributed on , is public to all agents and may coordinate their action lotteries. Nature draws the state from ; conditional on it, each designer's experiment draws a message profile. This sequence is Definition 1 and the game timeline, pp. 5–6.
For fixed , the agents play a Bayesian continuation game . Its equilibrium-outcome correspondence consists of conditional distributions of action profiles given all messages that can arise from Bayes Nash behavior using the public signal. The agents' incentive test is ex ante: each agent may replace his entire private-message-to-action-lottery rule while the others keep theirs. Private messages with zero probability impose no incentive restriction. Public randomization allows convex combinations of equilibrium outcomes. As stated in §2, p. 6, is nonempty and convex and is the set of public correlated equilibrium outcomes.
An equilibrium selection chooses one at every and is Borel measurable. For a selected outcome, designer receives
The designers may themselves mix: designer chooses a Borel probability measure on , and the profile law is the product of these measures. By Definition 2, p. 6, an equilibrium of is a selection together with a mixed Nash equilibrium of the designers' induced game. Selection at every gives the agents equilibrium behavior in every continuation subgame.
The goal is Theorem 1, p. 6: for every finite profile of message sets, the game admits an equilibrium. With and , the statement is
The milestone list follows the assertions used in the paper's proof. It first records the nonemptiness, convexity, and public-correlation characterization of ; then the compact convex values and upper hemicontinuity of and . The final two milestones record a Borel measurable payoff selection whose designers' game has a mixed equilibrium, and a Borel measurable continuation selection that realizes that selected payoff. These statements are on pp. 6–7.
Theorem 1 guarantees that the general finite-message model has at least one consistent profile of information design and agent continuation behavior. It permits multiple designers, arbitrary correlation in the prior, messages sent privately to different agents, and mixed experiment choices. The result supports the paper's later analysis by ensuring that the baseline game has an equilibrium even though an arbitrary continuation selection need not support one. The theorem is proved in the paper; the machine-checked proof and reusable formal infrastructure are the work of this mission.
Formalizing the result adds a precise interface for finite statistical experiments, agent continuation equilibria with public correlation, set-valued payoff maps, measurable selections, and mixed deviations over spaces of experiments. The finite-game lottery predicate from the published agt_games definition and its proved Nash-existence theorem are available as prerequisites. The remaining public-device, continuity, and selection material can serve other Bayesian-game formalizations.
The obvious first step is to choose one equilibrium outcome of the agents' game at each experiment profile and then seek a Nash equilibrium of the designers' game. That step fails because the chosen continuation outcome may change discontinuously with the experiments. In the paper's Example 5, a particular legitimate selection gives an induced zero-sum game with a gap between maxmin and minmax payoffs, so it has no approximate equilibrium. An argument that assumes every measurable selection works would be false. The existence theorem needs a selection compatible with mixed strategic behavior, and it needs that selection realized by actual agent equilibrium outcomes. Both demands are represented in the last two milestones.
The Lean model uses finite nonempty designer, agent, state, action, and message types. Nonempty message sets are an explicit addition to the printed hypotheses: if one such set were empty, that designer would have no experiment and the existence claim would fail. The paper's printed action-product index is read as , the agent index, because actions belong to agents. The common prior is a lottery on the whole state profile, without a product assumption.
Finite lotteries are nonnegative real weight functions summing to one. The experiment spaces inherit the finite-dimensional product topology and Borel sigma algebra. The public signal has Lebesgue probability law on ; its strategy process is measurable and Bayes Nash at almost every signal value. The outcome correspondence is constructed from these processes, with no free outcome variable unrelated to agent incentives. Upper hemicontinuity uses the open-neighborhood definition. Designer mixed profiles are independent Borel probability measures, and deviations range over every such measure. Integrability is required for the mixed payoff and every deviating payoff, avoiding Lean's default value for a nonintegrable Bochner integral.
The target requires an existential Borel selection that belongs to at every . A fixed selection, a nonmeasurable selection, or an unconstrained outcome map would alter the theorem. Contributions that establish compactness, upper hemicontinuity, measurable selection, and the mixed-equilibrium conclusion for these exact definitions are in scope. The separate results on splitting games, corporations, and multi-period play are outside this mission.
Large service systems such as call centres, hospital wards and cloud server farms route several customer classes to several server pools, with each pool trained for only some of the classes. Staffing such a network sits between two failure modes: too few servers make queues explode, and too many waste capacity. In the Halfin–Whitt (quality-and-efficiency-driven) regime, arrival rates and pool sizes grow like and the staffing surplus or deficit of each pool is of order . Whether those surpluses can be scheduled into a stable system is a question about the network as a whole: a surplus in one pool can serve a deficit elsewhere only through the compatibility graph.
Hmedi, Arapostathis and Pang (arXiv:2009.01942, v3, 2021; Operations Research 2023) answer this for networks whose compatibility graph is a tree and that have no abandonment. They introduce one number, the system-wide safety staffing (SWSS) , the value of a small linear program. They prove that its sign decides stability.
Timeline.
There are classes and pools. Write if pool can serve class , and assume the bipartite graph with these edges is a tree. The first-order rates are , and , and the second-order corrections are . Complete resource pooling (CRP) means that the linear program "minimize subject to , on the edges" has a unique solution , with and on every edge. Put and .
For a positive probability vector , the SWSS parameter is the optimal value of
over and supported on the edges.
Let be the unique array on the edges with row sums and column sums (defined when ). Let . The limiting controlled diffusion is
with and a standard Brownian motion. Here is the total queue, the number of idle servers, and the control says how queued customers are split among classes and idle servers among pools. A stationary Markov control is a Borel map , used as .
(a) If , then for every edge , under the constant control , the diffusion has a unique invariant probability measure . Moreover there are , and such that, with ,
(b) If , then under every stationary Markov control almost surely. If , then under every stationary Markov control there is no invariant probability measure.
The theorem turns a stochastic stability question into the sign of a linear-program value computable from the network data. Positive SWSS is the condition under which a staffing rule with safety capacity can be made stable by scheduling, and the proof exhibits a simple stabilizing control. The identity links the LP value to the drift of the diffusion. It extends earlier uniform-stability results from networks with a single non-leaf pool to arbitrary trees.
The results are proved on paper. This mission produces machine-checked statements, and eventually proofs, of the limiting-diffusion half. That requires:
No part of this is formalized elsewhere. The existing platform layers for Halfin–Whitt diffusions concern single-pool networks.
The linear-algebra half is a genuine induction on trees, not an unfolding of definitions. Theorem 2 eliminates leaves class by class. Theorem 3 identifies the gains with the entries of , which forces to be invertible and to be positive. Theorem 4 then rewrites the LP value through the drift.
The probabilistic half is harder:
Classes are Fin I and pools Fin J, and the tree is SimpleGraph.IsTree on Fin I ⊕ Fin J. States are EuclideanSpace ℝ (Fin I), and control values are pairs of vectors in Mathlib's stdSimplex. Strong solutions, standard Brownian motion, invariant measures, the generator and the weighted total-variation norm are the published EthierKurtz, GPhNGIDiffusion.EMError and UnifErgHW.Diffusion definitions. The weighted norm uses the weight , which is equivalent to the paper's -norm up to a factor .
Conventions committed to:
The statement admits trivializations, each ruled out:
For the instability clauses, strong solutions exist and are pathwise unique for every Borel control (a theorem of Veretennikov, 1981, and its locally bounded extensions; the drift is locally bounded with linear growth and the noise is additive and nondegenerate). This is background, not a claim of the mission.
Out of scope: the clauses of Theorem 1 about the diffusion-scaled th systems (Theorems 6 and 8), and the half of Theorem 4. They need a controlled continuous-time Markov chain layer with work-conserving action sets, which does not exist on the platform.
Welcome contributions:
Decision analysts routinely have to rank two risky prospects, with returns and , when nothing is known about them beyond a mean and a standard deviation for each. The classical tools are of two kinds. First-order stochastic dominance (FSD) ranks above for every increasing utility, but it can never be certified from means and variances alone: with only the first two moments fixed, the admissible laws of and include pairs that FSD does not rank. Mean–variance rules such as the Sharpe ratio rank everything, but lack a general expected-utility justification. Müller, Scarsini, Tsetlin and Winkler (Ranking distributions when only means and variances are known, Operations Research 69(3), 2021; SSRN 3440103) close the gap by restricting the utilities: they bound the ratio of marginal utilities, and they ask how strong that bound must be for every pair of laws with the given moments to be ranked.
The relevant order between the two extremes is almost first-order stochastic dominance (AFSD), introduced by Leshno and Levy (Management Science, 2002) to rule out "pathological" utilities that FSD must accommodate. Müller, Scarsini, Tsetlin and Winkler (Management Science, 2017) discuss that this symmetric case of their order is AFSD, i.e. the order generated by utilities whose marginal utilities differ at most by a fixed factor. Leshno and Levy computed the smallest parameter for which one given pair of laws is ranked; the present mission concerns a bound that holds for all pairs with prescribed means and variances.
Fix . The utility class consists of continuously differentiable with
For and real random variables , dominates by -SD, written , if for every . The symmetric case is -AFSD with : gives FSD, and gives the increasing affine utilities, i.e. ranking by means. Increasing shrinks and makes the order easier to satisfy.
Write for the means and for the standard deviations, and
The quantity is a standardized advantage of over ; decreases from at towards as .
The proof works with the piecewise-linear utilities and , with , and with the closed forms
the paper's worst-case values of and given the moments, and the point .
For square-integrable with ,
The goal quantifies over all with the given moments; nothing about their laws is fixed. The upper bound is the domain of the order in Definition 1(b).
PricingRM.DetHeuristic.gallego_bound (the case ).The result. Theorem 7 turns two summary statistics into an expected-utility guarantee: once exceeds the value making , every decision maker whose marginal utility varies by at most the factor prefers , concave or not. It complements the paper's Theorems 3 and 6, which restrict to concave and to convex utilities and give tight bounds in and ; the class contains utilities that are neither, and both standard deviations enter. The paper's Example 8 shows the practical use: with the rule "" settles a project choice for a whole team with heterogeneous, non-concave preferences. The authors note that the bound of Theorem 7 is not tight; the tight constant is open in the paper (Remarks 9–10).
Formalizing it. The result is proved in the paper; none of it is formalized. A formal development produces a reusable definition of the bounded-marginal-utility-ratio class and of AFSD in Mathlib's probability language, distribution-free bounds on expectations of piecewise-linear functions of a square-integrable variable, and a machine-checked version of the threshold. The Scarf/Gallego bound, which the proof uses twice, is already proved on the platform.
The obvious argument fails at the first step: a stochastic dominance relation is usually checked through distribution functions, but nothing about the distribution functions of and is known. For concave utilities (Theorem 3) Jensen's inequality disposes of entirely, which is why that bound ignores ; for the symmetric class no such step is available, both variables must be controlled at once, and the worst case over all laws with given moments must be computed in closed form for a family of utilities rather than for a single one. On the formal side, the normalization step needs the boundedness of to be derived from the ratio condition (there is no supremum hypothesis), the bounds need integrability of for an unbounded , and the threshold computation is real algebra with nested square roots.
Random variables are measurable functions on one probability space , with MemLp X 2 P and MemLp Y 2 P in the goal; only their laws matter. Means are Bochner integrals and with Mathlib's variance, never free reals in the goal. "Continuously differentiable" is ContDiff ℝ 1 and is deriv u. The order SDle carries and integrability of and , because the identity utility is in the class. It compares the expectations for every utility in the class for which both compositions are integrable. This excludes Lean's zero value for a non-integrable integral from a comparison, while keeping the order reflexive when ; every class utility is integrable under the goal's hypotheses. Divisions follow Lean's ; when the paper's is undefined, Lean gives and , and the goal then asserts dominance for increasing affine utilities only, which is true. The worst-case quantities and are stated as the inequalities the proof uses; attainment (the two-point laws) is not formalized.
A trivializing formalization is ruled out: the goal is stated for every in the class, not only for or at a fixed ; for every pair with the moments as hypotheses, not for chosen laws; and with , since for the class contains only constants.
A complete development needs: the mean value inequality for deriv; integrability of Lipschitz functions of an variable; the Gallego bound (available); and elementary real algebra with Real.sqrt. The utility class, the order, and the bounds on , are reusable for Theorems 3 and 6 of the same paper and for other almost-dominance results. Proofs of any milestone, alternative proofs of the goal, and formalizations of Theorems 3 and 6 are welcome.
In 1923 Hardy and Littlewood proposed two conjectures about the distribution of primes that have shaped a century of analytic number theory. The first — the prime -tuple conjecture — predicts that every admissible prime constellation occurs with a precise asymptotic density: the number of constellations with base point grows like , where the singular series constant is an explicit Euler product over the residues of the offsets modulo the primes. For the twin offsets this specializes to the twin prime conjecture with the twin-prime constant . The second conjecture asserts that the prime-counting function is subadditive: . Richards proved in 1974 that the two conjectures are incompatible — at most one of them is true. The source file states all three results in Lean 4: the two conjectures as open problems, and the incompatibility as a theorem.
The mission takes the first conjecture — the file's title statement, and the one widely believed — as its goal. It formalizes the conjecture's definitional core (prime constellations, admissibility, counting functions, the singular series), and curates as milestones the structural facts any proof must engage: the translation-invariance of admissibility, its necessity for primality, the vanishing count for inadmissible tuples, the divergence of the logarithmic-integral model, the positivity of the singular series, the infinitude consequences down to the twin prime conjecture, and Richards' incompatibility with the second conjecture.
The arena is the set of prime constellations: tuples of primes with even gaps, encoded by a function of offsets with . A constellation is admissible when its entries do not form a complete set of residue classes modulo any prime; the counting function counts admissible constellations with base point at most ; the singular series is with the number of residues occupied by the offsets modulo ; and the conjecture asserts for tuples with distinct offsets.
Nine conventions deserve disclosure. First, the platform publishes definitions as modules Definitions.Def_<definition_name>, so the three definition bundles — constellations and admissibility, counting functions, and the asymptotic layer with the singular series — are published as platform definitions (HardyLittlewood_constellation, HardyLittlewood_counting, HardyLittlewood_series) and attached to the proposal as reference items; the theorem drafts import them. Second, asymptotic equivalence is phrased through a self-contained definition — f ~ g when the difference is little-o of g — rather than an external asymptotic-equivalence notation; the formulation coincides with the classical ratio limit when the model sequence is eventually positive and unbounded, and it degenerates correctly: for an inadmissible tuple the singular series is zero, the model vanishes identically, and the conjecture asserts exactly that the counting function is eventually zero, which is the true degenerate content. Third, the counting functions are defined as the cardinalities of finite sets of natural numbers (noncomputable, Classical), with counting primes up to and including , matching the source's phrasing. Fourth, admissibility is split: the source's constellation-level condition is kept verbatim, and the parameter-free condition on the doubled offsets (IsAdmissibleTuple) is added beside it; the equivalence — residue coverage is invariant under translation by the base point — is the mission's first milestone, so nothing is assumed that is not proved. Fifth, the residue count is taken on the offsets themselves, exactly as the source's numResidues; at every odd prime this agrees with the count for the doubled offsets , and the product runs over the primes with the source's normalization and prefactor. Sixth, the singular series constant is defined through the unconditional infinite product; its convergence and positivity are not assumed anywhere — they are the content of a milestone, and the hypothesis that makes the product converge (pairwise distinct offsets) is stated there explicitly, since a repeated offset forces every factor to be and the product to diverge. Seventh, a curation decision: the goal is the first conjecture; the second conjecture is deliberately not drafted as a provable item, because Richards' theorem — itself a milestone — shows that the two cannot both hold; the second conjecture appears as a definition and inside the incompatibility milestone. Eighth, the goal is stated for every tuple, with the conjecture's own hypotheses ( and pairwise distinct offsets) inside the predicate, exactly as the source file states it. Ninth, the read-backs attached to the drafts were written by the same model that produced the statements (readback_model glm-5-latest-short), not by an independent auditor; the human item-by-item comparison against the source remains the main defense against an unfaithful formalization.
The goal is the first Hardy–Littlewood conjecture for every tuple. The supporting chain, in attack order, each step a milestone except the last:
The chain assembles: admissibility is the gatekeeper (necessity and vanishing), the model integral and the singular series are the two analytic quantities the conjecture relates, positivity and divergence turn the asymptotic into infinitude, the twin case is the celebrated concrete consequence, and Richards' theorem fences off the second conjecture.
The prime -tuple conjecture is the strongest concrete prediction about the distribution of primes that is consistent with current knowledge: it implies the twin prime conjecture, the Sophie Germain-type infinitudes, and every admissible pattern one can write down, each with a precise constant. It sits at the edge of the circle method — the same machinery that yields the ternary Goldbach theorem for additive patterns — and its obstruction is exactly the correlation between primes that current technology cannot rule in. A Lean formalization of the conjecture's statement, together with the surrounding structural facts, fixes the target unambiguously and gives solvers an attack path whose every waypoint is independently valuable: each milestone is a theorem of lasting interest in the theory of prime constellations, and the Richards incompatibility is a landmark result of 1974 that the community can be proud to carry.
The milestones span elementary number theory (residue coverage, admissibility, the twin-configuration check), real analysis (the divergence of the logarithmic integral), analytic number theory at the research frontier (the convergence and positivity of the singular series, via Mertens-type estimates), and combinatorial asymptotics for Richards' incompatibility. The admissibility lemmas are of moderate difficulty; the divergence of the model integral is a standard exercise in integral comparison; the positivity of the singular series requires the classical estimate that the Euler product converges on distinct offsets; the Richards milestone requires constructing, from the conjectured density of a suitable long admissible constellation, an interval carrying more primes than subadditivity permits — a research-grade formalization. The goal itself is one of the great open problems of number theory; the mission's value lies in the precisely stated target and the independently valuable waypoints, exactly the role of an OpenProblem mission.
Every item quantifies only over the objects it needs — offset tuples, base points, primes, bounds; no item carries a vacuous hypothesis: the twin configuration is admissible, the conjunctions of the conjecture are satisfiable, and the vanishing and incompatibility statements are the intended degenerate truths. The fragment excludes the second Hardy–Littlewood conjecture as a provable target (Richards' theorem makes it a trap), excludes no case of the first conjecture (it is stated for every tuple, exactly as the source), and adds no hypothesis to the conjecture beyond the source's own. Nothing in the mission asserts the truth of the first conjecture or of the twin prime conjecture; it formalizes the statements precisely, together with the implications among them that are known.
This mission formalizes the question whether the group of interval exchange transformations is amenable, Question 1.6 of Juschenko, Matte Bon, Monod and de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, p. 4 (doi:10.1017/etds.2016.32), together with the landmark results of the literature on the question.
An interval exchange transformation cuts the circle into finitely many arcs and puts them back in a different order. These maps model the dynamics of polygonal billiards with rational angles, and since Katok–Stepin (1967) and Keane (1975) they have been a central object of ergodic theory. Under composition they form a group, . Two questions about this group are open: whether it contains a non-abelian free subgroup (Katok's question), and whether it is amenable, that is, whether it carries a finitely additive, translation-invariant probability measure on all of its subsets. Amenability would answer Katok's question in the negative, since an amenable group has no non-abelian free subgroup.
Timeline.
Write for the circle (UnitAddCircle). A permutation of is an interval exchange transformation (IntervalExchange.IsIntervalExchange g) when it is right-continuous, has finitely many points of discontinuity, and has finitely many angles . Equivalently, cuts the circle into finitely many half-open arcs and translates each of them. The group (IntervalExchange.IET) is the subgroup of permutations of that they generate; a milestone states that it consists of the interval exchange transformations themselves. For a subgroup , the angle group (angleGroup G) is the subgroup of generated by all angles of elements of , and the rational rank (rationalRank) of a subgroup of is the supremum of the such that embeds in it. For a subgroup of , (IETOf Λ) consists of the elements of all of whose angles lie in .
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and . An action of on a set is amenable (IsAmenableAction G X) when carries a -invariant mean, and extensively amenable (IsExtensivelyAmenable G X) when the finite subsets of carry a -invariant mean that, for each finite , gives full weight to the finite sets containing .
The milestones use further notions, defined precisely in the definitions item and in their own statements:
IsRecurrentAction) when for every symmetric such and every , the induced walk returns to with probability .extend F X) is its extension to an arbitrary set by direct limits, and an action of on gives the semidirect product (FunctorProduct F G X) acting on . The lamplighter case is (Lamplighter G X).wobbling X) of a metric space consists of the permutations of with .The question is open. A proof settles it positively and, through von Neumann's theorem, answers Katok's question in the negative; a disproof shows that is not amenable.
The milestones are results from the literature, stated as their sources state them. From Juschenko–Matte Bon–Monod–de la Salle: is a group (p. 4); Lemmas 2.1 and 2.2 on extensive amenability; Theorem 1.3 and Corollary 1.4, the functorial criterion; Proposition 5.3, that a subgroup of is amenable if and only if its action on is extensively amenable; Proposition 4.1 and Lemma 4.3, the inverted-orbit reformulations; Theorem 4.2, recurrence implies extensive amenability; Lemma 5.2 and Theorems 5.1 and 1.9, amenability in rational rank at most ; and Theorem 1.10, the Liouville dichotomy, with the steps of its proof: Lemma 5.10, Proposition 5.11 with Lemma 5.13 (realizing as the topological full group of a minimal subshift of polynomial complexity), and Matte Bon's theorem for virtually cyclic groups. The external results these proofs cite are milestones too: Kesten's criterion for a graph (Woess, Theorem 10.6), Lyons–Peres Theorem 2.17 on rough embeddings, Pólya's theorem (already proved on the platform as MarkovMixing.polya_recurrence), the Baldi–Lohoué–Peyrière comparison lemma, and Matte Bon's Theorem 1.2 on topological full groups of subshifts of slow complexity. From Juschenko–de la Salle: Theorem 1.4 on the wobbling group, with coarse embeddings defined by non-decreasing control functions.
Garban's question, whether is extensively amenable for every , and Question 1.11 of Juschenko–Matte Bon–Monod–de la Salle, whether a polynomially growing Schreier graph forces extensive amenability, are stated as open milestones. Each comes with a milestone stating that a positive answer implies the goal.
The result. A proof would make a natural amenable group containing, by Juschenko–Monod and Juschenko–Matte Bon–Monod–de la Salle, finitely generated infinite simple amenable groups, and would answer Katok's question. A disproof would give the first non-amenable finitely generated group of interval exchange transformations; by Theorem 1.9 it would have rational rank at least .
Formalizing it. The definitions of extensive amenability, of the functorial semidirect products , of inverted orbits and recurrent actions, and of wobbling groups are reusable beyond this mission, as are the external probabilistic results (Kesten's criterion, rough embeddings and recurrence). Pólya's theorem is already formalized and proved on the platform (MarkovMixing.polya_recurrence). None of the other landmarks is formalized.
Every known amenability proof for subgroups of passes through Proposition 5.3 and then needs extensive amenability of the action on the circle. The available criterion for extensive amenability is recurrence of the Schreier graphs, which embed into lattices with the rational rank; for these graphs can be transient, so recurrence is unavailable. Garban's theorem shows that the natural strengthening of extensive amenability fails for all transient wobbling actions, and Theorem 1.10 shows that the Liouville route fails in rank at least .
is UnitAddCircle, and permutations act on it by evaluation. is defined as the subgroup generated by the interval exchange transformations, so that its group structure needs no proof inside the definitions; a milestone states that nothing else lies in it. The source's precise definition (“a right-continuous permutation of such that the set , called the set of angles of , is finite”) is read together with its opening phrase, “cutting this circle into finitely many intervals”, so the definition also requires finitely many points of discontinuity: without that requirement a right-continuous permutation with two angles can have infinitely many discontinuities, and the cocycle of Proposition 5.3 would not be finitely supported. Means take values in and are normalized to total mass . Random walks have finitely supported step distributions where the sources say “finitely supported”, and probabilities of events of a walk are finite sums over the step sequences. Recurrence of a Markov chain is return to the starting point with probability , expressed through first-return probabilities. Functors are Mathlib functors from the wide subcategory of FintypeCat on the injective maps to GrpCat with amenable values, extended to a set by the filtered colimit over its finite subsets.
The goal admits no trivializing reading: contains the irrational rotations and the non-rotation exchanges, and Garrido.IsAmenable is the standard notion. The external milestones (Kesten, Lyons–Peres, Baldi–Lohoué–Peyrière) are cited results, stated in the form the sources apply; proofs of them are welcome contributions in their own right.
We investigate the relaxation dynamics and steady state of a qubit interacting with a coherent environment through an energy-conserving flip-flop interaction within the Markovian repeated-interaction framework. We derive an exact analytical solution for the evolving and stationary state, nonperturbative in the environmental coherence. We show that environmental coherence provides a resource for dissipative state preparation by expanding the set of accessible steady states. In particular, coherent ancillas can increase the system ground- state population beyond that of the bath, corresponding to an effective temperature below the bath temperature, and enhance its steady-state purity, with these effects controlled by the interplay between the system energy scale and the system-ancilla coupling. Nevertheless, we prove that the purity of the system can never exceed the purity of the ancilla. We further analyze the thermodynamics of the protocol and show that environmental coherence can modify and even reverse the natural direction of heat transfer, giving rise to anomalous heat flow. Remarkably, for fixed interaction parameters, the direction of the coherence-induced heat transfer is governed by the relative phase between the system and ancilla coherence, whereas their magnitudes determine the amount of heat exchanged. Our results establish environmental coherence as a resource for controlling steady-state preparation and energy transfer in repeated-interaction dynamics. △ Less
This mission is the statement-level formalization of Coherence-assisted quantum state preparation and thermal control through repeated interactions (arXiv:2610.10794v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stationary purity is capped by ancilla purity (Abstract; §III B Eq.(26); Appendix D: ancilla purity cap, PDF p. 19). 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Can entangled noise erase entanglement more efficiently than separable noise? Standard robustness restricts the added noise to separable states; generalized robustness allows any state. We prove that the two costs coincide for every two-qubit state and give an explicit full-rank qubit--qutrit state with a strict gap. Positivity under partial transpose (PPT) characterizes separability in both dimensions, so the boundary is not caused by a failure of the PPT criterion. Instead, product-vector geometry permits a rank-one bridge between the two-qubit dual optimizations and supplies a two-dimensional completely entangled subspace for the qubit--qutrit separation. Local isometric embeddings complete the finite-dimensional bipartite classification, also for any fixed multipartite cut. Combined with known three-qubit separation, the result classifies universal equality relative to full separability in all finite multipartite systems. △ Less
This mission is the statement-level formalization of The Minimal Dimension of Entangled-Noise Advantage (arXiv:2609.28367v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
45 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main-text Theorem 1; seed announced in abstract (Main-text Theorem 1; seed announced in abstract, PDF p. 1). 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.