Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.
An independent set contains no adjacent pair. Write for the number of vertices, for average degree, and for the largest independent-set size. A graph is clique-free of order when it contains no pairwise adjacent vertices.
For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.
The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.
The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. 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 condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.
The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.
The shared definitions are supplied by CliqueFreeLog. 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 spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.
A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.
Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.
The goal is OAI.Barnette.main.
A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. 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.
Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.
The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.
The shared definitions are supplied by BarnetteHamiltonian. 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.
High probability under independent coordinate sampling need not give a family any closure under unions. Discrete convexity asks whether a bounded number of its members nevertheless cover most sets in the stronger sense of inexpensive containment certificates. The source is OpenAI's September 2026 manuscript.
On Bernoulli product space , each coordinate is present independently with probability . For a family , the exceptional family consists of sets contained in no union of members of . A family is -small when it has containment generators with total cost at most .
For every positive integer N, every density p with 0<p<1, and every family D of subsets of the ground set {0,...,N-1} (an arbitrary family, with no monotonicity assumption), if the product measure of D under independent Bernoulli(p) coordinates, namely the sum over s in D of p^|s|(1-p)^(N-|s|), is at least 1 - 1/2^75, then the family of exceptional sets is small. Here the exceptional family for k=2^75 consists of all subsets S of the ground set that are contained in no union of k members of D, where the k members are given as an arbitrary tuple of exactly k entries of D, repeats allowed and with no disjointness required. A family A is small at density p if there is a family G of generator sets that covers A, meaning every member of A contains some member of G, and whose cost, the sum over I in G of p^|I|, is at most 1/2.
The goal is OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity.
The conclusion supplies explicit containment witnesses at the original density. A small probability for the exceptional event alone would not provide such a cover. 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 family is arbitrary, so monotonicity cannot be used as an extra hypothesis. The same universal number of unions must work for all dimensions and all densities strictly between zero and one.
Lean uses finite families of finite subsets of Fin N, with and . A tuple has exactly entries; repetitions and overlaps are allowed. The cover cost counts each generator once. The separate two-union density-loss corollary is outside this goal.
The shared definitions are supplied by TalagrandDiscreteConvexity. 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.
Drawing all edges between two vertex classes creates unavoidable intersections. The Zarankiewicz target asks for the exact best crossing count with both part sizes variable. The source manuscript presents the surrounding research claim.
The complete bipartite graph has vertex type Fin m⊕Fin n and one edge for every pair in Fin m×Fin n. Admissible plane drawings use simple continuous arcs, distinct vertices, finitely many proper double crossings and no triple crossings.
For every m,n>0, prove there is a drawing with exactly
crossing points, and every admissible drawing has at least Z(m,n) crossings.
The selected formal target is OAI.Zarankiewicz.mainTarget_proof.
The formal target includes both an attaining drawing and the universal lower bound. Small positive part sizes remain in scope. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The best known construction alone cannot establish optimality. The lower bound must allow arbitrary continuous edge arcs and repeated crossings of a pair of edges.
Proper intersections use local coordinate-axis charts. Counted objects are crossing points, not merely pairs of edges that meet. The formula is implemented by axisPairs(r)=(r/2)((r−1)/2) in natural arithmetic. Tangencies, overlaps and triple crossings are excluded by the drawing model.
adc7f1241b42. Goal source.The complete graph forces many crossings in any plane drawing. The mission seeks the exact ordinary crossing number rather than one drawing’s upper bound. The source manuscript presents the surrounding research claim.
An admissible drawing uses distinct vertex points and injective continuous edge paths whose interiors avoid vertices. Intersections are finitely many proper double crossings, with no triple crossing. Every crossing point is counted, including repeated meetings of a pair of edges.
For n≥3, prove
The selected formal target is OAI.Paper170.complete_graph_crossing_number.
The target fixes the exact minimum across the full continuous-drawing class. It does not restrict edges to straight segments or impose a special layout. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An explicit drawing establishes only an upper bound. The equality also requires a bound valid for all admissible topological drawings.
The graph uses ordered endpoint pairs with increasing indices. Proper crossings are defined through local open partial homeomorphisms taking the two traces to coordinate axes. The ordinary crossing number is the natural infimum of crossing counts; hill uses natural subtraction and division. The selected theorem starts at n=3.
adc7f1241b42. Goal source.Graph homomorphism inequalities compare the frequency of a fixed pattern with what edge density predicts. The mission asks for one finite host graph violating the proposed bound for a specified bipartite pattern. The source manuscript presents the surrounding research claim.
The pattern H is the incidence graph between thirteen points and twenty-two explicitly listed triples, giving thirty-five vertices and sixty-six edges. Homomorphism density counts all edge-preserving maps, including noninjective maps, divided by the number of all vertex maps.
Construct a positive-size finite simple host G with at least one edge such that
The selected formal target is OAI.SidorenkoCounterexample.main.
The counterexample uses the exact supplied pattern rather than an unspecified bipartite graph. A finite host makes the density comparison an ordinary finite counting statement. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The required strict inequality concerns all homomorphisms, not only embeddings. The host must have an edge so the assertion cannot be replaced by a zero-density degeneracy.
H is built from the published table of twenty-two triples. Hosts use Fin size, and both graph counts and real density normalizations are fixed. The manuscript’s forcing-conjecture consequence is not an attached formal target.
adc7f1241b42. Goal source.List coloring permits each vertex to have different allowable colors. The mission asks whether the size of the largest clique minor still controls the required list size up to a universal linear factor. The source manuscript presents the surrounding research claim.
A clique minor of order t is represented by disjoint connected vertex sets, with an edge between every pair. The Hadwiger number h(G) is the largest possible t. The list chromatic number is the least k for which every assignment of at least k colors per vertex admits a proper selection.
Prove one integer C≥1 works for every finite nonempty simple graph:
The constant is chosen before the graph, the vertex type and all color lists.
The selected formal target is OAI.LinearListHadwiger.main_theorem.
The assertion controls list coloring rather than only a common-color-set chromatic number. It is a linear-factor statement, without coefficient-one optimality. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A coloring from one chosen palette need not respect independently assigned lists. The proof must cover arbitrary color types and list assignments.
The definitions use finite graph vertex types, arbitrary finite color sets, induced-subgraph connectivity and natural-number infima/suprema. Nonemptiness of the vertex type is explicit. Only the main inequality and its definition block are attached.
adc7f1241b42. Goal source.A tile may admit a translation tiling while forcing every such tiling to lack a full lattice of periods. The mission asks for this phenomenon in dimension three and its persistence under Euclidean thickening. The source manuscript presents the surrounding research claim.
A finite nonempty integer tile T⊆ℤᵈ tiles with complement A when addition T×A→ℤᵈ is bijective. Full periodicity means invariance under a finite-index subgroup. The thickening is the union of closed unit cubes based at T; Euclidean tiling means unique covering almost everywhere.
Construct T⊆ℤ³ that tiles but has no fully periodic complement, and whose thickening tiles ℝ³ but has no complement invariant under any full-rank lattice. Also prove
The selected formal target is OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality.
The goal includes both discrete and arbitrary-real-translation Euclidean assertions, plus minimality among all natural dimensions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Excluding periodic integer translation sets does not automatically exclude Euclidean tilings with noninteger shifts. The latter universal quantifier is a separate clause.
Discrete tilings are exact bijections, whereas Euclidean tilings are almost-everywhere unique representations relative to Lebesgue measure. Euclidean full periodicity uses the integer span of a real basis. Closed-cube overlaps are handled by the almost-everywhere convention.
adc7f1241b42. Goal source.A measure-preserving system may have low information production yet fail to admit a smooth realization. The target asks for a single ergodic system excluding every finite-dimensional smooth positive-volume model. The source manuscript presents the surrounding research claim.
The system is a measurable equivalence T of a standard nonatomic probability space. Standard nonatomic is expressed by an isomorphism with the unit interval after removing null sets. A smooth model is a compact smooth manifold, a smooth diffeomorphism and an invariant probability measure with strictly positive smooth local coordinate density.
Construct a system satisfying
The formal finite-entropy predicate requires every finite-partition entropy rate to converge, with one finite real upper bound.
The selected formal target is OAI.SmoothObstruction.main.
The obstruction ranges over every finite dimension, nonorientable manifolds and positive-dimensional smooth boundary models. The manuscript asserts zero entropy; the selected published theorem requires finite entropy only. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Failure of a particular embedding does not exclude all measure-theoretic conjugacies and all dimensions. Conjugacy is allowed after discarding invariant null sets.
The goal quantifies over measurable equivalences and uses conull measurable conjugacy, not topological conjugacy. Entropy is measured in bits by the supplied finite-partition definition. Closed models include dimension zero, boundary models require positive dimension, and no orientation hypothesis is imposed.
adc7f1241b42. Goal source.Topological entropy measures orbit complexity, whereas the induced map on homology measures algebraic growth. The mission asks for a C¹ self-map where these two measurements violate the proposed entropy lower bound. The source manuscript presents the surrounding research claim.
The counterexample manifold is S¹×(S²)^(q+1), realized as a product of standard Euclidean spheres. A C¹ self-map is continuous and locally agrees, through the standard embedding, with a C¹ ambient map. Real singular homology provides the induced linear action.
Construct q>0 and such a nonbijective f with
and prove 0<log 2≤log ρ_total(f), with 5≤2q+3.
The selected formal target is OAI.Problem340.exists_C1_entropy_counterexample.
The spectral-radius gap is an explicit conclusion, supported by an eigenvalue-two homology class. The target concerns noninvertible C¹ maps. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Algebraic expansion in homology must coexist with zero topological orbit entropy. Merely displaying a low-entropy subsystem would not establish zero entropy on the whole manifold.
The goal uses Dynamics.coverEntropy on the entire manifold, taking values in EReal. Its total homological spectral radius is defined through real pairs representing complex eigenvalues over all homology degrees. The manifold family, ambient-extension C¹ condition and nonbijectivity are fixed parts of the statement.
adc7f1241b42. Goal source.The standard map is a concrete area-preserving torus system whose global chaotic behavior is difficult to infer from local stretching. The target asks for positive metric entropy along an entire large-parameter tail. The source manuscript presents the surrounding research claim.
On (ℝ/ℤ)², the standard map is T_k(x,y)=(x+y+k sin(2πx),y+k sin(2πx)). The reference area is the product circle-volume measure. Metric entropy is defined from finite measurable partitions and their iterated block distributions.
Prove
The entropy-complete companion additionally asserts positive largest Lyapunov behavior and its equivalence with entropy positivity; the component target describes positive-area hyperbolic Bernoulli components.
The selected formal target is OAI.StandardMapEntropy.main_entropy.
The chosen goal is the central entropy statement with all sufficiently large positive parameters. A positive-measure subset of parameters would not meet this quantifier. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Large derivatives in some regions do not establish positive metric entropy for area measure. The claim concerns long-term orbit statistics with possible cancellations.
Circle period is one, so the sine uses 2πx. Entropy takes values in ENNReal and is a supremum over finite measurable partitions. Lyapunov and component source groups have independent repeated definitions and remain separate references. The simpler entropy goal is selected as the stable central endpoint.
adc7f1241b42. Goal source.Sampling costs can be measured by potential and gradient queries independently of the computation between them. This model isolates the information needed for a well-conditioned log-concave distribution. The source manuscript presents the surrounding research claim.
The admissible potentials V on ℝᵈ are C², satisfy V(0)=0 and ∇V(0)=0, and have Hessian between I and 2I. Their Gibbs law has density proportional to exp(−V). A measurable adaptive algorithm receives exact (V(x),∇V(x)) replies.
For the least query budget q(d) achieving total-variation error at most 1/10, prove
plus q(d)≥c log d eventually for some c>0, and optimal dimension exponent γ*=0.
The selected formal target is OAI.LogConcaveSampling.exact_source_main.
The target gives both a subpolynomial upper bound and a logarithmic lower bound. It leaves computation between queries unrestricted. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The sampler must work uniformly across every admissible potential and use a deterministic query budget on every execution. A dimension-dependent condition number or merely expected budget would change the problem.
Algorithms have measurable query/output maps driven by private randomness and finite transcripts. Query complexity lies in ℕ∞, retaining infeasibility as infinity. Total variation is the specified supremum-style bound on measurable sets, and the upper/lower comparisons use ENNReal.
adc7f1241b42. Goal source.Allowing a finite automaton to move its head in both directions complicates the state cost of language complement. A lower bound independent of alphabet size must handle alphabets that grow with the witness. The source manuscript presents the surrounding research claim.
A two-way nondeterministic automaton has a finite state set, two endmarkers and left/stay/right moves. Acceptance is the existence of a finite run reaching an accepting state. The witness alphabet consists of relations on Fin(n−2), and its language tests whether their ordered product is nonempty.
For every n≥4, construct one n-state witness A for that language such that every complement automaton B satisfies
For n≥131, every deterministic automaton for the same language must satisfy the corresponding bound without the minus one.
The selected formal target is OAI.TwoWayComplementation.explicit_family_main.
Both bounds concern the same explicit-language witness. The goal includes determinization as well as complementation, while the companion target isolates the complement bound. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The lower bound ranges over every finite state type and every competing automaton. Producing one inefficient complement construction would not establish it.
Natural-number subtraction and division determine the exponent. Runs start on the left endmarker and may have length zero. Tape positions remain inside the marked input. The relation alphabet is finite but grows with n. Source groups redeclaring the automaton model remain independent.
adc7f1241b42. Goal source.Average sensitivity measures how often a Boolean decision changes after one coordinate flip. For polynomial threshold rules, a degree-sensitive estimate limits the total influence of all coordinates. The source manuscript presents the surrounding research claim.
A polynomial threshold function evaluates a real multilinear polynomial p on the uniform cube {−1,1}ⁿ, then applies sign with sign(0)=1. Average sensitivity is the sum, over coordinates, of the fraction of cube vertices whose output changes under that flip.
For n≥1 and 1≤d≤n, prove
for every multilinear p of total degree at most d.
The selected formal target is OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement.
The constant is uniform in both dimension and degree. The formal target is the asymptotic Gotsman–Linial estimate with its explicit coefficient eight. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A separate estimate for fixed degree would not establish the bound uniformly as d varies with n. Zeros of p on the cube must respect the specified tie convention.
The cube is Fin n→Bool and coordinates are converted to ±1. Multilinearity is a support predicate on Mathlib multivariate polynomials, and the degree condition is explicit. General polynomial reduction to multilinear form is not an additional attached theorem.
adc7f1241b42. Goal source.Semidefinite representations may be smaller than linear descriptions of a polytope. Lower bounds for their matrix size require a factorization obstruction that applies to arbitrary positive-semidefinite factors. The source manuscript presents the surrounding research claim.
For even n, columns are perfect matchings of the complete graph. Rows comprise edges and odd vertex subsets. The unshifted slack matrix has edge-incidence entries and odd-cut entries |M∩δ(U)|−1. Its real PSD rank is the least positive r admitting trace products of positive-semidefinite r×r factors.
Prove that every positive real power is eventually exceeded:
The separate lift target gives the same superpolynomial lower bound for every exact affine PSD lift.
The selected formal target is OAI.PerfectMatchingPSD.main.
The selected formal goal excludes polynomial-size factorizations. The manuscript dated October 5 states exponential bounds for positively shifted matching matrices; that stronger shifted statement is not the existing published target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Factors are unrestricted real PSD matrices, with no rank-one or symmetry requirement. Lower bounds for nonnegative rank alone do not rule them out.
The target concerns the full unshifted row set and uses real exponentiation with C fixed before n₀. The affine-lift companion quantifies over affine sections and affine images of PSD cones. Independent definition groups are retained separately. The description deliberately makes no exponential or positive-shift claim for these references.
adc7f1241b42. Goal source.Inversion gates create domains of definition as well as nonzero-value conditions. A rational hitting list must find a point where every inverse exists and where the final value is invertible. The source manuscript presents the surrounding research claim.
A noncommutative rational formula over ℚ has variables, constants, sums, ordered products and inverse gates, with tree-node size. Evaluation is a relation requiring genuine two-sided inverses. Admissible means defined at some positive-dimensional rational matrix tuple; nonzero means one such defined value is nonzero.
Construct one deterministic finite-state Turing machine and positive integers C,k which, on unary n,s≥1, outputs a list H of common positive-dimensional rational tuples with
and every admissible nonzero size-s formula has a defined invertible value at some tuple in H.
The selected formal target is OAI.RationalHitting.main.
The output-length bound controls the full binary representation, including rational entries and all tuples. No separate inverse-depth or coefficient-height parameter is added. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A tuple detecting one rational expression may encounter a singular inverse in another. Definedness and invertibility must be guaranteed at a list point for every eligible formula.
Matrices and constants are rational; scalars use the algebra map. The fixed TM0 alphabet and state space, self-delimiting binary output and unary parameter input are explicit. The matrix dimension is shared across the entire list and required positive.
adc7f1241b42. Goal source.Testing a noncommutative polynomial at scalar points can lose its ordered-word structure. Matrix evaluation preserves noncommutativity and permits a single prescribed tuple to test an entire bounded-size formula class. The source manuscript presents the surrounding research claim.
A division-free formula has scalar and variable leaves and addition or ordered multiplication gates. Its size counts every tree node. Nonzero means that at least one coefficient of its word series is nonzero. The published generator is an explicit tuple of rational matrices depending only on n and s.
For all n,s≥1, every characteristic-zero field F and every formula f of size at most s, prove
where the rational tuple T is coerced into F and has dimension 2ns², except for the specified one-variable size-one case.
The selected formal target is OAI.NCHitting.universal_hitting.
One tuple is universal for the whole size class and every characteristic-zero coefficient field. The formal goal establishes its hitting property. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Nonzero word coefficients must survive the same matrix substitution uniformly across all formulas. Choosing a point separately for each f would reverse the required quantifiers.
Formula coefficients are defined by word convolution; evaluation uses scalar matrices and the explicit rational generator. The theorem asserts nonzero matrix output, not invertibility. The manuscript’s deterministic construction-time claim is not a separate statement in this selected Lean target.
adc7f1241b42. Goal source.Online selection must commit before all values arrive, while the offline optimum sees the full vector. The mission asks how much one independent sample per item can recover under a matroid feasibility constraint. The source manuscript presents the surrounding research claim.
A matroid on Fin n specifies feasible independent subsets. An online rule sees the full initial sample vector, a finite random seed and the arriving label/value prefix. Sample and value coordinates are jointly independent, corresponding marginals agree, and the seed is independent of all of them.
For every labeled matroid, construct a distribution-independent rule and seed law such that every prefix is feasible and, for every measurable arrival permutation,
The arrival order may depend on all samples, all values and the entire seed. Reward integrability is also required.
The selected formal target is OAI.MatroidProphet.one_sample.
The rule and its seed distribution depend only on the known matroid. The allowed adversary is stronger than an order chosen before the values or random seed are revealed. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Independence of the input coordinates does not imply independence of the adversarial order. The guarantee must survive an order selected with full information while decisions remain irrevocable.
Values are nonnegative almost surely, and only the actual offline optimum is assumed integrable. The hidden-vector target with ratio 2⁻²⁹³ provides an available supporting milestone. The duplicated one-sample formulation and secretary consequence remain references in their independent source group.
adc7f1241b42. Goal source.Hyperbolic polynomials define convex optimization regions through real-rooted line restrictions. A spectrahedral representation would describe the same region by one finite symmetric positive-semidefinite matrix inequality. The source manuscript presents the surrounding research claim.
The formal ambient space consists of two real symmetric 4×4 matrices X,Z and a vector y∈ℝ³. A fixed determinant expression defines a multivariate polynomial p. At e=((I,I),0), the cone consists of x for which every complex root of t↦p(te−x) is real and nonnegative.
Prove dim(ambient)=23, p(e)=1, and
with every line polynomial real-rooted. For every N>0 and linear symmetric pencil L, prove
The selected formal target is OAI.Paper256.main_result.
The formal target rules out every finite homogeneous real symmetric pencil size. It also verifies the algebraic and root properties of its fixed polynomial. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Excluding one determinantal expression is weaker than excluding all matrix-inequality representations of the cone. The final universal quantifier ranges over all positive dimensions and all real linear pencils.
The published Lean formula has asserted degree 20. The manuscript abstract describes degree 16; this draft follows the actual published degree-20 statement rather than substituting the manuscript number. Symmetric matrices use selfAdjoint, and positivity is Matrix.PosSemidef. No affine pencil or projected semidefinite lift is asserted here.
adc7f1241b42. Goal source.The worst covering density over convex bodies measures how much overlap is unavoidable when translations must cover all of space. Comparing unrestricted centers with a single lattice separates two geometric constraints. The source manuscript presents the surrounding research claim.
The translative density θ_T(K) is the infimum of volume(K) times the upper intensity of locally finite covering center sets. Intensity is measured in expanding centered cubes. The lattice density θ_L(K) takes the corresponding infimum over discrete full-rank lattice coverings.
For each of the four suprema Aₙ, over all or centrally symmetric convex bodies and using θ_T or θ_L, prove common positive constants c,C and a threshold n₀ with
The selected formal target is OAI.CoveringOrder.optimal_order.
The selected endpoint asserts the same asymptotic order for all four worst-case quantities. The manuscript’s new translative lower-bound claim is part of this broader packaged endpoint. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A lower bound for lattice centers does not exclude a more efficient nonlattice cover. The unrestricted lower bound ranges over every locally finite covering set.
The definitions retain extended nonnegative real densities and suprema, so a finite upper bound also asserts finiteness. Central symmetry may have any center. The theorem concerns suprema over bodies, not a lower bound on every individual body.
adc7f1241b42. Goal source.Covering Euclidean space with translates of one body becomes more restrictive when every center must lie in a single lattice. The mission asks for a density bound with the optimal-order n log n shape claimed in the manuscript. The source manuscript presents the surrounding research claim.
A convex body is compact and convex with nonempty interior. A full lattice L is a discrete integer submodule spanning the real coordinate space. It covers by K when K+L=ℝⁿ, and its covering density is volume(K)/covolume(L).
Establish one absolute constant C>0 with
The lattice may depend on K and n.
The selected formal target is OAI.SingleLatticeCovering.single_lattice_covering.
The centers form one full-rank lattice. The target includes no symmetry or boundary smoothness assumption on K. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A union of a few lattice cosets is not itself the required single lattice. Density control must accompany exact coverage of every point.
The formal theorem explicitly supplies DiscreteTopology L and IsZLattice ℝ L in addition to the integer submodule. It uses Mathlib lattice covolume, real volume and the natural logarithm. Dimension starts at two, and the universal C is chosen before K and n.
adc7f1241b42. Goal source.The volume of a symmetric convex body multiplied by the volume of its polar is unchanged by invertible linear coordinates. Its extremizers are therefore classified up to linear equivalence. The source manuscript presents the surrounding research claim.
For an origin-symmetric compact convex K⊆ℝⁿ with nonempty interior, the polar body K° consists of p with Σpᵢxᵢ≤1 for every x∈K. Hanner bodies are generated from centered nondegenerate intervals by products and convex joins; linear Hanner bodies also allow invertible linear images.
For n≥1, prove the equality classification
The lower-bound inequality is retained as a separate supporting target.
The selected formal target is OAI.SymmetricMahler.symmetric_mahler_equality.
The goal identifies every equality case, not only one minimizing example. The manuscript’s inequality and equality assertions appear as distinct published statements. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Showing that the recursively constructed examples attain the value gives only one implication. The reverse implication must classify arbitrary symmetric convex bodies, including nonpolyhedral inputs.
Points are functions Fin n→ℝ and polarity uses the coordinate dot product. Volumes are converted from ENNReal to ℝ in the product. The two definition groups both declare coordinatePolar; they remain separate references rather than an aggregate module.
adc7f1241b42. Goal source.Finite patterns fit inside positive-measure sets after a sufficiently small affine change. The dyadic similarity problem asks whether one particular infinite pattern can be excluded even from compact sets of nearly full measure. The source manuscript presents the surrounding research claim.
The dyadic sequence is D={2⁻ⁿ:n≥1}. Its affine copies are x+sD with arbitrary x∈ℝ and nonzero signed scale s. The ambient measure is Lebesgue measure on the real line.
For every 0<η<1, construct a compact E⊆[0,1] with
The same E must avoid every translation and both signs of dilation.
The selected formal target is OAI.Problem310.dyadic_affine_avoidance.
The result concerns the dyadic sequence specifically, with a stronger near-full-measure conclusion than merely finding one positive-measure avoiding set. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Excluding a countable collection of copies does not handle the continuum of scales and centers. Finite initial segments cannot replace the entire sequence.
The definition dyadicPoint accepts n=0, but the theorem explicitly chooses n≥1. Measure is ENNReal-valued and compares with ENNReal.ofReal(1−η). Compactness and interval containment are required conclusions. General infinite sets are outside this selected target.
adc7f1241b42. Goal source.Choosing real signs in a polynomial controls how much its values can peak around the unit circle. The target seeks asymptotically optimal maximum modulus at every sufficiently large length. The source manuscript presents the surrounding research claim.
A real Littlewood polynomial has consecutive coefficients εₖ∈{−1,1}: P_N(z)=Σₖ₌₀ᴺ⁻¹ εₖzᵏ. The coefficient family may depend on both its length and the requested accuracy.
Prove
All sufficiently large integer lengths are required, rather than a subsequence.
The selected formal target is OAI.AsymptoticallyMinimalLittlewood.main.
The selected target is the uniform maximum-modulus assertion. The companion finite-flatness target gives one sign family whose normalized modulus tends to one in every positive finite Lᵖ moment. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Control at finitely many sample points does not directly give a bound on the full circle. Uniformity in the circle variable and coverage of all large lengths are separate obligations.
Coefficients are real-valued Fin N functions explicitly constrained to ±1 and evaluated as complex polynomials. The companion theorem uses Haar probability on UnitAddCircle and a single family for every p>0. Both independent definition groups are referenced; finite-flatness is a related endpoint rather than a claimed prerequisite.
adc7f1241b42. Goal source.Integral-means spectra record the worst derivative concentration among normalized conformal maps. A strict bound at exponent −1 tests a specific predicted value of that spectrum. The source manuscript presents the surrounding research claim.
For a normalized univalent disk map f, M(−1,f,r) is the average of |f′|⁻¹ on the circle of radius r. The bounded spectrum B_b uses the extended-real limsup growth exponent, then takes its supremum over maps with bounded image.
Prove that there exist real ε and C with 0<ε<1/4 such that
for every normalized univalent f and 1/2≤r<1. Also prove B_b(−1)<1/4 and the failure of the defined Kraetzer prediction to equal B_b at every real exponent.
The selected formal target is OAI.StrictInverseFirstPower.main.
A strictly positive uniform ε is the content of the improvement. The target explicitly includes the spectrum consequence and the negation of the full predicted formula. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An exponent arbitrarily close to 1/4 from above does not give a strict gap below 1/4. The same ε and C must precede the quantification over f and r.
The circle estimate covers all normalized univalent maps, whereas the spectrum uses the bounded-image subclass. Complex derivatives, real interval integrals and EReal suprema are the supplied representations. The prediction is the specified piecewise quadratic/linear function.
adc7f1241b42. Goal source.