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.
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?
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.Metric absorption asks whether adjoining a null-sequence component changes a space up to controlled distances. Linear absorption imposes a different requirement. The pinned manuscript supplies the research context.
The space Z is a separable real Banach space. The product Z×c0 uses the product metric, and equivalent metrics are compared through positive bi-Lipschitz constants.
The selected goal is OAI.C0Absorption.main_result. Its central assertion is
The theorem states that there exists a real normed space Z, in a fixed universe, with the following properties, where C₀ denotes the real Banach space of sequences ℝ-valued on ℕ that tend to zero at infinity, and a map f between metric spaces is bi-Lipschitz if there are constants 0<c≤C with c·d(x,y) ≤ d(f x,f y) ≤ C·d(x,y) for all x,y. First, Z is complete and separable. Second, Z contains no linear copy of C₀: every continuous linear map T from C₀ to Z fails to satisfy ‖Tx‖ ≥ c‖x‖ for all x for any c>0. Third, there is a surjective bi-Lipschitz map F from the product metric space Z × C₀ onto Z. Fourth, there is a bi-Lipschitz map from C₀ into Z. Fifth, Z is metrically universal for separable metric spaces: every separable metric space M, in the base universe, admits a bi-Lipschitz map into Z. Sixth, Z × C₀ is not linearly homeomorphic to Z, that is, there is no continuous linear equivalence, with continuous inverse, between Z × C₀ and Z.
The target also includes a bi-Lipschitz embedding of c0, universality for base-universe separable metric spaces, and failure of linear homeomorphism between the product and Z. 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 metric universality and absorption maps must not produce a bounded-below linear embedding of c0.
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.The separable quotient problem asks whether every infinite-dimensional Banach space admits a separable infinite-dimensional quotient. The selected statement isolates a negative result under the continuum hypothesis. The pinned manuscript supplies the research context.
A quotient is encoded as a surjective bounded linear map between Banach spaces over the same scalar field. The target considers both real and complex scalars.
The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is
The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.
CH is an explicit assumption. The published goal does not state relative consistency, a positive model, or the complete independence assertion in the manuscript title. 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 obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.
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.The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.
C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.
The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is
The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.
The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. 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 conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.
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.Tensorial absorption is a structural regularity property of a C*-algebra. A criterion in the central-sequence algebra would detect it through asymptotically commuting elements. The pinned manuscript supplies the research context.
For a nontrivial separable unital C*-algebra A and a free ultrafilter, the central algebra is the commutant of A's diagonal copy inside its norm ultrapower.
The selected goal is OAI.KirchbergRordam.character_criterion. Its central assertion is
The theorem states that, for a nontrivial separable C*-algebra A (in the base universe Type) and a free ultrafilter ω on the natural numbers, meaning an ultrafilter that refines the cofinite filter, the norm central-sequence algebra of A has no characters if and only if A is isomorphic to its minimal (spatial) C*-tensor product with the Jiang–Su algebra. The norm ultrapower of A is the quotient of the C*-algebra of bounded sequences in A by the ideal of sequences whose norms tend to zero along ω; the central algebra is the closed star-subalgebra of this ultrapower consisting of elements commuting with the diagonal copy of A, the images of constant sequences. The central algebra has no characters means that every star-homomorphism from it to ℂ (a linear, multiplicative, star-preserving map, not required to preserve the unit) is the zero map. The Jiang–Su algebra is the inductive limit C*-algebra of the standard prime-dimension-drop model system. The right-hand side asserts the existence of a star-algebra isomorphism over ℂ from A onto this tensor product. The proof is admitted in the source.
The target is the character criterion for one algebra and one free ultrafilter. The manuscript's infinite tensor-power consequence is not separately attached. 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 directions relate a scalar-valued representation obstruction to an isomorphism with a tensor product, using the precise inductive-limit Jiang–Su model.
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.Uniqueness of irreducible representations is a strong condition on a C*-algebra. The target asks for a counterexample to the expected compact-operator characterization without added set-theoretic hypotheses. The pinned manuscript supplies the research context.
Representations are nonzero star homomorphisms on complete complex inner product spaces. Irreducibility is expressed by closed invariant subspaces, and equivalence by an intertwining linear isometry.
The selected goal is OAI.NaimarkZFC.main. Its central assertion is
The theorem states that, for every universe level choice, there exists a type A carrying a C*-algebra structure (over ℂ) with the following five properties. First, A is simple in the sense that it is nontrivial and its only closed two-sided ideals are {0} and A itself. Second, A is not finite-dimensional as a complex vector space. Third, there is a continuous linear functional τ : A → ℂ that is a faithful tracial state: τ has norm 1, τ(aa) is a nonnegative real number for every a, τ(ab) = τ(ba) for all a and b, and τ(aa) > 0 whenever a ≠ 0. Fourth, A has a unique irreducible representation up to unitary equivalence: whenever π and ρ are nonzero star-homomorphisms (non-unital algebra homomorphisms preserving star) from A into the bounded operators on complete complex inner product spaces H and K, taken in the stated universe levels, and each has no closed invariant subspace other than 0 and the whole space, there is a linear isometric isomorphism U : H → K with U(π(a)x) = ρ(a)(Ux) for all a and x. Fifth, for every complete complex inner product space H in the stated universe, A is not isomorphic to the algebra of compact operators on H, meaning there is no injective star-homomorphism φ : A → B(H) whose range is exactly the set of compact operators on H.
The target explicitly requires simplicity, infinite dimension, a faithful tracial state and failure of all compact-operator isomorphisms in the stated universes. No additional set-theoretic hypothesis appears in its binders. 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 construction must combine infinite dimension, a faithful trace and uniqueness across the specified representation universes.
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.Hochschild cohomology measures whether a cocycle equation admits a primitive. In an operator algebra the boundedness requirement is part of the mathematical problem. The pinned manuscript supplies the research context.
Cochains are continuous complex multilinear maps into the von Neumann algebra itself, with its natural left and right multiplication actions.
The selected goal is OAI.BoundedHochschild.KadisonRingrose.main_result. Its central assertion is
The theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.
The goal covers every natural n, hence degrees at least two. It does not include a separately referenced degree-one inner-derivation theorem. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
An algebraic primitive is insufficient: the lower-degree cochain must remain continuous and bounded in the encoded operator-norm sense.
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.Quasitraces behave linearly on commutative subalgebras but need not initially be additive on all positive elements. A uniform defect on a fixed pair would separate them from traces. The pinned manuscript supplies the research context.
The algebra is separable and carries a normalized 2-quasitrace, meaning a quasitrace with the specified extension to two by two matrices. The witnesses are positive contractions.
The selected goal is OAI.Kaplansky.kaplansky_quasitrace_counterexample. Its central assertion is
The theorem (admitted in the source, not proved there) states that there exists a separable C*-algebra A, with its complex C*-algebra structure, for which the following hold. First, A carries a normalized 2-quasitrace. Here a 1-quasitrace is a function τ : A → ℂ such that τ(xx) is a nonnegative complex number for all x; τ(xx) = τ(xx*); τ(h + i k) = τ(h) + i τ(k) for self-adjoint h and k; and the restriction of τ to every norm-closed commutative (non-unital) star-subalgebra over ℂ is ℂ-linear. It is normalized if τ(1) = 1, and it is a 2-quasitrace if it extends to a 1-quasitrace σ on the 2×2 matrices over A (as a C*-matrix algebra) satisfying σ of the matrix with a in the upper-left corner and zeros elsewhere equal to τ(a) for all a. Second, there are positive contractions a and b in A, meaning each is of the form x*x and has norm at most 1, such that every normalized 2-quasitrace τ on A satisfies Re(τ(a+b) − τ(a) − τ(b)) ≥ 1/144. So no such τ is additive on this pair.
The selected goal is the quantitative quasitrace counterexample. The stable-finiteness and tensor-product consequences are retained as a separate published bundle. 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 same positive contractions must exhibit the defect for every normalized 2-quasitrace, while at least one such quasitrace exists.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Norm ultrapowers permit approximations along a free ultrafilter. An explicit algebra excluded from every nuclear target ultrapower tests the limits of this embedding mechanism. The pinned manuscript supplies the research context.
The group is the stated dyadic semidirect product. Its full group C*-algebra is specified by a universal property, and the ultrapower is bounded sequences modulo norm-null sequences along the ultrafilter.
The selected goal is OAI.NuclearUltrapower.main_no_embedding. Its central assertion is
The theorem states that, working in universe level 0, there exist a nonzero unital complex C*-algebra A and a group homomorphism ι from G into the unitary group of A such that the following hold. Here G is the semidirect product of the additive group of 3-vectors over the dyadic rationals Z[1/2] by SL₃(ℤ) × ℤ, where a matrix acts linearly on the vectors and the integer n acts by multiplication by 2ⁿ. First, (A, ι) is the full group C*-algebra of G: the span of ι(G) is dense in A, and every homomorphism of G into the unitaries of a nonzero unital C*-algebra D extends uniquely to a unital -homomorphism A → D. Second, A is separable as a topological space. Third, for every nonzero unital C-algebra B that is nuclear in the tensor-norm sense (minimal and maximal C*-tensor norms agree on B ⊗ C for every C*-algebra C) and every free ultrafilter ω on ℕ (one containing no finite set), there is no injective unital -homomorphism from A into the norm ultrapower of B, namely bounded B-valued sequences modulo those tending to 0 along ω. Fourth, there exist a nonzero unital C-algebra O and two elements s₀, s₁ of O satisfying the Cuntz relations (each sᵢsᵢ = 1 and s₀s₀ + s₁s₁* = 1), with O universal for these relations, such that for every free ultrafilter ω there is likewise no injective unital *-homomorphism from A into the norm ultrapower of O. The theorem is admitted in the source, not proved.
The goal includes separability, the full group universal property, nonembedding and the Cuntz-algebra corollary in the stated base universe. 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 single source algebra must obstruct all nuclear targets and free ultrafilters. Universal full-group and Cuntz-algebra constructions are part of the target.
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.Hilbert-space spectral localization does not automatically produce bounded elements of the underlying operator algebra. Bounded recovery asks when positive averaged detection survives that passage. The pinned manuscript supplies the research context.
A standard modular datum has a cyclic separating vector, spectral calculus and scalar centralizer. Unit vectors lie in shrinking bands around a fixed real spectral parameter.
The selected goal is OAI.BoundedRecovery.bounded_recovery. Its central assertion is
The theorem states that, for a standard modular datum S on a complex Hilbert space H (a von Neumann algebra M with a unit cyclic and separating vector ξ, a nondegenerate real spectral calculus D with unitary group D.unitary t, an antilinear isometric involution J, and a closed Tomita graph of a ↦ (aξ, a*ξ) over a ∈ M equal to the pairs (p, Jq) where p is mapped to q by the half-exponential graph of D) satisfying ScalarCentralizer (every a in M fixed by conjugation with D.unitary t for all real t is a complex multiple of the identity), the following holds. Let ω be an ultrafilter on ℕ that refines the at-infinity filter (ω ≤ atTop), let T be a bounded complex-linear operator on H, let s be real, and let δₙ > 0 tend to 0. Suppose hₙ are unit vectors, each with spectral support in the interval [s − δₙ, s + δₙ] (every bounded continuous function vanishing on that interval annihilates hₙ under the calculus), and suppose the limsup over n of the ω-limit of the symmetric time averages (1/2k)∫{−k}^{k} ‖T(D.unitary t hₙ)‖² dt is strictly positive. Then the recovery conclusion holds: there are a strictly increasing sequence nⱼ, operators vⱼ in M, and constants C and η > 0 such that for every j, ‖vⱼ‖ ≤ C, ‖T(vⱼ ξ)‖ ≥ η, and vⱼξ has spectral support in [s − 4δ{nⱼ}, s + 4δ_{nⱼ}]. The proof is admitted, not supplied.
The hypothesis is positivity of the specified ultrafilter time average and outer limsup. Bicentralizer triviality and further rigidity applications are not separate conclusions 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.
The recovered vectors must come from uniformly bounded algebra elements while retaining detection and shrinking spectral support along a subsequence.
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 bounded algebra representation need not visibly preserve adjoints. The similarity problem asks whether one bounded change of Hilbert-space coordinates restores that structure. The pinned manuscript supplies the research context.
Representations are continuous unital complex algebra homomorphisms into bounded operators on a complete complex inner product space. The conjugating operator must have a bounded inverse.
The selected goal is OAI.KadisonSimilarity.similarityTheorem. Its central assertion is
The theorem states that, for every C*-algebra A in universe u and every complex inner product space K in universe v that is complete (a Hilbert space), every bounded unital representation of A on K is similar to a star representation. Here a bounded unital representation is a continuous ℂ-algebra homomorphism π from A into the algebra of bounded linear operators on K; being an algebra homomorphism of unital algebras, it preserves the identity. Similarity to a star representation means that there is an invertible bounded operator S on K, with bounded inverse, such that for every a in A, S π(a*) S⁻¹ equals the adjoint of S π(a) S⁻¹. Equivalently, the conjugated map a ↦ S π(a) S⁻¹ commutes with the involution. This is the Kadison similarity statement as a defined proposition SimilarityTheorem, and the source declares it as a theorem whose proof is admitted rather than supplied.
Similarity is the selected goal. The two commutator formulations and explicit hyperreflexivity estimate remain distinct references with their own constants and universes. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
One operator S must work simultaneously for every algebra element. Uniform matrix-amplification estimates cannot acquire a dimension-dependent constant.
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.
Additional published targets are included as separate references:
OAI.KadisonSimilarity.universalCommutatorTheorem (Open).OAI.KadisonSimilarity.universalHyperreflexivity (Open).OAI.Kadison.uniform_commutator (Open).adc7f1241b42. Selected goal source.Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.
The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.
The selected goal is OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic. Its central assertion is
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. 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 required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.
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 hierarchy of infinitely many overlap scales need not fill an interval. Full support asks whether an admissible zero-temperature SK minimizer leaves any gap below overlap one. The pinned manuscript supplies the research context.
An order parameter is a nonnegative, monotone, right-continuous integrable function on [0,1). The Parisi value is defined by a Brownian stochastic-control supremum. The Stieltjes measure μ lives on the subtype Time=[0,1); its support below is taken in that relative topology.
The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is
The theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.
The main target is the five-part full-support conclusion for every encoded minimizer and Brownian system. The separate value-consequences bundle is retained as an additional formal 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.
The conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.
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.
Additional published targets are included as separate references:
OAI.SKValue.value_consequences (Open).adc7f1241b42. Selected goal source.Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.
The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.
The selected goal is OAI.MinimalVertex.main. Its central assertion is
The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.
The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.
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.Bounded-error factoring and exact factoring have different correctness requirements. Repetition until success and increasingly accurate rotations do not automatically give a fixed-gate, worst-case polynomial exact algorithm. The pinned manuscript supplies the research context.
Circuit instructions use NOT, CNOT, Toffoli, Hadamard and phase primitives, their inverses and singly controlled versions. A classical finite-stack machine generates each encoded circuit from unary input length.
The selected goal is OAI.ExactQuantumFactoring.exact_quantum_factoring. Its central assertion is
The theorem states that the defined proposition MainTheorem holds, i.e. there is a family of quantum circuits indexed by input bit length ℓ with three properties. Circuits are lists of instructions on q qubits, each applying one of 20 named gates (the primitives NOT, CNOT, Toffoli, Hadamard and phase, each optionally inverted and optionally given one extra control) to distinct wires; the output state is obtained by applying the instructions in order to the basis state holding the binary digits of N, least significant bit first, on the first ℓ wires, with all other wires zero. First, the family is uniform: a single Turing machine (TM2) with finite stack alphabets computes in polynomial time the encoding of the ℓth circuit from the unary string of length ℓ, where the encoding writes the qubit count, instruction count and each instruction's gate code, inverse and control flags and wire indices in unary. Second, the numbers of qubits and of instructions of the ℓth circuit are both bounded by one fixed polynomial in ℓ with natural-number coefficients. Third, for every ℓ and every integer N ≥ 2 whose binary length is exactly ℓ, the circuit has at least ℓ + n² qubits, where n = max(128, ℓ), and the total squared amplitude on basis states whose output is correct equals exactly 1. A basis state is correct if reading n consecutive blocks of n bits after the input wires, each block as a binary number, gives the nondecreasing list of prime factors of N with multiplicity, padded with zeros to length n.
The output is a sorted list of prime factors with multiplicity in fixed binary blocks, padded with zeros. The target is an existence theorem for a uniform circuit family, not an uploaded executable factoring program. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Uniform generation, polynomial qubit and gate bounds, a fixed finite gate alphabet, and probability-one correctness must all hold together.
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.Parallel repetition is useful for amplifying errors in nonlocal games, but a joint entangled strategy can correlate outcomes across repetitions. Independence of the sampled questions does not imply independence of wins. The pinned manuscript supplies the research context.
A finite two-player game has a probability distribution on question pairs and a Boolean acceptance predicate. Its entangled value is a supremum over finite-dimensional states and local positive-operator measurements.
The selected goal is OAI.ThresholdParallelRepetition.threshold_parallel_repetition. Its central assertion is
The theorem states that there is a universal constant κ₀>0 such that the following holds for every two-player nonlocal game G with question sets of sizes x+1 and y+1 and answer sets of sizes a+1 and b+1, given by a probability distribution on question pairs and a Boolean acceptance predicate on questions and answers, whose entangled value is strictly less than 1. Here the entangled value is the supremum of the winning probability over finite-dimensional entangled strategies, which consist of a unit state on a bipartite space, positive semidefinite measurement operators for Alice and Bob summing to the identity for each question, with answer probabilities given by the Born rule. For every δ with 0<δ<1−entangledValue(G) and every number of repetitions k≥1, consider k-fold parallel repetition, where k independent question pairs are drawn from G's distribution and the players answer all coordinates at once. The threshold probability of a repeated entangled strategy S is the probability that the number of coordinates won is at least ⌈(entangledValue(G)+δ)k⌉. The theorem asserts that this probability is at most exp(−κ₀ δ¹³ k /(1+ln((a+1)(b+1)))) for every repeated strategy S, and that the threshold value, defined as the supremum of the threshold probability over all repeated strategies, satisfies the same bound. The statement is admitted without proof in the source.
The selected published Lean exponent is δ^13, not the manuscript abstract's δ^5 or its distribution-dependent cubic rate. Both every-strategy and supremum conclusions are included. 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 estimate must hold uniformly over finite dimensions and collective strategies. Taking the supremum cannot assume that an optimal strategy exists.
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.The parity function tests whether a shallow quantum circuit can combine information from all input bits. Polynomially many ancillary qubits make the measured-output formulation substantially stronger than a restriction to clean final registers. The pinned manuscript supplies the research context.
Allowed gates are arbitrary one-qubit unitaries and Toffoli gates with finitely many controls. Gates within a layer have disjoint supports. Inputs occupy the first n qubits, with zero ancillas.
The selected goal is OAI.QAC.parity_lower_bound_polynomial_size. Its central assertion is
The theorem states that, for any positive integers d, k and C, there is a threshold n₀ such that for every n ≥ n₀ and every total qubit count N with n ≤ N ≤ C(n+1)^k, the following holds. Take any circuit given as a list of at most d physical layers on N qubits, where a layer is a list of gates with pairwise disjoint supports and each gate is either a one-qubit unitary on a single qubit or a Toffoli gate with an arbitrary finite set of control qubits and a target outside that set (flipping the target exactly when all controls are 1). The circuit's matrix is the product of the layer matrices, with the first layer acting first. For every choice of output qubit out among the N qubits, there exists an n-bit input x such that successProbability, the total Born probability over all final computational-basis strings y whose out-th bit equals the parity (sum mod 2) of x, is strictly less than 2/3. Here the input state is x placed on the first n qubits with all remaining qubits set to 0, and the remaining qubits are summed over with no requirement that they be clean. So fixed-depth circuits with polynomially many qubits cannot compute parity with worst-case success probability at least 2/3. The theorem is admitted in the source (proof is sorry).
The published goal fixes success threshold 2/3 and positive integer depth, polynomial exponent and coefficient. It does not state the manuscript's full range of positive advantages. 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 bound covers arbitrary gates, all choices of output qubit and polynomially many total qubits. Discarded registers can retain unrestricted garbage.
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.Positive partial transpose imposes strong constraints on quantum maps, but composition may retain entanglement. Explicit finite-dimensional examples make that distinction a precise algebraic target. The pinned manuscript supplies the research context.
The selected maps act on complex 10 by 10 matrices. Complete positivity is quantified over matrix amplifications, while separability is expressed by finite sums of positive tensor factors.
The selected goal is OAI.DimensionTen.main_pair. Its central assertion is
The theorem states that there exist maps Φ₁ and Φ₂ from 10×10 complex matrices to 10×10 complex matrices, equal to the defined maps phiOne and phiTwo, each of which is PPT, meaning complex-linear, completely positive, and such that composing with the transpose of the output is also completely positive (complete positivity means that applying the map to one factor of any positive semidefinite block matrix on ℂᵏ⊗ℂ¹⁰, for every k≥1, yields a positive semidefinite matrix). Here phiOne sends A to the 6×6 matrix obtained from the transpose of A by embedding it as a symmetric tensor in ℂ⁴⊗ℂ⁴, applying the tensor square of an explicit 4×4 pencil map built from four integer 6×4 blocks, and compressing to the antisymmetric subspace, then padding it to a 10×10 matrix in the first six coordinates. phiTwo is the Hilbert–Schmidt adjoint of an associated complementary map, which uses a Hodge-type complement matrix, applied to the compression of its input onto the first six coordinates. Moreover, letting Z be the Choi matrix of the composition Φ₂∘Φ₁, a 100×100 matrix with entries given by the images of the matrix units, Z is nonzero; no nonzero product vector u⊗v with u,v∈ℂ¹⁰ lies in the range of Z, that is, whenever Z applied to some w∈ℂ¹⁰ˣ¹⁰ equals u⊗v then u=0 or v=0; and Φ₂∘Φ₁ is not entanglement breaking, where entanglement breaking means completely positive and sending every positive semidefinite amplification to a separable matrix, a finite sum of Kronecker products of positive semidefinite matrices. This theorem is admitted in the source, not proved.
The selected target is the explicit pair of PPT maps in dimension ten, including its nonzero Choi matrix and product-vector obstruction. It does not state a secret-key distillation theorem. The separate 21-dimensional channel is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
PPT properties and non-entanglement-breaking composition require different certificates. The range condition must exclude every nonzero product vector.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.
At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.
The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is
The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.
The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. 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 bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.
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.
Additional published targets are included as separate references:
OAI.Laughlin.mainTarget_proved (Open).OAI.LaughlinFock.thm_fock (Open).OAI.Laughlin.planar_gap (Open).adc7f1241b42. Selected goal source.Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.
A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.
The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is
The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.
The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.An exterior electron count defines a radius of a neutral atom without selecting individual electrons. Its scaling tests how well Thomas–Fermi theory describes the outer region of the full interacting atom. The pinned manuscript supplies the research context.
Choose any normalized ground state for each neutral atom with N+1 electrons. The radius is the infimum of radii outside which the expected electron mass is at most m.
The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is
The theorem states that, for every choice of wavefunctions Ψ_N for neutral atoms with N+1 electrons and nuclear charge Z=N+1 (each a spin-dependent complex function of N+1 positions in three-dimensional space, with spins taking two values), such that each Ψ_N is a normalized ground state, the outer radii of the atoms obey a Thomas–Fermi-type scaling law. A normalized ground state is an antisymmetric wavefunction with a weak gradient, square-integrable in each spin component together with its gradient, with finite Coulomb integrals against |Ψ|², total squared norm 1 summed over spins, and minimal energy among all such normalized functions. The energy is half the squared L² norm of the gradient plus the expectation of the Coulomb potential, which is −Z times the sum of inverse distances of electrons to the nucleus plus the sum of inverse inter-electron distances over pairs. The electron density is N+1 times the spin-summed integral of |Ψ|² over the other N positions, and the radius for m is the infimum of r≥0 such that the density mass outside the ball of radius r is at most m. For each m, upperRadius and lowerRadius are the limsup and liminf, in the extended reals, of these radii as N→∞ with N+1>m. With bTF=(81π²/2)^(1/3), the theorem states that both m^(1/3)·upperRadius(m) and m^(1/3)·lowerRadius(m) converge to bTF as m→∞ through the natural numbers.
The target uses extended-real upper and lower radii, followed by a natural-number limit in m. No spherical symmetry is assumed, and the atom remains neutral. 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 assertion must hold for every choice of ground states. The inner large-charge limsup and liminf cannot be silently replaced with an assumed pointwise limit.
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.Removing outer electrons changes an atom's energy on a smaller scale than its total binding energy. A total-energy asymptotic alone does not determine the difference. The pinned manuscript supplies the research context.
The quantum model uses antisymmetric spin-dependent wavefunctions, two spin states, weak gradients and the full nuclear and electron-electron Coulomb interactions. The comparison is with the Thomas–Fermi density functional.
The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is
The theorem states that the proposition MainStatement holds: there is a real constant a>0 such that three asymptotic statements about atomic ionization energies all hold with this same a. Here the quantum energy of N electrons around a nucleus of charge Z is the infimum, taken over admissible spin-dependent wavefunctions on (ℝ³)^N, of the energy (1/2) times the total squared L² norm of all gradient components, minus Z times the expectation of Σᵢ 1/|xᵢ|, plus the expectation of Σ_{i<j} 1/|xᵢ−xⱼ|, with energy defined as 0 when N=0. Admissibility means that each spin component and each prescribed gradient component is square integrable, the gradient components are the weak partial derivatives of the values, the values are antisymmetric under simultaneous permutation of spins and positions (by the sign of the permutation, almost everywhere), the total squared norm summed over spins is 1, and the nuclear and electron-electron Coulomb densities are integrable. The ionization energy of removing m electrons from a neutral atom of charge Z is ionization(m,Z)=E(Z, Z−m)−E(Z, Z), with natural-number subtraction. The Thomas-Fermi energy tfEnergy(Z,M) is the infimum over nonnegative integrable densities ρ on ℝ³ of total mass M, with ρ^{5/3}, ρ/|x| and ρ(x)ρ(y)/|x−y| integrable, of (3/10)(3π²)^{2/3}∫ρ^{5/3} − Z∫ρ/|x| + (1/2)∬ρ(x)ρ(y)/|x−y|, and tfIonization(m,Z)=tfEnergy(Z,Z−m)−tfEnergy(Z,Z) for real m and Z. The three conclusions are: for every real m>0, tfIonization(m,Z) tends to a·m^{7/3} as the real number Z tends to infinity; for all natural-number sequences m_j, Z_j with 1≤m_j<Z_j, m_j→∞ and Z_j/m_j→∞, the ratio ionization(m_j,Z_j)/m_j^{7/3} tends to a; and as m→∞ through the naturals, both limsup and liminf over Z of ionization(m,Z), each divided by m^{7/3}, tend to a.
The main proposition includes a positive common constant, the fixed-m Thomas–Fermi limit, the joint quantum limit, and normalized limsup and liminf limits. It concerns energies rather than outer-electron radii. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Errors negligible relative to the total atomic energy can still dominate ionization energies. The common leading constant must work in the joint regime and both iterated limits.
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.Random site energies change the spectral behavior of a lattice Schrödinger operator. Identifying its almost-sure spectrum is one part of the planar Anderson problem. The pinned manuscript supplies the research context.
The lattice is the integer plane. A state is a square-summable complex function on its sites, and the potential at each site is independently uniform on the interval from −h to h, with h positive.
The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is
The theorem states that for every real h>0, for almost every disorder configuration v under disorderLaw(h), there exists a bounded complex-linear operator H on the Hilbert space ℓ²(ℤ², ℂ) of square-summable complex functions on the planar lattice ℤ×ℤ such that H is an Anderson operator for v, H is self-adjoint, and the spectrum of H in ℂ equals the real interval [-4-h, 4+h] (embedded in ℂ as the points with imaginary part 0). Here a configuration is a real-valued function v on lattice sites, and disorderLaw(h) is the infinite product measure over sites of the uniform distribution (Lebesgue measure conditioned on the interval) on [-h,h], so the potential values are independent. H is an Anderson operator for v when, for every u in ℓ² and every site x=(a,b), (Hu)(a,b) = u(a+1,b)+u(a-1,b)+u(a,b+1)+u(a,b-1)+v(a,b)u(a,b), the sum of the four nearest-neighbour values plus the local potential times u at x. The statement is recorded as an admitted theorem.
The selected goal asserts existence, self-adjointness and the spectrum interval. Pure-point spectral type, a complete eigenbasis and dynamical localization are not conclusions of this published 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.
The interval must be identified almost surely for an infinite random operator, including both exclusion of spectrum outside the interval and inclusion of its interior.
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.Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.
A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum , assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.
For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).
The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate 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.
Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.
The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.
The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. 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.