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?
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.
Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem
the worst-case expectation of a value vector over the ambiguity set . Robust value iteration is only as practical as this inner problem is cheap.
The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change .
Let be a finite set of states and let be the probability measures on . For and write
Fix a centre with for every (in the paper is the empirical next-state distribution of one state–action pair) and a radius . The χ² set (46) is
Since , the relative entropy is at most the χ² distance, so lies inside the relative-entropy ball of radius : it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ , all in the namespace RobustDP.ChiSquare.
For every value vector ,
where ranges over vectors with componentwise. Both extrema are attained. The lemma's complexity claim, for (48), is a statement about an algorithm and is not part of the mission.
Two further results stand on the same definitions: the inequality of Section 4.2, and the analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):
The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level . The truncation comes from the constraint .
Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.
The obvious argument drops the constraint . Without it, the minimum of the linear function over the ellipsoid follows from Cauchy–Schwarz and equals . The page notes (p. 19) that earlier work solved only this relaxed problem. With the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier of is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone needs an additional argument, namely that an optimal multiplier has the truncation form (53).
Fintype; vectors are functions S → ℝ; is Mathlib's stdSimplex ℝ S. Nonemptiness of follows from . Finiteness is the standing restriction of Section 4 (p. 15).IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.0 ≤ μ). The multiplier of the equality ranges over . The page's "" in (50) is a misprint: the proof of Lemma 6 writes , and the optimal may be negative.⨆ over an unbounded set, would make the statement junk.The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a fraction, then take the first item better than everything seen) selects the best item with probability about , and no rule does better. Many allocation problems are not single-choice: a seller with identical goods facing bidders who arrive over time, an advertiser with a budget of impressions, an employer with openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when selections are allowed?
Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least times the sum of the largest values, so the ratio tends to as grows, and stated a matching upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).
Timeline. Dynkin (1963) and the classical literature settle with ratio . Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves for selections, with the explicit constant . Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.
Let be a finite set of distinct non-negative real numbers. The elements of are revealed in a uniformly random order: each of the orders has probability . After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most elements may be selected. Write for the set of the largest elements of (all of if ) and
for their sum, the best total any rule could collect knowing in advance.
Kleinberg's algorithm is defined by recursion on :
The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.
The statement is uniform in and ; it says nothing beyond the explicit constant printed in the paper.
The paper proves the theorem by induction on . Its sketch introduces , the set of the first arrivals, , the modified value of a set (the sum of its elements lying in ), and , the number of elements of exceeding . The milestones are its stated claims, in order:
The result. Theorem 2.1 shows that random arrival order costs only a factor when many items are sold, against the constant for a single item. With the paper's matching upper bound, it pins down the optimal rate for the -choice problem. It is the base of the paper's strategyproof online auction for identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.
Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.
The obvious argument fixes and treats the threshold as if it split the remaining elements exactly. Both steps fail. With a fixed , the first arrivals are not a uniform subset of and is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of is what makes uniform. And the number of later elements beyond fluctuates by order : the second phase may run out of budget before reaching all of , or accept elements outside . Controlling this fluctuation, while the cap of also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.
The Lean development fixes these conventions.
Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time (0-based) under the order is the -th smallest element of , and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.PMF over sets of selected positions, defined by well-founded recursion on . The base case is the published SecretaryWD.DiscUpper.classicalSecretary. is Mathlib's PMF.binomial (1/2). At the algorithm selects nothing, for totality only; all statements assume .A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.