Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In information design (Bayesian persuasion), a designer commits to a signal about an unknown state, and every signal induces a distribution over the receiver's posterior beliefs. Kamenica and Gentzkow (2011) showed that the distributions a signal can induce are exactly the Bayes-plausible ones, those whose mean posterior is the prior, and that the designer's optimal value is the concave hull (concavification) of the designer's objective, evaluated at the prior. This reduces the design problem to a computation in convex analysis, and it is the basic tool of the information design literature.
Many applications add constraints on the distribution of posteriors: a capacity or cost constraint on information (rational inattention), participation or incentive constraints when the designer is a mechanism designer with limited commitment, or a bound on the probability of a given action. Le Treust and Tomala (2019) treated one inequality constraint for finitely supported distributions. Doval and Skreta (arXiv:1811.03588v3, Mathematics of Operations Research, 2024) allow any finite number of inequality and equality constraints, and an arbitrary Borel distribution over posteriors. Their first main result, Theorem 3.1, shows that the value is still a concave hull, of a function of more variables.
Let be a finite set of states and the simplex of beliefs. The data are measurable functions on : an objective , inequality constraint functions and equality constraint functions , with .
For a prior , is the set of Borel probability measures on with mean . The constrained information design problem (CID) at a parameter , , is
component-wise, with when no is feasible. The feasibility set (Definition 2.2) is the set of at which (CID) is feasible.
The pointwise set collects the parameters at which the constraints hold for the degenerate distribution at . The modified objective (3.1) is
equal to on and off . For a function on , the hypograph is and the concave hull (Definition 2.1) is
In the Lean development these are IsBayesPlausible, IsConstraintFeasible, value, feasibleSet, pointwiseSet, modObj, hypo and cav, in the namespace ConstrInfoDesign.Cav.
For every ,
The statement fixes no constants and assumes nothing beyond measurability; it covers infeasible parameters, where both sides are , and unbounded objectives, where both sides may be .
Theorem 3.1 gives the value function of (CID) in closed form as a single concave hull. Its consequences in the paper are a bound on the number of posteriors an optimal design needs (Corollary 3.1), a refinement to with binding constraints (Corollary 3.2), and, combined with Lagrangian duality, the characterization of optimal designs in applications such as mechanism design with limited commitment and persuasion of a privately informed receiver. The result also explains when the feasibility set is the convex hull of the pointwise set (Lemma A.1), which is the geometric reason the constrained problem behaves like an unconstrained one in coordinates.
The result is proved in the paper; to the best of current knowledge none of it is formalized. Mathlib has convex hulls, Carathéodory's theorem, measures, supports and Bochner integrals, but neither the concavification theorem of Kamenica and Gentzkow nor the Rubin–Wesler theorem that the mean of an integrable random vector lies in the convex hull (not only its closure) of a set carrying it. A complete development would give machine-checked versions of both, reusable by any formalization of Bayesian persuasion with finitely many states.
The obvious argument for says that the mean of the vector under lies in the convex hull of its range. Mathlib's tools (Convex.integral_mem) only give membership in a closed convex set, and the range of an integrable, possibly unbounded and discontinuous is not closed; the closure gives the concave closure of , which differs from the concave hull on the boundary of its domain (Example D.1 of the paper). The Rubin–Wesler theorem closes this gap, but it needs its own argument by induction on dimension.
In Proposition A.2, Carathéodory's theorem in gives points of the hypograph; the claimed bound needs the extra observation that a point of the hypograph can be moved up to the graph. The remaining steps are bookkeeping in the extended reals: shifting thresholds so that each point of a convex combination lies in , and approximation arguments when the suprema are infinite.
States are Fin N; beliefs are points of Fin N → ℝ and is stdSimplex ℝ (Fin N). The parameter space is the product (Fin N → ℝ) × ((Fin I → ℝ) × (Fin E → ℝ)). The functions , are total on Fin N → ℝ; their values off the simplex never matter. A distribution over posteriors is a Borel probability measure on Fin N → ℝ that gives the complement of the simplex measure zero, and its mean is the Bochner integral of the identity.
Conventions committed to:
EReal; suprema are sSup in EReal, so the empty supremum is .Trivializing formalizations are ruled out: is not taken over finitely supported distributions only (which would make Proposition A.1 empty), cav is Definition 2.1 and not the sum formula of Proposition A.2, is Definition 2.2 and not , integrals of non-integrable maps are excluded rather than counted as , and no supremum is taken in .
The development needs the Rubin–Wesler theorem in finite dimensions, a Carathéodory variant for hypographs, and the finite-dimensional facts that a measure on a second-countable space is carried by its support and that finite sums of Dirac masses are probability measures with the expected integrals. The Rubin–Wesler theorem and Proposition A.2 are reusable beyond this mission. Proofs of the milestones and of the goal, and alternative arguments, are welcome.
Passive funds hold a market index rather than selecting individual stocks. In the model of Baruch and Zhang (2022), this difference matters for what prices reveal. An investor who studies individual stocks can bring information about their payoffs into trading; an investor restricted to the market portfolio cannot make the same stock-by-stock trades. The paper asks how the mix of these investors changes the information about future asset payoffs that can be inferred from market prices. Its answer separates the market portfolio from every other stock portfolio: indexing preserves the former's price efficiency while reducing the latter's, at an increasing rate. This mission targets that price-efficiency result, Theorem 3 on p. 6226.
The question matters to asset-pricing models that use prices as information. A price can be informative even when it is affected by many other forces; here the paper gives a controlled Gaussian economy in which the effect of replacing active investors with indexers can be isolated. The target is a theorem about conditional variances, not an empirical estimate of the effect of real index funds. The equilibrium interpretation comes from the paper's earlier price construction; the formal statements here use the public statistic that the paper proves equivalent for this purpose (15)–(16), p. 6224.
There are risky assets and investors. The random payoff vector is , with multivariate normal law . Investor sees a private signal , where . The payoff and all noise vectors are mutually independent, and the two covariance matrices are positive definite. A stock portfolio pays . The all-ones vector is the market portfolio. These are the assumptions and terms introduced in §2, p. 6221.
The investors are partitioned into indexers , who hold the market portfolio, and nonindexers . Both kinds are present: , with p. 6222. Equation (3) sets . Equation (4) combines the nonindexers' average signal and a scalar statistic of all signals into the public statistic
The first component has coordinates; the second has one. The paper identifies the conditional variance given this statistic with the variance given equilibrium prices (16), p. 6224. In this mission, means the conditional variance of given . It is initially a random variable, and equation (20) asserts that it is almost surely a deterministic matrix expression under the Gaussian model.
The goal is Theorem 3, p. 6226, stated for all admissible nonindexer sets on the same probability space. For any real , market-portfolio multiples have unchanged conditional variance:
For every other portfolio, fewer nonindexers, equivalently more indexers, strictly raise conditional variance. The rate also grows: whenever and ,
The six milestones are the identities and statements used in the paper's development: the cross-covariance in (7), the covariance of in (8), Gaussian conditioning in (20), the characterization of market portfolios in Lemma 2, the first derivative in (21), and the second-derivative conclusion in §6.1, p. 6227. They make the model-to-goal path explicit without changing the goal's three clauses.
The result specifies which price information survives a shift toward passive investing in this economy. It says that market-portfolio payoff information is preserved while information about every portfolio outside the span of is lost, with an accelerating loss across successive increases in indexer count. The distinction is used later in the paper to discuss asset-price comovement and a conditional CAPM measure §6.2–6.3, pp. 6227–6228.
Baruch and Zhang proved the theorem in 2022. The formalization work is to represent their Gaussian model, its public statistic, the conditional-variance identity, and the comparative-statics claims in Lean, then supply machine-checked proofs. The current proposal contains checked statements and definitions with open theorem proofs; it does not claim that those proofs already exist. The model interface and covariance identities could also support later formalizations of the paper's price and comovement results.
The target compares conditional variances arising from different information sets. Their equality or ordering cannot be read directly from the definitions of conditional expectation. The Gaussian assumption turns the conditional variance into a matrix expression, but the derivation must preserve the dependence structure of all signals and the special scalar coordinate of . The boundary makes redundant and its covariance singular, so the inverse formula requires the paper's standing condition that both investor types are present.
The rate claim requires more than the sign of the first derivative. The printed second-derivative argument on p. 6227 omits the minus sign in the derivative of a matrix inverse; the nonnegativity conclusion survives, but its formal statement records the corrected derivative value. The strict increasing-rate clause in the goal is stronger than the non-strict inequality displayed in that proof. These distinctions must be established for every portfolio outside the market span, including edge dimensions, rather than inferred from a numerical example.
Assets are indexed by Fin n and investors by Fin m, both starting at zero. The final coordinate of is represented by the Unit side of Fin n ⊕ Unit. Mathlib's multivariate Gaussian law lives on a Euclidean space; a SignalModel bundles the Gaussian laws, positive definiteness, mutual independence, and measurability of payoffs and noises. Joint normality follows from these model assumptions. The measurability fields ensure that is a sub-σ-algebra of the ambient one.
The conditional variance in the goal is Mathlib's conditional variance of given , compared almost surely across choices of . It is not defined by the Schur-complement formula: milestone (20) asserts that identity. The matrix and the coefficients in (19) use a real variable in the derivative milestones, extending the integer count used by the economy. Positive definiteness and rule out the junk inverse and zero-denominator cases. The strict discrete-increment statement expresses “increasing rate” in the goal.
The equilibrium prices and their equivalence with in (16), Theorems 1–2, and the later comovement and CAPM results are outside this mission. Contributions are welcome on Gaussian conditioning, covariance identities, matrix inverse differentiation, and the comparison of successive portfolio variances. General Gaussian and matrix lemmas can be reused beyond this paper.
Linear perturbations of a rotating, charged black hole are governed, after a mode decomposition, by a coupled first-order system for the linearised Weyl and Maxwell quantities. For the uncharged Kerr solution these equations decouple into the Teukolsky equation, and mode stability was proved by Whiting (1989) through an integral transform. For the charged Kerr–Newman family the Weyl and Maxwell perturbations stay coupled, and no separation of variables was available for decades; Giorgi (2020, arXiv:2002.07228) obtained coupled Teukolsky-type and Regge–Wheeler-type systems but not a separated form. Hintz (2026, arXiv:2609.33661) found a matrix integrating factor that removes the same-chirality coefficient A from the first-order derivatives and makes the remaining coefficient matrix split into a radial and an angular part; from this he derives separation of variables and mode stability for subextremal Kerr–Newman black holes. The algebraic core of that derivation is a chain of explicit, local, coordinate-level transformations between first-order systems on the exterior region. This mission formalises that chain.
Prior formalised material on this platform: the Boyer–Lindquist Kerr vacuum certificate and the Exact Vacuum Atlas I/II coordinate certificates and transports (same author, same environment). None of them touch perturbation theory; this mission starts a new, independent layer and does not depend on them.
Fix subextremal Kerr–Newman parameters , , with (Lean: Hintz2026.SubextremalKN). Put , , and work on the open set
(Lean: U p, with x 0 = r, x 1 = θ). Write , . Fix a frequency and an azimuthal number (kept real in Lean; integrality is not used by any statement here), and put , .
The first-order operators of the Newman–Penrose formalism in these coordinates are, for a label ,
with daggers obtained by , . Partial derivatives are coordinate-slice derivatives (Lean: cpd), and all fields are complex-valued functions on that are on .
System (1) (positive spin) is the system (1a)–(1d) of Hintz for the four rescaled mode quantities ; the negative-spin system is obtained from it by the replacement rules stated in the paper (Lean: res1a–res1d, res1aN–res1dN, each the difference "left side minus right side"). The chiral variables (3) are
System (4) is with the explicit matrices , and scalar of the paper (Lean: A, Bmat, cscalar; is the spin label). The integrating factor is the matrix of equation (5), with , and system (7) is
for , and . The paper's separation statement is that with four explicit coefficient functions .
for both spins (Lean: Hintz2026.main_pos, Hintz2026.main_neg, with the on- forms main_pos_on_U, main_neg_on_U). The composite transformation is explicitly invertible on : first recover and , then apply the inverse chiral map invPos or invNeg. The goal leaves the frequency and azimuthal parameters free, assumes nothing beyond subextremality and regularity on , and does not assert anything at the horizon or at infinity.
Dminus_X_eq_AX, Dplus_XstarInv_eq).Dm_Xv_sub_AXv, Dp_Yv_add_AYv, Dm_zero_iff_Xv_residual_zero_on_U, …).Cmat_eq_Csep), and .system4_iff_system7).ident_*, identN_*), and the equivalence (1) ⟺ (4) (sys1_iff_sys4_pos, sys1_iff_sys4_neg).The chain (1)→(4)→(7) is the step on which the rest of Hintz's argument rests: once is known to separate, the angular operator can be diagonalised and the radial problem reduces to a scalar second-order equation, which is where the mode-stability argument lives. The transformations are algebraic but far from trivial to check by hand — each entry of is a rational-trigonometric expression in , , , and the three parameters, and the cancellation of all mixed terms is the content of the separation claim.
Everything in this mission is already proved in the paper. What the mission adds is a machine-checked verification of the explicit coefficient data and of the transformation identities for arbitrary fields, with the regularity and domain hypotheses made explicit. All targets listed here already carry accepted proofs on this platform; the mission records them as a public, reviewable dependency tree. Not formalised here: the derivation of (1) from the Einstein–Maxwell equations, the angular eigenvalue problem, the radial reduction, the Whiting-type transform, and mode stability itself.
The naive approach — substituting the chiral variables into (4) and comparing with (1) term by term — produces hundreds of rational terms with half-integer powers of and of . The first-order terms match by construction; the difficulty is that the zeroth-order terms only match after using , and the specific values of , , . A second trap is in the negative-spin system: the replacement rules put sign changes inside the operators, and an identity proved for a "simplified" version of the rules would be an identity about a different system. The formalisation keeps the rules literally and derives linearity separately.
Coordinates are with , ; no manifold, tetrad or spacetime object is defined. Derivatives are coordinate-slice derivatives (deriv along one coordinate), and the final unknown-field interfaces use ContDiffOn ℝ ∞ _ (U p); auxiliary statements may require only coordinate-slice differentiability, and explicit coefficient statements retain the stronger analytic order ω. Real exponents , are Real.rpow; is Real.sqrt. All coefficient matrices are explicit Matrix (Fin 2) (Fin 2) ℂ; the separated form is an independent explicit definition, not derived from , so Cmat_eq_Csep is a genuine check. The spin label is a real parameter in the definitions of and ; the two spins are the instances , each proved separately with its own chiral variables.
Nothing here is vacuous: the systems are Props about arbitrary fields, the residuals are explicit, and the domain is nonempty and open. A reader can check that the Lean definitions reproduce the paper's formulas from the transcript of the paper's equations included with the source.
Reusable beyond this mission: the slice-derivative calculus (cpd, Dm, Dp, product and sum rules), the integrating-factor layer (X, A, invertibility, residual identities) and the prefactor calculus for .
A neural network can change its behavior substantially when both its width and its training duration grow. For a network with two hidden layers, the parameters of the layers interact during training, so a large-width description must account for the output of the actual optimization algorithm. Sirignano and Spiliopoulos study this question for online stochastic gradient descent (SGD) under a mean-field normalization. Their Theorem 2.3 identifies the limit of the trained network when the first hidden layer grows, followed by the second, and gives a rate for the intermediate second-layer approximation. The result concerns a trained network: all three families of weights evolve at every SGD step.
The normalization matters. Each hidden layer contributes an average, with factors and for the first and second widths. The learning rates depend on those widths, so the output can continue changing on the time scale of SGD steps. The paper notes that a different scaling may lead to a different limiting equation or to no nontrivial training behavior at large width. A precise statement therefore needs the finite network and its SGD updates alongside the limiting equations, not merely a claim about an abstract mean-field flow.
Let be an input dimension and an input. A two-hidden-layer network has first-layer units and second-layer units. Its parameters are output weights , first-layer vectors , and second-layer weights . With an activation , its output is
Training samples are independent draws from a probability law supported on a compact product . The three initial weight families are mutually independent and identically distributed within each family, with laws , , and . Each law has a continuous density and compact support. The activation is twice continuously differentiable and, as the paper's notation requires, it and its first two derivatives are bounded. These are the standing conditions of Assumption 2.1.
At each step, SGD updates all parameters from the same previous parameter state and the same sample. The learning rates in equation (2.1) are , , and , applied with the step-size denominators in equation (1.4). The output at time is the output after updates. For fixed , the first-width limit is described by an -particle system. Its first-layer particle retains both its initial first-layer vector and the full vector of its second-layer initial weights, because its dynamics depend on all of them. The second-width limit is a limiting integro-differential system for representative paths , , and .
For and , the target is the existence and uniqueness of the limiting system (2.6), together with
The order is fixed: grows first while is held fixed. The goal states the entire Theorem 2.3, including the existence clause; without existence, convergence quantified only over solutions would have no content.
For the particle output , the same theorem gives a constant such that
The attack path records the finite-particle well-posedness of Lemma A.5; the first-width output limit stated after Lemma 2.2; the uniform particle bound (5.5); the sampling-variance estimate (5.9); the mean squared particle-error estimate (5.15); the output rate from Section 5.8; and uniqueness from Lemma 6.1. Each is a stated result or displayed assertion in the source. The rate and uniqueness milestones are also conclusions of the goal theorem.
The theorem specifies what the output of this trained network approaches, rather than only describing the parameters of a network at initialization. It connects the discrete SGD recursion to a finite particle system and then to a deterministic output from a limiting system. The bound makes the second-width approximation quantitative, while uniqueness makes the limiting output independent of the choice of representative solution. These claims provide the basis for the paper's later discussion of global convergence under stronger assumptions; they do not themselves assert that training reaches a global minimum.
The paper proves the first-width and error estimates and gives a uniqueness argument for the limiting system. It asserts existence of a solution to (2.6) in Theorem 2.3, although a separate existence proof is not supplied there. A complete machine-checked development must account for that clause as well as the known arguments. No proof of this mission's goal or milestones is currently included in the draft Lean statements; they are targets for solvers. The network model, initialization law, and particle equations can also serve as reusable interfaces for further formal work on trained wide networks.
A direct large-width argument cannot treat the two widths as one undifferentiated limit. With fixed, the shared first-layer weights couple all second-layer units. The first limit is a stochastic statement about the SGD iterates and a particle system whose state includes a vector of initial second-layer weights. Only after that limit can the fluctuations be controlled. The second stage must bound both the sampling fluctuation of the representative output and the discrepancy between the particle paths and the limiting paths. The source's existence assertion also needs a mathematical justification in the specified continuous-solution class. Simply taking a pointwise limit of the network formula leaves all of these issues unresolved.
Lean uses EuclideanSpace ℝ (Fin d) for inputs, Fin N_1 and Fin N_2 for neuron indices, and Measure.pi or Measure.infinitePi for independent initial weights and data. The arrays of all widths live on one probability space with the stated product law. The SGD recursion is the simultaneous update (1.4), with the exact factors from (2.1), and time uses . The representative and particle systems are written in integral form. Solutions are jointly continuous on times the compact supports of their initial states; this supplies the regularity needed for the integrals and matches the class used in Lemma 6.1. No nonempty-input-set assumption or monotonicity assumption on is added.
The inner probability limit in the goal uses a limsup in . Footnote 2 writes an inner limit but does not assert its existence at every probability threshold; the limsup version implies its claim whenever that inner limit exists. A single rate constant works for all , all positive , and all . The particle state includes the full vector of initial values, and the conditional expectation defining its second-layer preactivation is an integral over their product law at fixed initial values. The finite network, particle system, and limiting system must be connected by the stated results; an arbitrary output function with the desired limit would not formalize this theorem.
A complete development needs probability measures on product spaces, integrals of continuous functions on compact supports, convergence in measure, finite-sample variance estimates, and existence and uniqueness theory for the coupled integral systems. Contributions to these pieces and to the stated milestone theorems are within scope. The measure-valued Skorokhod-space statement of Lemma 2.2, numerical experiments, and the paper's separate global-convergence theorem are outside this mission.
We formalize the task of unitary Schur sampling -- an extension of weak Schur sampling -- which is the process of measuring the Young label and the unitary group register of an input qudit state. Intuitively, this task is equivalent to applying the Schur transform, projecting onto the isotypic subspaces of the unitary and symmetric groups indexed by the Young labels, and discarding of the permutation register. As such unitary Schur sampling is the natural task in processes such as quantum state tomography or spectrum estimation. We generalize this task to unitary mixed Schur sampling to account for the recently introduced mixed Schur-Weyl transform. We provide a streaming algorithm which achieves an exponential reduction in the memory complexity and a polynomial reduction in the gate complexity over na"ive algorithms for the task of unitary (mixed) Schur sampling. Further, we show that if the input state has limited rank, the gate and memory complexities of our streaming algorithm as well as the algorithms for the full Schur and mixed Schur transforms are further reduced. Our work generalizes and improves on the results in arXiv2309.11947.
This mission is the statement-level formalization of A memory and gate efficient algorithm for unitary mixed Schur sampling (arXiv:2410.15793v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Four properties of homogeneous Littlewood–Richardson coefficients (Lemma 11, PDF p. 32). 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We study and solve the problem of distilling secret key from quantum states representing correlation between two parties (Alice and Bob) and an eavesdropper (Eve) via one-way public discussion: we prove a coding theorem to achieve the "wire-tapper" bound, the difference of the mutual information Alice-Bob and that of Alice-Eve, for so-called cqq-correlations, via one-way public communication. This result yields information--theoretic formulas for the distillable secret key, giving ``ultimate'' key rate bounds if Eve is assumed to possess a purification of Alice and Bob's joint state. Specialising our protocol somewhat and making it coherent leads us to a protocol of entanglement distillation via one-way LOCC (local operations and classical communication) which is asymptotically optimal: in fact we prove the so-called "hashing inequality" which says that the coherent information (i.e., the negative conditional von Neumann entropy) is an achievable EPR rate. This result is well--known to imply a whole set of distillation and capacity formulas which we briefly review.
This mission is the statement-level formalization of Distillation of secret key and entanglement from quantum states (arXiv:quant-ph/0306078v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: one-way secret-key coding theorem (Theorem 1, 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.
We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon , one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available. Approximation error must vanish against arbitrary adaptive users with quantum memory and references. Writing for the bath dimension rate and for the actual initial entropy rate, we prove that the achievable region is exactly , and . Here is maximum entropy exchange and is a smoothed independent-reference extension cost, with the zero-error limit taken before the supremum over full-rank inputs. Its exact fixed-input form is an affine transform of the zero-leakage quantum privacy funnel. The minimum dimension rate is . The proof combines entropy converses, a bath-dimension-independent support repair, and a closed adaptive implementation of encoder-only fully quantum Slepian--Wolf recycling. All seeds, clocks, workspace and retained residues are counted. Worked examples include dephasing, pure replacement and a qubit channel with . No computability of or efficient circuit synthesis is claimed. △ Less
This mission is the statement-level formalization of Bath dimension and initial entropy for closed repeated use of a quantum channel (arXiv:2609.18267v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: uniform collision gain (Theorem 3.1, PDF p. 6). 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we fill the gap in previous works by proving the formula for entanglement-assisted capacity of quantum channel with additive constraint (such as bosonic Gaussian channel). The main tools are the coding theorem for classical-quantum constrained channels and a finite dimensional approximation of the input density operators for entanglement-assisted capacity. The new version contains improved formulation of sufficient conditions under which suprema in the capacity formulas are attained.
This mission is the statement-level formalization of Entanglement-assisted capacity of constrained quantum channel (arXiv:quant-ph/0211170v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trace-norm compactness of an energy sublevel (§3, unnumbered Lemma (proof on PDF p.11), PDF p. 10). 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
The Schur transform, which block-diagonalizes the tensor representation of the unitary group on qudits, is an important primitive in quantum information and theoretical physics. We give a generalization of its quantum circuit implementation due to Bacon, Chuang, and Harrow (SODA 2007) to the case of mixed tensor , where is the dual representation. This representation is the symmetry of unitary-equivariant channels, which find various applications in quantum majority vote, multiport-based teleportation, asymmetric state cloning, black-box unitary transformations, etc. The "mixed" Schur transform contains several natural extensions of the representation theory used in the Schur transform, in which the main ingredient is a duality between the mixed tensor representations and the walled Brauer algebra. Another element is an efficient implementation of a "dual" Clebsch-Gordan transform for . The overall circuit has complexity . Finally, we show how the mixed Schur transform enables efficient implementation of unitary-equivariant channels in various settings and discuss other potential applications, including an extension of permutational quantum computing that includes partial transposes.
This mission is the statement-level formalization of The mixed Schur transform: efficient quantum circuit and applications (arXiv:2310.01613v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-input conclusive teleportation: exact success and corrected output (Section 5.1.1: two-input conclusive teleportation success, PDF p. 29). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The maximum rates for reliably transmitting classical information over Bosonic multiple-access channels (MACs) are derived when the transmitters are restricted to coherent-state encodings. Inner and outer bounds for the ultimate capacity region of the Bosonic MAC are also presented. It is shown that the sum-rate upper bound is achievable with a coherent-state encoding and that the entire region is asymptotically achievable in the limit of large mean input photon numbers.
This mission is the statement-level formalization of Multiple-Access Bosonic Communications (arXiv:quant-ph/0506171v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational homodyne and heterodyne coherent-state MAC regions (§II.B, (5)–(8): single-mode homodyne/heterodyne capacity regions, 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball under the extra hypothesis that the inverse map is continuous; the project's earlier results, all unpublished, covered c₀(Γ) itself without that hypothesis (the earlier c0 mission), smooth strictly convex blocks of any finite dimension and strictly convex planes, with scalars beside them, ℓ¹ₙ blocks of bounded dimension, and polygonal planes, also beside discs. This mission formalizes a proof that the closed unit ball of every c₀ sum of real spaces of dimension at most two is plastic, for arbitrary index sets and arbitrary norms on the blocks, together with the two-space statement that every nonexpansive bijection between the balls of two such sums is an isometry. The results come from an unpublished research project on the plasticity problem.
For a family of real normed spaces, the sum consists of the families with and along the cofinite filter, with the norm . Its closed unit ball is . The blocks here have dimension at most two: zero, the real line, or a real plane with any norm, whose unit ball may be a parallelogram, a polygon, a disc, or have flat edges and curved arcs in any combination, with no uniformity over .
For finite index sets the balls are finite-dimensional, and both statements are covered by Zavarzina's theorem for finite-dimensional targets (Ann. Funct. Anal. 9 (2018), Theorem 3.8); the content is the infinite case.
The result. It settles plasticity for all c₀ sums of blocks of dimension at most two. It gives the first infinite c₀ sums in which scalar coordinates sit beside polygons or other planes that are not strictly convex, and the first non-polygonal planes that are not strictly convex (a curved ball with two edges meeting at a corner, or with countably many extreme points). Its proof shows that nonexpansive bijections between such balls are block-diagonal linear isometries, with scalar blocks going to scalar blocks after each parallelogram plane is split into two scalar coordinates.
Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. Known inputs available in this environment through earlier missions are invariance of domain, the Freudenthal–Hurewicz theorem and Brouwer's fixed-point theorem; Baire's theorem, Krein–Milman and Mazur–Ulam are in Mathlib.
For infinite index sets the ball is not compact, its unit sphere has large flat faces, and no regularity of the inverse map is assumed. The planar geometry is the bulk: covers of a planar ball by three translates near corners where two edges meet, an extreme lens and a far-comparison estimate at extreme points where the norm is curved, and the linearization of an extreme-point correspondence between two different planes from a single radial inequality. The c₀ part must match blocks, exclude scalar coordinates that feed planar blocks, and exclude the collapse of a block by a two-lift argument.
Real scalars, arbitrary index sets (no countability or nonemptiness assumed), arbitrary norms on the blocks.
The sum is Mathlib's lp E ⊤; the c₀ sum is the submodule c0Sum E of it (definition Plasticity_C0Sum), with its subspace norm.
"Dimension at most two" is Module.rank ℝ (E i) ≤ 2, which excludes infinite-dimensional blocks.
The goal uses HasPlasticUnitBall (definitions Plasticity_Basic); the two-space theorem is stated for functions between the subtypes Metric.closedBall (0 : c0Sum E) 1, with LipschitzWith 1 and Function.Bijective.
Extremal graph counterexamples, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
Write for the maximum number of edges in an -vertex simple graph containing no subgraph copy of , with value if there is no eligible graph; a copy is an injective edge-preserving map and need not be induced. For a finite family of finite simple graphs, each encoded on for its own , let be the maximum edge count over simple graphs on containing no copy of any member of , again taking for an empty collection. There exist a nonempty such family and real constants such that every member is connected, bipartite, and not acyclic; for each , for all sufficiently large natural , with a threshold that may depend on ; for every and every simple graph on containing no copy of any member, ; and for every , . These last two bounds use the same and include . The conclusions also include and , as equalities and inequalities of real numbers. No member and real constant satisfy for all sufficiently large . Moreover, the assertion that every nonempty finite family of finite simple graphs whose members each contain a cycle admits such a member and constant is false.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, J_CompactnessConjecture.json, J_TwoDegenerateGraphs.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Multicolor triangle Ramsey numbers, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For each , let be the infimum in of the integers such that every labeling of the edges of the complete simple graph on by colors has a monochromatic triangle; equivalently, no such labeling has every color graph free of a three-vertex clique. This is the least such when the set is nonempty, with infimum for an empty set. Both of the following hold: for every integer , , where all quantities in the inequality are real; and as , meaning that for each real there is such that whenever . The root sequence is defined also at using real division , so that term equals and does not affect the limit.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, I_MulticolorTriangleRamsey.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Ehrhart volume inequality, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
Let be any positive natural number and any convex compact set with nonempty interior. Write for its Lebesgue measure converted from to a real number, and define its barycenter as . The conversion sends infinite measure to zero and real inversion is total, but these hypotheses make finite and positive. If this barycenter is the zero vector and , then . The lattice condition says both that the origin lies in the interior and that no other integer vector does. The volume in this inequality is the real Lebesgue volume itself.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, F_EhrhartVolumeInequality.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Hardness of the closest vector problem, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every Boolean language of finite bit strings for which there exist a polynomial and a deterministic polynomial-time Boolean verifier satisfying if and only if there is a bit-string certificate with and , there exists a total deterministic polynomial-time map on bit strings sending every with into the following YES set and every with into the following NO set. An instance consists of a natural dimension , an integer matrix with , a target all of whose coordinates are integers, and a rational radius . It is in YES exactly when some satisfies , and in NO exactly when every satisfies . The sets consist of the exact encoded instance strings, formed by concatenating the encodings of , , the target coordinates in order, and the matrix entries in row-major order. Each scalar is encoded by taking its library natural-number code, applying the library's natural-number-to-bit-string encoding to get a word , and prefixing with true bits followed by one false bit. Strings without such a valid encoded instance, and instances satisfying neither distance condition, are outside both sets; dimension one is included. Polynomial time is witnessed in the library's TM2 machine model, using its product encoding of Boolean lists for verifier input, its Boolean output encoding for the verifier, and identity encodings for the reduction's input and output.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, H_GapCVP.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Arithmetic formula lower bounds for the permanent, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every natural number and every finite arithmetic formula whose leaves are variables , , or arbitrary complex constants and whose binary operations are addition, subtraction, multiplication, and division, assume that every divisor subformula evaluates to a nonzero element of the fraction field of and that the value of in this fraction field equals the polynomial under the canonical inclusion. Then the number of variable-leaf occurrences satisfies , with both sides viewed as real numbers. Repeated occurrences are counted separately, constants contribute zero, and the leaves of both operands of each operation, including division, are counted. Nonzero divisors are required as rational functions, not at every numerical substitution.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, C_PermanentFormulaLowerBound.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Counterexamples to Connes rigidity, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
There exist a countable group and a sequence of countable groups , indexed also at , such that all of them are finitely generated and infinite, every conjugacy class of a nonidentity element in each such group is infinite, and every such group has property T. For every , is isomorphic to as specified below, and for every , including , is isomorphic to in the same sense. If , there is no group isomorphism , and for every there is no group isomorphism . For each group concerned, property T means that, for every complete complex inner-product space and every homomorphism , if for every finite and every real there is a vector with and for all , then there is a nonzero vector fixed by every . Here is the double commutant, inside the bounded complex-linear operators on , of the left translations , and . An asserted isomorphism of these tracial algebras is a complex -algebra equivalence preserving such that both it and its inverse preserve every existing supremum of any set of self-adjoint idempotents, with projection order defined by .
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, E_ConnesRigidity.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
A finitely presented non-sofic group, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
There exist a set and a group structure on such that has a finite presentation and is not sofic in the following precise sense: there are a finite subset and a real number for which no positive integer and map with simultaneously satisfy for every and for every with . Here is normalized Hamming distance; is defined on all of and is not assumed to be a homomorphism. The finite subsets in the defining sofic approximation property include the empty subset, and the permutation sets are required to be nonempty.
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, D_NonSoficGroup.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Binary and spherical codes, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every real with , the following strict inequality holds. Write , with the total-real logarithm convention . Let be the maximum cardinality of a finite subset of in which every two distinct words differ in at least coordinates, and put . Empty codes are permitted in the maximum; the sequence term is zero by total real division. Define and , a real infimum. Then .
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, B_BinaryCodes.json, B_SphericalCodes.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
High-dimensional sphere packing, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For each natural number , let consist of complex-valued Schwartz functions on Euclidean whose values and Fourier-transform values are real, with for every , , and whenever ; radiality is not required. Put , , and , where the infimum is taken in . Put , , and . The assertion is the conjunction of the following ten claims: ; there exists a real sequence such that for every ; ; ; there exists a real sequence such that for all sufficiently large ; there exists a real sequence , nonnegative for every natural , such that for all sufficiently large and every , ; ; ; ; and there exists a real sequence such that for all sufficiently large . Each limit is along natural dimensions tending to infinity, and the four existentially quantified error sequences need not coincide. The sequences are defined also at using total real operations, in particular and division by zero equal to zero; the displayed powers denote those real powers.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, A_SpherePacking.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
In this paper we study the subset of generalized quantum measurements on finite dimensional systems known as local operations and classical communication (LOCC). While LOCC emerges as the natural class of operations in many important quantum information tasks, its mathematical structure is complex and difficult to characterize. Here we provide a precise description of LOCC and related operational classes in terms of quantum instruments. Our formalism captures both finite round protocols as well as those that utilize an unbounded number of communication rounds. While the set of LOCC is not topologically closed, we show that finite round LOCC constitutes a compact subset of quantum operations. Additionally we show the existence of an open ball around the completely depolarizing map that consists entirely of LOCC implementable maps. Finally, we demonstrate a two-qubit map whose action can be approached arbitrarily close using LOCC, but nevertheless cannot be implemented perfectly.
This mission is the statement-level formalization of Everything You Always Wanted to Know About LOCC (But Were Afraid to Ask) (arXiv:1210.4583v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is An explicit two-qubit instrument in the closure of LOCC but outside LOCC (Abstract; §§4.1,4.3, Eqs.(10)–(12), 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
In view of controlling finite dimensional open quantum systems, we provide a unified Lie-semigroup framework describing the structure of completely positive trace-preserving maps. It allows (i) to identify the Kossakowski-Lindblad generators as the Lie wedge of a subsemigroup, (ii) to link properties of Lie semigroups such as divisibility with Markov properties of quantum channels, and (iii) to characterise reachable sets and controllability in open systems. We elucidate when time-optimal controls derived for the analogous closed system already give good fidelities in open systems and when a more detailed knowledge of the open system (e.g., in terms of the parameters of its Kossakowski-Lindblad master equation) is actually required for state-of-the-art optimal-control algorithms. -- As an outlook, we sketch the structure of a new, potentially more efficient numerical approach explicitly making use of the corresponding Lie wedge.
This mission is the statement-level formalization of Lie-Semigroup Structures for Reachability and Control of Open Quantum Systems (arXiv:0811.3906v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The generated Markovian semigroup has the full channel tangent wedge (Theorem III.3, PDF p. 8). 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.
30 results of the paper are not stated yet, because the library lacks an interface they need:
The classical capacity of a noisy optical channel is the maximum rate at which information can be transmitted reliably, given a constraint on the mean input energy. For the ubiquitous bosonic Gaussian channels, which include standard models of loss and noise in fibre and free-space optical links, determining this rate requires addressing whether entanglement between channel uses or non-Gaussian signals can outperform Gaussian encodings. More precisely, the question is whether the energy-constrained Holevo information is additive across arbitrarily many channel uses and coincides with its Gaussian counterpart. We answer these fundamental questions in the affirmative for every single-mode bosonic Gaussian channel at every input energy. Namely, we prove that independently prepared Gaussian states with Gaussian-distributed random displacements achieve the capacity, including in the low-energy regime where squeezing the signals competes with encoding information in their displacement. Our proof connects an entanglement inequality to a sharp, additive lower bound on output entropy. We then characterise communication above capacity: under a strict total photon-number cutoff, the probability of correct decoding decreases exponentially with the number of channel uses, and we derive explicit bounds on the decay exponent. When only the mean photon number is constrained, a simple energy-rescaling formula determines exactly the entire asymptotic rate--error trade-off: the capacity at mean photon number and allowed average decoding error equals the vanishing-error capacity at mean photon number . Together, these results identify the ultimate limits of classical communication for some of the most fundamental models of optical communication. △ Less
This mission is the statement-level formalization of Classical Capacity of Single-Mode Bosonic Gaussian Channels (arXiv:2610.22308v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Affine envelope and joint convexity of the moment-resolved entropy (Eq. (18), PDF p. 4). 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.
27 results of the paper are not stated yet, because the library lacks an interface they need:
We give a representation for entanglement-breaking channels in separable Hilbert space that generalizes the "Kraus decomposition with rank one operators" and use it to describe the complementary channels. We also give necessary and sufficient condition of entanglement-breaking for a general quantum Gaussian channel. Application of this condition to one-mode channels provides several new cases where the additivity conjecture holds in full generality.
This mission is the statement-level formalization of Entanglement-breaking channels in infinite dimensions (arXiv:0802.0235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Radon–Nikodym representation of a POVM (Lemma 1: Radon–Nikodym representation of a POVM (9)–(10), PDF p. 3). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The work is devoted to study of quantum mutual information and coherent information -- the two important characteristics of quantum communication channel. Appropriate definitions of these quantities in the infinite-dimensional case are given and their properties are studied in detail. Basic identities relating quantum mutual information and coherent information of a pair of complementary channels are proved. An unexpected continuity property of quantum mutual information and coherent information following from the above identities is observed. An upper bound for the coherent information is obtained.
This mission is the statement-level formalization of Mutual and coherent informations for infinite-dimensional quantum channels (arXiv:1004.2495v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: complementary-channel mutual-information identity (22) (Theorem 1: complementary-channel mutual-information identity (22), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.