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?
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.
A linear filling inequality captures a form of large-scale negative curvature. The source asks whether a finite aspherical complex with that property must admit a geometric model of local nonpositive curvature. The source is OpenAI's September 2026 manuscript.
A finite complex has its usual barycentric realization. Asphericity means higher homotopy groups vanish. A linear disk-filling inequality bounds triangular face moves needed to fill an edge loop by a constant times its length.
The defined proposition MainStatement holds, namely that there exist a finite abstract simplicial complex K on vertices Fin n, with its standard barycentric realization |K| (nonnegative coordinate vectors summing to 1 supported on a face), a basepoint x in |K|, and a real constant C ≥ 0 such that all of the following hold. |K| is connected and aspherical at x, meaning every homotopy group π_{m}(|K|,x) with m ≥ 2 is trivial. K satisfies a linear disk-filling inequality: every closed edge path p that bounds some disk, where a disk is a chain of elementary moves (collapsing a repeated vertex, removing a spur a,b,a, or replacing a,b,c by a,c across a nondegenerate triangular face, which costs one) reducing p to a single vertex, admits such a disk using at most C times (length of p minus 1) triangular faces. The fundamental group G = π₁(|K|,x) is word hyperbolic in the four-point sense: for some finite generating set S and some δ ≥ 0, every a,b,c,d in G satisfy d(a,c)+d(b,d) ≤ max(d(a,b)+d(c,d), d(a,d)+d(b,c)) + 2δ, where d is word distance. G admits no geometric CAT(0) action: there is no proper cocompact isometric action of G on any nonempty proper complete metric space X (in universe u) that is CAT(0), in the sense that segments exist with the squared-distance comparison inequality. Finally, for every finite complex L whose realization is homotopy equivalent to |K|, there is no metric on |L|, inducing its given topology, that is geodesic and locally CAT(−1), meaning each point has a ball that satisfies the hyperbolic-cosine midpoint inequality cosh d(z,m) ≤ (cosh d(z,x)+cosh d(z,y))/(2cosh(d(x,y)/2)) for segment midpoints m.
The goal is OAI.HyperbolicObstruction.main.
The goal also excludes a finite homotopy-equivalent complex with a compatible geodesic locally CAT(-1) metric. It joins a finite topological model, a group-theoretic obstruction, and a metric-model consequence. 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.
A large-scale hyperbolicity inequality does not directly construct a local curvature metric. Excluding all geometric actions requires more than finding a defect in the original complex’s chosen metric.
Word hyperbolicity uses the four-point word-distance condition. Excluded CAT(0) actions are on nonempty proper complete spaces. The final metric must induce the finite realization’s existing topology; changing that topology is not permitted.
The shared definitions are supplied by HyperbolicObstruction. 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.
Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.
A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.
The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.
The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. 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.
Conjugation obscures the standard generating subsets, so intersecting and alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.
The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.
The shared definitions are supplied by ArtinParabolicIntersections. 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.
Artin presentations often admit useful geometric models of nonpositive curvature. The source constructs a finite presentation designed to obstruct every geometric action on a proper CAT(0) space. The source is OpenAI's September 2026 manuscript.
A geometric action is an isometric group action that is proper and cocompact. CAT(0) is expressed by existence of geodesic segments and Euclidean comparison inequalities. The target uses one explicit Artin matrix on 116 generators.
The following explicit matrix on 116 generators is symmetric, has diagonal entries 1, and has every off-diagonal entry in {2, 3, ∞}, and that its Artin group admits no geometric action on any nonempty proper CAT(0) metric space. Index the generators by 0, …, 115. For each b = 0, 1, 2, form the ordered block (b, (b + 1) mod 3, 5 + 37b, …, 41 + 37b). Distinct generators have matrix entry 3 if they are consecutive in a block; otherwise they have entry 2 if they are nonconsecutive members of a block or one is 3 or 4 and the other is 0, 1, or 2; all remaining entries are ∞. The Artin group has these generators and, for each finite entry n, equates the two alternating words of length n starting with the corresponding generators. Here a CAT(0) space is a geodesic metric space satisfying Euclidean triangle comparison, and proper means that closed balls are compact. The excluded geometric action is an action by isometries such that, for every compact set K, only finitely many group elements g satisfy gK ∩ K ≠ ∅, and some compact set has translates covering the whole space. Thus, for every nonempty proper metric space and every action of this explicitly presented group, at least one of the CAT(0), isometry, compact-intersection finiteness, or compact-covering conditions fails.
The goal is OAI.ArtinCAT0.main.
The formal statement verifies the matrix’s structural properties and excludes actions of the resulting explicit group. It does not merely assert that some unspecified Artin group has an obstruction. 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.
Ruling out one candidate complex is insufficient because the conclusion ranges over all nonempty proper metric spaces and actions. The algebraic relations must force a contradiction with geometric-action properties themselves.
The matrix is generated by three overlapping length-39 blocks plus sentinel relations. Properness is compact-intersection finiteness and cocompactness is coverage by translates of a compact set. The action target is universe-polymorphic.
The shared definitions are supplied by ArtinCAT0. 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 classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.
An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.
For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.
The goal is OAI.HarmonicArtin.salvetti_cover_contractible.
The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. 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.
Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.
SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.
The shared definitions are supplied by HarmonicArtin. 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.
Simplicity constrains normal subgroups, amenability provides almost invariant finite sets, and finite presentation gives a finite description by generators and relations. The source seeks an infinite group satisfying all three conditions together. The source is OpenAI's September 2026 manuscript.
A simple group is nontrivial and has no proper nontrivial normal subgroup. Følner amenability means that every finite collection of translations changes a suitable nonempty finite set by a small relative symmetric difference.
There exists a group G, with underlying type in the lowest universe, that is infinite, finitely presented, simple, and Følner-amenable. Here FolnerAmenable(G) is the defined proposition that for every finite subset K of G and every real ε>0 there is a nonempty finite subset D of G such that, for every g in K, the symmetric difference between the left translate gD={g·d : d∈D} and D has cardinality strictly less than ε times the cardinality of D. Simple means G is nontrivial and has no normal subgroups other than the trivial one and G itself, and finitely presented means G has a presentation with finitely many generators and finitely many relations.
The goal is OAI.SimpleAmenable.main.
The target supplies one group with simultaneous infinitude, simplicity, finite presentation, and the specified Følner property. Each condition is part of the conclusion. 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.
Finite generation is weaker than finite presentation, and an amenability argument need not survive an arbitrary quotient or enlargement used to enforce simplicity. The construction must preserve all four properties.
Finite sets are Finsets and translations act on the left. The Følner witness is nonempty and the inequality is strict for every member of the given finite set. No uniform bound on the number of generators or relators is imposed.
The shared definitions are supplied by SimpleAmenable. 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.
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.
Periodic groups have only finite-order elements, but this local condition does not visibly bound the group’s size. The source asks whether an ordinary finite presentation forces such a group to be finite. The source is OpenAI's September 2026 manuscript.
A periodic group satisfies: for each element there is some positive power equal to the identity. A Steinberg group is generated by elementary root symbols subject to additive, commuting, and multiplicative commutator relations over a coefficient ring.
Two propositions hold together. For a natural number n and a ring R, a root is an ordered pair (i,j) of distinct indices in {0,…,n−1}, and the Steinberg group St(n,R) is the group generated by symbols x_{ij}(a), one for each root (i,j) and each a in R, subject to three families of relations: x_{ij}(a+b) = x_{ij}(a)x_{ij}(b); the commutator [x_{ij}(a), x_{kl}(b)] = x y x⁻¹ y⁻¹ is trivial whenever j≠k and i≠l; and for pairwise distinct i, j, k, the commutator [x_{ij}(a), x_{jk}(b)] equals x_{ik}(ab). A group is periodic if every element g has some positive integer m with gᵐ = 1. The first statement, MainStatement, asserts that there exist a ring R in the lowest universe, carrying an algebra structure over ZMod 2, such that St(12,R) is infinite, finitely presented, and periodic. The second statement, BurnsideStatement, asserts that there exists an infinite, finitely presented, periodic group G. The theorem asserts the conjunction of these two existence claims, with no bound on the orders of elements.
The goal is OAI.SourceBurnside.thm_main.
The formal goal includes both this ring-based construction and the general existence of an infinite finitely presented periodic group. It preserves the stronger concrete realization through a Steinberg group. 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.
A finite collection of torsion generators does not imply that every product has finite order. Conversely, infinitely many torsion relations do not supply an ordinary finite presentation. Both requirements must hold for the same infinite group.
The orders of elements may vary; no common exponent is asserted. Finite presentation is Mathlib’s group property. The goal does not include the manuscript’s separate nil-algebra, radical-algebra, or unitization conclusions.
The shared definitions are supplied by PeriodicGroup. 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.
The Partition Principle reverses the cardinal comparison provided by a surjection without requiring a section. The source studies whether this weaker form of comparison can hold while full Choice fails. The source is OpenAI's September 2026 manuscript.
The Partition Principle says that a surjection from onto implies an injection from into . Ordinal-indexed Choice provides choices for families indexed by internal ordinals. The formal consistency predicate rules out finite derivations of falsity in a specified first-order proof system.
A relative consistency result in pure first-order set theory with membership and equality: if ZF, meaning the full axioms of extensionality, empty set, pairing, union, power set, infinity and foundation together with every instance of Separation and Replacement for arbitrary formulas with arbitrary parameters, and without Choice, is consistent, then so is the theory obtained by adding three sentences to ZF. Consistency is syntactic: no finite classical natural-deduction derivation of falsity exists from the theory, allowing any finite supply of free variables. The added sentences are the Partition Principle PP, which says that whenever there is a set surjection from X onto Y then there is a set injection from Y into X, with functions coded internally as sets of Kuratowski pairs and the injection not required to be a section of the surjection; the ordinal-indexed Choice axiom ACwo, which says that for every internal von Neumann ordinal (transitive and internally well-ordered by membership) every family of nonempty sets indexed by it has a choice function; and the negation of full Axiom of Choice AC, which says that every set of nonempty sets has a choice function.
The goal is OAI.PartitionConsistency.main_consistency. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen goal is the relative syntactic consistency claim. A separate attached model-construction target gives a transitive extension under its stronger ground-model assumptions. 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.
The function and ordinal notions must be expressed internally in the set-theoretic language. An ambient use of classical choice cannot substitute for satisfaction of the internal Choice sentence.
The source theory includes every Separation and Replacement instance with parameters. The auxiliary model target assumes a countable transitive ground and a standard inaccessible in that ground; it is not presented as an assumption-free construction over arbitrary countable transitive models.
The shared definitions are supplied by PartitionConsistency, PartitionPrinciple. 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.
Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.
A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.
There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).
The goal is OAI.SignedSweeps.signed_occurrence_moment_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. 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.
Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.
The quantifier order is , then each small , then , then each small , then one positive integer . Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.
The shared definitions are supplied by SignedSweepMoment, SpinAngle, 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.