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?
Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).
Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.
Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model
for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form
with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of
Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).
Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then
The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.
The milestones are the displays of the proof, in the order the proof uses them:
Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.
The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.
The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.
Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.
TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.sInf would make (2.19) false and is ruled out.The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.
A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.
In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.
Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.
Timeline.
Decisions and states are vectors in . The decision set is a possibly infinite set and the state set is . In period the decision maker picks , then the state is revealed, and the cost is the dot product . The state sequence is fixed in advance (an oblivious adversary).
Write , with . The offline oracle is a map with
Because costs are linear, the best fixed decision after periods has cost
Three parameters measure an instance, with :
FPL(), for a parameter : in each period , draw uniformly at random from the cube and play . Its expected cost is .
Hannan(): the same rule with uniform on .
For every state sequence and every ,
The constants are the paper's. With the expected regret is at most .
For any state sequence in , any and any ,
This bound needs no knowledge of . It is included as a separate theorem, not a milestone of the goal.
The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.
Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound and therefore yields a weaker constant () in this setting. This mission states the exact-oracle bound with the paper's constant , where bounds itself. A correct proof must handle that constant carefully; see the next section.
Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.
The central difficulty is the stability step: bounding, period by period, how much worse it is to play than . The obvious argument says that the two perturbed points have laws that agree on a fraction, and on the rest "one can only be larger". Under the printed definition of the difference of two costs can be as large as , so this per-period bound fails for costs of mixed sign: with , and suitable , the per-period difference is , while . The theorem itself, with , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than , is the substantive part of the mission.
Fin n → ℝ; is dotProduct (⬝ᵥ); is written out as ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.s : ℕ → Fin n → ℝ indexed from (s 0 is unused); the hypothesis is imposed for .IsArgminOracle Dset M: and for all . Every theorem quantifies over all such ; the oracle is never a chosen Classical.epsilon minimiser.OracleRO.ApproxFPL.FPL: prefixSum s t ; perturbLaw n ε, the uniform law on ; and fplExpectedReward M s ε T , which with an argmin oracle is the expected cost of FPL() (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.
An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.
All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.
The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is
The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.
The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Fixed-point bounds compare Hamiltonian dynamics with critical points of smooth functions. Degenerate fixed points are central to the unrestricted formulation tested here. The pinned manuscript supplies the research context.
The space is the complex projective quadric threefold, represented through its unit quadric and quotient tangent directions. Hamiltonian maps are endpoints of the specified smooth isotopies.
The selected goal is OAI.ArnoldCounterexample.main. Its central assertion is
The theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.
The goal includes the lower bound on all smooth critical sets and at least one degenerate fixed point. A rational cup-length computation is not a separate conclusion of this target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Counting fixed points is insufficient: the construction must satisfy the Hamiltonian lift conditions and give a genuine nonzero quotient-tangent eigenvector at a degenerate point.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Rademacher cotype measures how vector norms compare with random signed sums. The target relates cotype of a space and its dual to boundedness of the Rademacher projection. The pinned manuscript supplies the research context.
X is a nonzero real Banach space with the ordinary approximation property: finite-rank operators approximate the identity on each compact set, with no uniform operator-norm bound required.
The selected goal is OAI.Cotype.mainTarget_proved. Its central assertion is
The theorem states that, for every real Banach space X (a complete real normed space) that is nontrivial, the defined proposition MainTarget(X) holds. MainTarget(X) says: if X has the approximation property, then X is K-convex if and only if both X and its dual space of continuous linear functionals X →L[ℝ] ℝ have finite cotype. Here the approximation property means that for every compact set M ⊆ X and every δ > 0 there is a continuous linear operator S : X → X with finite-dimensional range such that ‖Sx − x‖ < δ for all x in M. On the discrete cube {±1}ⁿ (with sign false = +1 and true = −1), the L² norm of f : cube → X is the square root of the average of ‖f(ε)‖² over all ε. The moment of f at coordinate i is the average of ε_i f(ε), and the Rademacher projection of f is the function ε ↦ Σᵢ ε_i times the moment at i. X is K-convex if there is a constant K ≥ 0 such that, for every n and every f on the n-cube, the L² norm of the Rademacher projection of f is at most K times the L² norm of f. X has cotype q, for real q ≥ 2, if there is C ≥ 0 such that, for every n and all vectors x₁, …, xₙ in X, (Σ ‖xᵢ‖^q)^(1/q) ≤ C times the L² norm of ε ↦ Σ ε_i xᵢ. Finite cotype means cotype q for some such q.
The approximation property is a hypothesis inside MainTarget. The statement does not assert the equivalence without it; the cube normalization is the encoded average L² norm. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The two cotype exponents may differ, and ordinary approximation cannot be strengthened silently to bounded approximation.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.A Banach norm supplies both linear and metric structure. A bi-Lipschitz equivalence controls distances, but the target asks for spaces whose linear structures cannot be identified. The pinned manuscript supplies the research context.
The two spaces are real, complete and separable. The obstruction uses the space of null sequences with values in the real Hilbert space ℓ².
The selected goal is OAI.LipschitzCounterexample.main. Its central assertion is
The theorem states that the defined proposition MainClaim holds (it is admitted in the source, not proved here). MainClaim asserts that there exist two separable real Banach spaces X and Y, each given as a type with a norm, a real normed-space structure, completeness and separability, together with a bijection Ψ from X onto Y, such that Ψ is a bi-Lipschitz equivalence with explicit constants: for all s and t in X, (4/21)‖s−t‖ ≤ ‖Ψ(s)−Ψ(t)‖ ≤ (76/25)‖s−t‖. Moreover, there is no continuous linear equivalence (linear homeomorphism) between X and Y, so the two spaces are Lipschitz equivalent but not linearly isomorphic. In addition, there is a linear isometric embedding of C0L2 into X, where C0L2 is the space of continuous functions from the natural numbers to the real Hilbert space ℓ² that vanish at infinity. Finally, Y does not contain a linear copy of C0L2, meaning there is no bounded linear map T from C0L2 to Y and constant a>0 with a‖x‖ ≤ ‖T x‖ for every x in C0L2.
The goal includes the explicit distortion bounds, lack of continuous linear equivalence, an isometric copy of c0(ℓ²) in X, and absence of a bounded-below linear copy in Y. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
A global metric bijection must coexist with a linear embedding obstruction, so the counterexample cannot follow merely from nonlinearity of a particular map.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Residual finiteness means that finite quotients can distinguish every nonidentity group element. The source asks whether coarse negative curvature forces this separation property even without torsion. The source is OpenAI's September 2026 manuscript.
A torsion-free group has no nonidentity element whose positive power is the identity. A word-hyperbolic group admits a finite generating set whose Cayley graph has geodesic triangles of uniformly bounded thickness.
The theorem states, without a verified proof (it is admitted), that there exists a group G, in the lowest universe Type, that is torsion-free, word-hyperbolic, and not residually finite. Torsion-free means that for every g in G and every positive integer n, g^n = 1 implies g = 1, so no nonidentity element has finite order (this does not assert unique roots). Word-hyperbolic means that there is a finite subset S of G whose unit-edge Cayley graph (the simple graph with the multiplicative Cayley adjacency determined by S) is connected, which says that S generates G, and a natural number δ such that geodesic triangles are uniformly δ-thin. Precisely, for all vertices x, y, z and walks p from x to y, q from y to z and r from z to x, each of which is a geodesic (its length equals the graph distance between its endpoints), every vertex of each side lies within graph distance δ of some vertex on one of the other two sides. The statement also requires that G fail the Mathlib property Group.ResiduallyFinite.
The goal is OAI.Release075.main.
The goal puts a geometric condition and failure of finite-quotient separation into one existential statement. Torsion-freeness is retained explicitly. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Hyperbolicity concerns large-scale word geometry, whereas residual finiteness quantifies over every finite quotient. Checking a finite list of quotients cannot establish the required failure.
Hyperbolicity is encoded by vertexwise thin triangles in a connected unit-edge Cayley graph for some finite generating set. Torsion-freeness is the positive-power condition and does not mean a unique-roots property. Residual finiteness uses the Mathlib definition.
The shared definitions are supplied by TorsionFreeHyperbolic. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A Diophantine representation translates membership in a computably enumerable set into solvability of one polynomial equation. The source asks whether the entire auxiliary witness can always be made unique. The source is OpenAI's September 2026 manuscript.
A single-fold representation uses an integer polynomial evaluated at natural-number inputs and witnesses. An input belongs to the represented set exactly when a witness makes the polynomial zero, and any two complete witnesses at the same input must coincide.
The proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w.
The goal is OAI.SingleFold.main.
The target strengthens mere existential representation by enforcing uniqueness across every auxiliary coordinate. It covers all recursively enumerable sets of positive-length natural tuples. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Encoding a computation with extra witnesses can introduce many choices that do not affect the represented input. Every such auxiliary choice must be controlled, rather than leaving hidden coordinates outside the uniqueness assertion.
The input length and witness length are positive naturals. REPred expresses recursive enumerability. Polynomial coefficients and evaluation are integral, while variables range over naturals cast into the integers. The goal is existential and does not require one fixed universal polynomial.
The shared definitions are supplied by SingleFold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An inequality involving only four rows can feed into a recursion for a much larger permutation shuffle. The source seeks an exponent strictly below two that survives a small perturbation of the uniform permutation law. The source is OpenAI's September 2026 manuscript.
A permanent expectation averages the product of four selected entries, one from each row and each column, over a probability law on the 24 permutations. Uniform marginals require every row to choose each column with probability .
The theorem is stated as admitted, not proved here. Sites are Fin 4, and a law is a real-valued mass function ν on the 24 permutations of the four sites. It states that there exist a real exponent p₀ with 4/3 < p₀ < 2 and a real ε > 0 such that the following holds for every law ν that is a probability law (all masses nonnegative and summing to 1), has total variation distance from the uniform law less than ε (total variation being half the sum over permutations π of |ν(π) − 1/24|), and has uniform marginals (for every pair of sites i and j, the total mass of permutations with π(i)=j equals 1/4). For every 4-by-4 array f of real numbers with all entries f(i,j) ≥ 0, the permanent expectation Σ_π ν(π) ∏_i f(i, π(i)) is at most the product over the four rows i of the normalized ℓ^{p₀} norm of row i, where the norm of a row g is ((Σ_j g(j)^{p₀})/4)^{1/p₀}, using the uniform counting normalization with division by 4.
The goal is OAI.FourRow.robust_permanent. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The goal is uniform over all nonnegative arrays and all probability laws within the chosen total-variation neighborhood that have exactly uniform marginals. The shared Thorp bundle is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Near-uniformity alone does not enforce the marginal identities. The exponent improvement must hold even for highly uneven nonnegative row entries.
The law has nonnegative real masses summing to one. Its distance from the uniform law is strictly less than the selected , and row norms use division by four. No explicit value for the existential exponent or radius is imposed.
The shared definitions are supplied by FourRowPermanent, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Critical self-avoiding walks have weights balanced between exponential path growth and decay. The source studies bridge-length scaling; the available target establishes summability of the bridge sums used to define these quantities. The source is OpenAI's September 2026 manuscript.
A honeycomb bridge is a self-avoiding vertex list crossing a strip from a fixed initial port to any terminal port on the opposite layer. A path with vertices has critical weight , with .
For every integer h ≥ 1, six families of sums over self-avoiding bridge paths in a honeycomb strip are absolutely summable. Vertices of the honeycomb lattice are of two kinds, up(i,j) and down(i,j) with integer i and j, and the layer of a vertex is its second index j; an up vertex (i,j) is adjacent to the down vertices (i,j−1), (i,j) and (i−1,j), and adjacency is symmetric. A bridge path of height h is a list of distinct vertices, consecutive ones adjacent, starting at up(0,0), ending at some down(i,h−1), with every vertex in layers 0 through h−1. Its weight is λ^L, where L is the number of vertices and λ = 1/(2cos(π/8)) is the critical activity, and its first-length weight is L·λ^L. Let bridgeMass(h) be the total weight of all bridge paths. A path is confined if every vertex has horizontal coordinate (i + j/2 for up vertices, i + j/2 + 1/2 for down vertices) of absolute value at most h(log h)², and confinedMass(h) is the total weight of confined paths. The theorem asserts summability over all bridge paths of the weight, of the first-length weight, and of the first-length weight divided by bridgeMass(h), and summability over confined paths of the weight, of the first-length weight, and of the first-length weight divided by confinedMass(h). The proof is admitted in the source, not established here.
The goal is OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums.
The full formal statement gives six summability assertions, including normalized first-length weights and their corridor-confined counterparts. These are prerequisites for interpreting bridge masses and mean lengths. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Each strip has unbounded horizontal extent and admits paths of arbitrarily large length. Finite strip height therefore does not by itself make the path family finite.
The length convention counts vertices. Confinement means horizontal coordinate bounded by . The target proves summability, without asserting the manuscript’s asymptotic law. Normalized terms use the masses defined by tsum.
The shared definitions are supplied by HoneycombBridgeFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.
A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size costs . An ordinary cover and a fractional cover both have budget ; a fractional cover assigns weights in and supplies total weight at least one inside each member. The expectation thresholds and are suprema of feasible parameters in .
For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.
The goal is OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence.
The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.
The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.
The shared definitions are supplied by TalagrandExpectationThreshold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An oriented graph may have very uneven outdegrees, yet the second-neighborhood conjecture asks for one vertex whose new two-step reach is at least its immediate outdegree. The source manuscript presents the surrounding research claim.
An oriented graph is a loopless asymmetric relation r on a finite nonempty vertex type. First neighbors satisfy r(v,w). Second neighbors are vertices w distinct from v, not already first neighbors, but reached by some directed path v→u→w.
Prove that some vertex v satisfies
Every second-neighborhood vertex is counted once, irrespective of how many two-step paths reach it.
The selected formal target is OAI.SeymourSecondNeighborhood.exists_goodVertex.
The statement covers all finite oriented graphs, including disconnected graphs and graphs whose underlying undirected graph is not complete. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Counting length-two walks overcounts repeated endpoints and may include first neighbors. The conclusion concerns the set of vertices at directed distance exactly two.
The formal relation need not be supplied with decidability; the finite sets are formed classically. Looplessness and asymmetry are explicit hypotheses, and the vertex type is finite and nonempty. GoodVertex is exactly the finite-cardinality comparison.
adc7f1241b42. Goal source.Euclidean Ramsey theory asks which finite shapes must occur monochromatically in a sufficiently high dimension. The scale is fixed, so an algebraic criterion must capture exact distances rather than approximate similarity. The source manuscript presents the surrounding research claim.
A Ramsey configuration a=(aᵢ) has a monochromatic congruent copy under every finite coloring in some dimension depending on the number of colors. Let F be the rational field generated by all coordinates, B=F⊗ℚF, and pᵢ=(1,aᵢ) the augmented coordinate vectors. Multiplication m:B→F sends x⊗y to xy.
For an injective configuration of at least two points affinely spanning ℝᵈ with d≥1, prove
The criterion asks for a matrix P over B with (pᵢ⊗1)ᵀP(1⊗pᵢ)=0 for every i and m(P_{αβ})=δ_{αβ} on the coordinate-coordinate block.
The selected formal target is OAI.EuclideanRamsey.classification.
The criterion is necessary and sufficient for the stated configurations. Available companion targets describe spherical necessity, positive classes and concrete non-Ramsey circle configurations. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Applying m to the tensor identity loses information because multiplication need not be injective. Equality in the tensor ring, and arbitrary colorings without measurability, are essential.
The goal uses real Euclidean coordinates and the exact generated intermediate field over ℚ. Congruence preserves all pairwise distances at their original scale. All published companion references are retained as separate groups because they repeat Ramsey definitions. Milestones state their own hypotheses and do not identify every spherical set as Ramsey.
adc7f1241b42. Goal source.Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.
States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.
Prove
with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).
The selected formal target is OAI.Problem315.switch_chain_main.
The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.
The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.
adc7f1241b42. Goal source.Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.
Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.
Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with
The selected formal target is OAI.TreeEdit.binary_lower_bound.
The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.
The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.
adc7f1241b42. Goal source.Covering numbers measure the size of a set at a given scale: is the least number of translates of needed to cover . Their logarithms, the metric entropy, appear across approximation theory, operator theory (entropy numbers of compact operators), probability (Dudley's bound) and learning theory. A basic question in asymptotic geometric analysis is how metric entropy behaves under duality: if is hard to cover by , is the polar body equally hard to cover by ? The duality conjecture for metric entropy, originating in Pietsch's 1972 work on operator ideals, predicts that the two quantities agree up to universal constants, independently of the dimension.
The source of this mission is an OpenAI preprint dated September 24, 2026, which disproves the dimension-free conjecture.
Work in with the standard pairing . A convex body is a compact convex set with nonempty interior; it is origin-symmetric if . Its polar is
For bounded and a body , the covering number is the least such that for some (centres need not lie in ). Logarithms are natural. Let be the cube; its polar is the cross-polytope.
The duality conjecture asks for absolute constants such that, for every and all origin-symmetric convex bodies ,
For every there are and an origin-symmetric convex body such that, with ,
The Lean statement OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers is open on the platform.
The theorem shows that the upper inequality of the conjecture fails for every proposed pair of constants, so the two-sided conjecture has a negative answer, even when one body is a cube. It also separates ordinary covering entropy from convexified-packing entropy, for which Artstein–Milman–Szarek–Tomczak-Jaegermann proved universal duality (Corollary 5.1 of the source). Dimension-dependent results (König–Milman, E. Milman) remain compatible with the counterexample, which shows that some dependence on dimension or structure is unavoidable.
The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The counterexample is explicit and finite-dimensional, which makes a full formalization realistic.
The known positive cases (Euclidean balls, ellipsoids, bounded K-convexity) suggest the conjecture is true, and the obvious candidate bodies, products and cubes, satisfy it. A counterexample needs a body whose primal entropy against the cube is large while the polar side is small; the paper reduces this to a finite matrix with entries in whose rows are pairwise -separated in the sup norm while the absolutely convex hull of its columns admits a small uniform approximation list. Producing such matrices requires partition structures over finite fields with uniform control over all row coordinates, and the entropy gap must beat every fixed after the scale change .
RealSpace (Fin n) = Fin n → ℝ with pairing the standard dot product; cube is ; polar K uses .Covers A B centers means every has some centre with ; coveringNumber is the sInf of the admissible . The statement includes Coverable side conditions, which only certify that both infima are over nonempty sets.IsSymmetricConvexBody = compact, convex, , nonempty interior.a⁻¹ • polar K; logs are Real.log of natural numbers cast to reals.A complete development needs support functions and polarity, elementary covering-number bounds, finite-field polynomial zero bounds (Schwartz–Zippel), and the matrix-to-body conversion. The covering-number and polarity layer is reusable for other convex-geometry missions. Contributions formalizing Lemma 2.1 (matrix-to-body conversion), Proposition 3.2 (uniform compression) and Proposition 4.3 (partitions with separated rows) are welcome.
A map is nonexpansive if . Unlike strict contractions, nonexpansive maps need not have fixed points: on a bounded set, existence depends on the geometry of the norm. A Banach space has the fixed point property (FPP) if every nonexpansive self-map of every nonempty closed bounded convex subset has a fixed point. Since the mid-1960s, whether every reflexive Banach space has the FPP in its given norm has been one of the central open questions of metric fixed point theory. Many sufficient geometric conditions are known, but none of them covers all reflexive spaces. In fixed point theory, the question has been listed as unresolved as recently as 2026 (Nourouzi 2026).
Let be a real Banach space and its continuous bidual. The canonical map , , is always a linear isometry, and is reflexive if is surjective. A subset is taken nonempty, closed in the norm topology, bounded and convex. A map is nonexpansive in the given norm of , and a fixed point is a point with .
In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.
This is exactly Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem answers the reflexive-space fixed point problem for the given norm, with no extra geometric assumption (uniform convexity, normal structure, unconditional bases, uniform nonsquareness). With Bruck's 1974 theorem it gives the source's Corollary 1.2: for every commuting family of nonexpansive self-maps of , the common fixed point set is nonempty and is a nonexpansive retract of . Alspach's example shows that reflexivity cannot be weakened to weak compactness of in an arbitrary Banach space.
Formalizing it. Earlier proposed proofs of the same assertion exist, and the literature has not reached a consensus, so a machine-checked proof would give unusual certainty on a disputed question. The proof relies on the minimal invariant set reduction (Zorn's lemma and weak compactness), the Goebel–Karlovitz lemma, compact semigroups of nonexpansive maps (an Ellis-type idempotent), and a tree construction with weighted telescoping estimates. Mathlib has the bidual, the weak topology, and Banach–Alaoglu, but most of the fixed-point-theoretic layer has to be built.
The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in is asymptotically diametral. Normal-structure arguments then find a point whose radius is strictly below the diameter. In a general reflexive space there is no such geometric gain, and Karlovitz's example shows that normal structure is not necessary for the conclusion. Alspach's example shows that compactness of and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of ), not just of the domain. A further obstacle is that is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.
CompleteSpace X, and reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ X (the continuous bidual). Completeness also follows from reflexivity, so including it is harmless. The scalar field is ; complex spaces enter as real spaces.Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of , not in an equivalent norm.∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial is excluded only by nonemptiness, as in the source.For a square matrix , the spectrum alone does not control the size of : a nonzero nilpotent matrix has spectrum yet . The numerical range is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial ,
i.e. that is a -spectral set; the constant would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has matrix coefficients, uniformly in ; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of to a contraction with condition number at most .
This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For () let . A matrix polynomial of degree with coefficient size is with . Its evaluation at is
with the base space first. All norms are Euclidean operator norms. For this is the usual .
For a bounded operator on a complex Hilbert space , and ; acts on . A bounded open convex is admissible if its boundary is a regular real-analytic Jordan curve. For such ( a matrix) with interior conformal map , put and
For , is compact and convex and contains .
If , the numerical range is empty, every polynomial, holomorphic and rational evaluation is , and the corresponding inequalities read (with the supremum over the empty set taken to be ).
For admissible conformal coordinates exist; for every and with , the problem defining is strictly feasible with attained minimum ; for a minimizer , satisfies and is a contraction with ; and one continuous with , represents for every and every -valued holomorphic near , giving .
For all , , , : , and no smaller universal constant works.
For every complex Hilbert space (no separability assumption) and : if then is compact, convex, contains the spectrum, and for every
for matrix polynomials , matrix functions holomorphic on an open (holomorphic functional calculus), and matrix rational functions with poles off ; if the degenerate statements above hold; and the constant is optimal.
The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: is a complete -spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most , and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.
Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.
Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in , but one must show every vector of and its image under live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.
H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification is the completion of the algebraic tensor product, and is the completed TensorProduct.mapL.supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is , matching the convention of Corollary 6.3.CalculusContour around inside ; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.SharpConstant is witnessed by a matrix with and .Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).
For a square matrix , the spectrum alone does not control the size of : a nonzero nilpotent matrix has spectrum yet . The numerical range is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial ,
i.e. that is a -spectral set; the constant would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has matrix coefficients, uniformly in ; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of to a contraction with condition number at most .
This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For () let . A matrix polynomial of degree with coefficient size is with . Its evaluation at is
with the base space first. All norms are Euclidean operator norms. For this is the usual .
For all , , and ,
If the inequality holds with a constant in place of for all , then .
Both assertions together: the constant is valid and no smaller universal constant is.
The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension , the coefficient size and the degree, including matrices whose numerical range is a point or a segment. The scalar case had recently been proved by other authors and the complete case was known only for ; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete -spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most making the conformal disk image of a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.
Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant- Crouzeix bound is known.
The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields . To reach in the complete setting, the argument must keep both multiplication orders and of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair of , represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).
Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of over unit vectors of EuclideanSpace ℂ (Fin n).B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is indexed by Fin n × Fin m, base factor first.rangeMaximum A B is the sSup of over . Since , is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all , all , all and .OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).
This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
An -mode bosonic system has Fock space with number basis , . A state is a positive trace-one operator ; it has finite energy if . The von Neumann entropy is (natural log). The thermal entropy per mode is
increasing from to , and the entropy photon number of is , the mean photon number per mode of the product thermal state with the same entropy. For independent inputs and transmissivity , the beam-splitter output is the reduced state of the modes after passive mixing of . No independence among the modes within either input is assumed.
For every finite , every pair of finite-energy -mode states and every ,
Thermal inputs with a common mean photon number within each port give equality.
The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.
Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.
Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.
Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to .FiniteEnergy ρ is summability of .entropy ρ is the sum of diagonal entries of ; for finite-energy states it is finite, so the tsum is the true entropy.gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of on .IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to ; the inputs are arbitrary density matrices, so internal entanglement is allowed.Given a group , adjoin one new generator and impose one relation , where is a word in and elements of . Can the result collapse to the trivial group when is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation with coefficients in have a solution in some group containing ?
The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.
Let be a group, , and the free product. Let be the homomorphism that kills and sends to ; is the exponent sum of in . A word is unimodular if . Write for the normal closure of in . The coefficient map is the composite
Its injectivity is equivalent to solvability of over : there is an overgroup and with .
The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.
Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if then for every , since for the quotient maps onto . It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on : no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.
The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of .
Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.A complete development needs the group von Neumann algebra of (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed -planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.
A class of structures is categorical in a cardinal if it has exactly one model of size up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with (the Hanf number for existence of arbitrarily large models), categoricity in some should imply categoricity in every . Deciding which form holds is a central question in non-elementary model theory.
Work with relational structures in a finitary relational language (a set of relation symbols, each with a finite arity). An abstract elementary class is a class of -structures with a relation ("strong substructure") such that: is a partial order on refining substructure; and are closed under isomorphism; coherence holds (, , imply ); unions of -chains are in , are -extensions of each member, and are -below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number , the least such that every subset of a model lies in some with .
is categorical in if it has a model of size and any two models of size are isomorphic. The beth numbers are , and suprema at limits. CH is .
Assume CH. There is a countable finitary relational language and an AEC in such that
has two nonisomorphic models of cardinality , and, with ,
Hence is a categoricity cardinal from which downward transfer to fails, while eventual categoricity holds for this . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.
Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.
Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound while categoricity holds on a tail, with . One must build two nonisomorphic models at and simultaneously rule out any two nonisomorphic models above , without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.
RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; Type with countable.ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.HasLSNumber ℵ₀ asserts both that is a Löwenheim–Skolem bound and that it is the least one.hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).Categorical μ includes existence of a model of size ; TwoModels asks for two nonisomorphic models of the given size.Many questions about random graphs ask when a property — connectivity, containing a triangle, having a perfect matching — appears in the Erdős–Rényi random graph , where each of the possible edges is present independently with probability . For an increasing property the probability rises from to as grows, and the threshold width measures how quickly: the length of the interval of over which climbs from to . Friedgut and Kalai showed in 1996 that symmetry alone forces every such transition to be narrow, and conjectured the optimal universal width. This question links probabilistic combinatorics with the Fourier analysis of Boolean functions, and the influence inequalities developed for it are now standard tools in theoretical computer science and statistical physics.
Fix an integer and let be the set of unordered pairs of vertices. A graph configuration is a map (in Lean GraphConfig n := GraphEdge n → Bool, where GraphEdge n is the type of 2-element subsets of Fin n). A Boolean function on configurations is
For the graph mean is , the probability that has the property when . For the quantile is
For every , every vertex-invariant, increasing, nontrivial , and every ,
The constant is the source's explicit choice and is not claimed to be sharp; the content is the order with linear dependence on . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The bound is uniform over all monotone graph properties and is of optimal order in for fixed , as the clique example of Friedgut and Kalai shows. It settles the exponent question left open between the bound of 1996 and the bound of 1997. The driving estimate in the source, Theorem 1.2 (variance is at most times total influence, for every and without monotonicity), is a graph-symmetric influence inequality of independent interest; it removes the loss of the 2020 bound and holds at every bias.
Formalizing it. A formal proof would certify a universal statement over all graph properties with an explicit constant. The supporting library — Fourier–Walsh analysis on biased product spaces, pivotal influences, the Margulis–Russo derivative formula, and random restrictions — is reusable for other threshold and influence results, none of which are currently formalized in Mathlib in this form.
The classical route bounds the derivative from below through the largest influence, using only that the symmetry group acts transitively on edges; transitivity alone cannot give better than , because there are transitive families (on non-graph coordinate sets) whose thresholds are that wide. Reaching requires using the vertex structure of the symmetry group, and the bound must hold uniformly for every bias , including very small where hypercontractive estimates degrade. Influence estimates at alone do not suffice, since a width bound requires control throughout the transition interval.
GraphEdge n → Bool; the measure is the explicit finite sum graphMean p f with product weights or ; logarithms are natural (Real.log).graphQuantile a f is sInf of . For a nontrivial increasing , , so this set is nonempty and the infimum is not a junk value; the hypotheses NontrivialGraphProperty and exclude the degenerate cases.A Hadamard matrix of order is an matrix with entries whose rows are mutually orthogonal, . Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.
The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths are known, and the long-standing Barker-sequence conjecture says there are no others.
Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring .
A real matrix is circulant if there is a function with , indices taken modulo . It is a sign Hadamard matrix if every entry is or and
For a circulant sign matrix with first row , the periodic autocorrelations are ; the Hadamard condition says for .
A Barker sequence of length is with aperiodic autocorrelations
The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.
Combined with the classical odd-length classification, this gives the Barker length list .
Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters exist only for . It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.
The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.
The orthogonality condition is a norm equation in the group ring , and every character sends to a cyclotomic integer of absolute value . Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case with odd and divisible by several primes. The obstruction must combine information from all prime divisors of simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.
RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.IsSignHadamard H is entrywise IsSign (equal to or ) together with H * H.transpose = (n : ℝ) • 1.0 < n, matching the paper's "positive integer ".Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by in absolute value for .A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above , and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction , odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.
A finite strategic game can be changed in ways that no player can detect strategically. Adding to player 's utility any function that does not depend on player 's own strategy leaves every unilateral comparison "is strategy better for me than strategy , given what the others do?" unchanged, so it leaves every best response and every pure Nash equilibrium unchanged. Such changes are not irrelevant, however: they move the payoff levels, and therefore change which outcomes are efficient.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011, DOI 10.1287/moor.1110.0500) make this precise. They decompose every finite game uniquely into a potential component, a harmonic component and a nonstrategic component (their Theorem 4.1). The first two determine all pairwise comparisons; the third determines nothing about equilibria. Section 5.3 of the paper asks what the third component can do to efficiency, and answers with Theorem 5.9: by changing only the nonstrategic component, the pure Nash equilibria of a game can be made to coincide exactly with its Pareto optimal profiles. This mission formalizes that result.
The question matters wherever a designer can transfer payoffs without altering incentives (for instance side payments to a player that depend only on the other players' actions): the theorem says such transfers can always align equilibrium with efficiency, provided an equilibrium exists.
There is a finite set of players. Player has a finite nonempty set of strategies; a strategy profile is , and denotes with player 's strategy replaced by . A game is a family of utilities , .
Two profiles are -comparable if they differ, and differ only in player 's strategy. The game graph has node set and an edge between every pair of profiles that are -comparable for some . On this graph:
Games form the space with the inner product . With the Moore–Penrose pseudoinverse for these inner products, the potential and harmonic components of a game are
and the nonstrategic component is what remains. A profile is a pure Nash equilibrium of if for all and , and it is Pareto optimal (Definition 5.3) if no profile has for all and for some .
For every game that has a pure Nash equilibrium there is a game with
The statement is existential and fixes nothing about beyond its potential and harmonic components; it asserts the full equality of the two sets, not one inclusion.
The result. The nonstrategic component has no influence on the pairwise comparisons, and hence on equilibria, yet Theorem 5.9 shows that it controls efficiency completely: whenever a pure equilibrium exists, some choice of it makes every equilibrium Pareto optimal and every Pareto optimal profile an equilibrium. Read the other way, two games that are strategically indistinguishable can have opposite efficiency properties, so any efficiency statement about a class of games (a price-of-anarchy bound, for instance) must depend on more than the strategic structure. The paper also uses Lemma 5.4 as a normalisation: the payoff levels at equilibria are a free parameter of the nonstrategic component.
Formalizing it. The theorem has a short proof on paper, but the proof works with the pairwise comparisons, whereas the statement is about the components , defined through pseudoinverses. Connecting the two requires the identities of the decomposition: that and that . The mission therefore produces a machine-checked link between the linear-algebraic decomposition of games and their equilibrium sets, which other results of the paper (and of the literature on near-potential games) also need. To the best of our knowledge, none of these statements has been formalized before; the result itself is proved in the paper.
The construction on pp. 31–33 is explicit, so the difficulty is not finding but keeping two descriptions of "differ only in the nonstrategic component" consistent. The statement uses the component maps; the proof checks pointwise that for -comparable . Passing from the second to the first needs the pseudoinverse identities for and with respect to the specific inner products of and ; a naive argument that treats as an inverse fails because has a large kernel. A second point is the case analysis in the definition of : whether a profile is -comparable to an equilibrium must be shown independent of which of two -comparable profiles is examined, and the case where a non-equilibrium profile is -comparable to an equilibrium for every player needs the separate argument of p. 33.
Players form a finite type ι with decidable equality; strategy sets E m are finite, nonempty and have decidable equality. A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), i.e. with the unweighted sum inner product of Section 4; the weighted inner product of Section 6 is not used. carries the inner product with the factor . The pseudoinverse is defined directly (Mathlib has none) as the inverse of on composed with the orthogonal projection onto the range. Pure Nash equilibrium is AGT.IsPureNash from the published agt_games bundle; Pareto optimality is Definition 5.3, stated for a plain utility function.
Added hypothesis. The paper leaves implicit that has a pure Nash equilibrium, and the goal carries it as a hypothesis. It is necessary: every finite game has a Pareto optimal profile (a maximizer of ), while a game without pure equilibria, such as matching pennies, has none in any game with the same potential and harmonic components, so the set equality would fail. The paper's proof uses an equilibrium in the step "deviation to a NE increases the payoff of at least one player". Lemma 5.4 needs no such hypothesis.
"Same potential and harmonic components" is stated as equality of the two component maps of Theorem 4.1, never as membership of in ; the two are equivalent only through the decomposition theorem. Without condition (i) the goal would be trivial (take constant, so that every profile is both an equilibrium and Pareto optimal), so condition (i) is what makes the statement nontrivial.
Needed infrastructure: the Penrose identities for the pseudoinverse; ; the fact that determines each (the -comparable edge sets for different are disjoint); and the explicit constructions of and . The pseudoinverse lemmas and the "same comparisons, same equilibria" bridge are reusable throughout the series. Proofs of the milestones, of the bridge in either direction, and of the Penrose identities are welcome as separate contributions.