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?
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.A divergent reciprocal sum is a sparse largeness condition on integers. The mission asks whether it still forces additive structure of every finite length. The source manuscript presents the surrounding research claim.
For A⊆ℕ, reciprocalTerm(A,n) is 1/n when n∈A and zero otherwise, using Lean’s total real inverse at n=0. A nonconstant arithmetic progression has terms a+i·d with positive integer d.
Prove
The starting term a is a natural number and is not separately required positive; the step d is strictly positive.
The selected formal target is OAI.Erdos3.manuscriptReciprocalProgressionTheorem.
The selected endpoint is the reciprocal-sum progression theorem. The manuscript’s quantitative bounds for progression-free subsets motivate it but are not supplied as separate published targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Positive density arguments alone do not cover all sets with divergent reciprocal sums. The hypothesis permits sets whose density tends to zero.
The formal hypothesis is ¬Summable of a real sequence and ranges over all natural-number sets. All natural lengths k are included, including the degenerate zero and one cases. The n=0 summand equals zero and does not affect divergence. No quantitative constants are asserted here.
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.Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.
States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.
Prove
with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).
The selected formal target is OAI.Problem315.switch_chain_main.
The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.
The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.
adc7f1241b42. Goal source.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.Configuration linear programs relax bin packing by allowing fractional combinations of feasible bins. The mission asks whether the integral optimum can stay within any universal additive constant of this relaxation. The source manuscript presents the surrounding research claim.
A bin-packing instance lists rational item sizes in (0,1]. Feasible bins have total load at most one. The formal development specifies both an individual-item configuration LP and a type-based configuration LP, plus binary encodings of instances, assignments and reductions.
For every natural c, construct I and B with 5B items of sizes strictly between 1/6 and 1 such that
Also prove NP-hardness of every fixed additive packing gap, existence of a polynomial-time absolute-additive algorithm iff P=NP, and the specified exact algorithm consequences under P=NP.
The selected formal target is OAI.BinPackingGap.main_results.
The goal combines unbounded relaxation gaps with a complexity characterization of constant-additive approximation. Item sizes above 1/6 force every bin to hold at most five items. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A large LP gap does not by itself supply NP-hardness. The reduction must have the stated completeness and soundness while preserving the explicit encoding and item-size constraints.
Reductions are finite-alphabet polynomial-time machines from every encoded NP language. The P=NP consequence includes exact optimal bin count, the canonical empty-instance answer and rejection of malformed or invalid input. All clauses of main_results are retained.
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.Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.
For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.
Prove the strict bound
The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.
The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.
Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.
Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.
adc7f1241b42. Goal source.Mean-payoff games ask which starting positions allow a player to guarantee a nonnegative long-run average reward. Binary-encoded weights make the bit cost of solving the complete winning set a central part of the question. The source manuscript presents the surrounding research claim.
A game is a finite nonempty directed multigraph with integer edge weights, an owner for each vertex and an outgoing edge everywhere. Winning means that a history-dependent maximizer strategy guarantees liminf average payoff at least zero against every opponent strategy.
Construct one randomized three-tape machine and C>0 such that every encoded game of length L has a time bound
all T-bit random tapes halt by T, and at least 7/8 of them output the exact winning-set indicator, with all other output cells blank.
The selected formal target is OAI.randomized_quasipolynomial_mean_payoff.
The target makes the input encoding, computation model, success fraction and complete output explicit. It is an existence theorem for a uniform machine, not a separate solver for each game. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The running time must hold on every random tape, while correctness holds on the specified fraction. Signed weights and the full binary input length cannot be replaced by unary magnitude bounds.
The published definitions specify games, strategies, plays, liminf payoffs, serialization and tape transitions. The independent finite Truffet elimination counterexample is retained as contextual reference; it is not a prerequisite or an asserted proof of the randomized algorithm. The manuscript’s certification/always-correct consequence is not an additional attached goal.
adc7f1241b42. Goal source.A slope-field perturbation of a two-cylinder cover trades a reduction in projected area against the extra overlap needed to maintain coverage. The slope-field manuscript studies when the net cost becomes strictly smaller. The companion radial-sweep manuscript establishes finite triangular approximation with arbitrary tagged equal subdivisions. Both manuscripts map to the same published Lean goal, so this draft covers their shared target. The source manuscript presents the surrounding research claim.
A cylinder is a measurable finite-area planar base plus a line in its perpendicular unit direction. Ruled sets vary the segment direction over compact planar labels. Radial sweeps use p₀+ρ(a+tb)+s(e+w(t)), with 0≤ρ≤R(t), |s|≤L, and w′(t)=λ(t)(a+tb).
Prove the seven-part fourPaperMain conjunction: the explicit angular-area construction; C¹ hyperbolic approximation; C¹ square-zero-derivative approximation; regular-tetrahedron counterexamples with parallelogram bases and with bounded open bases; aligned radial triangular approximation; and actual-sweep projection bounds. In particular, the tetrahedron clauses require
The selected formal target is OAI.CylinderCovering.fourPaperMain.
The selected published goal is a joint endpoint shared by four related manuscripts, and therefore includes more than the slope-field application alone. Its finite covers retain both cost inequalities. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A local area decrease cannot guarantee a global cover. All regularity, exact coverage and error bounds in the separate conjuncts must hold in their stated regimes.
Hyperbolic and nilpotent clauses use their C¹ definitions; radial data require a nonempty parameter interval, positive segment half-length, continuous nonnegative cap and alignment derivative. All tagged equal subdivisions are covered. The radial clause requires triangular-base area to converge to weightedArea(D), while actual sweep projections have eventual cost at most weightedArea(D)+ε and the corresponding limsup bound. The separate RuledApproximation.fullMain is also retained as a related reference but is not mislabeled as one of these seven conjuncts.
adc7f1241b42. Goal source.A continuously varying family of line segments suggests a low-cost cylinder cover, but a finite approximation must control both gaps and accumulated base area. The source manuscript presents the surrounding research claim.
A ruled set consists of segments (s,p+sv(p)) with p in a compact planar label set D and |s|≤L. The basic weighted projection cost is ∫_D(1+|v(p)|²)^(-1/2)dp. The source also defines physical rescalings, square intercept tiles and singular slope fields.
Prove the published FullMain conjunction. Its central finite-approximation clause gives
for every ε>0 under its C¹ hyperbolicity hypotheses. The package additionally contains physical-rescaling, logarithmic, product-cell, orthogonal-grid, smooth nilpotent and singular-tetrahedron assertions.
The selected formal target is OAI.RuledApproximation.fullMain.
The chosen goal supplies a package of finite-cover results with explicit regularity and base-shape requirements. The broad fourPaperMain reference also contains a C¹ nilpotent variant. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Freezing directions can create gaps and a persistent area loss. The final family must be finite and cover every point while the area error is arbitrarily small.
FullMain uses Euclidean planes and three-space. Some clauses require null-measure boundary or C² regularity; its NilpotentStatement requires smoothness and a square-zero derivative. The singular clause includes its stated p,γ ranges and strict tetrahedron cost below √2/2. These are the selected published clauses; the manuscript’s latest C¹ formulation is not silently substituted for them. Independent definition groups remain separate references.
adc7f1241b42. Goal source.Cylinder covers measure coverage cost by perpendicular base area. For a regular tetrahedron, the familiar half-minimum-shadow threshold is tested by a finite family of tilted triangular cylinders. The source manuscript presents the surrounding research claim.
The reference tetrahedron K has coordinates (x,y,√2t) with 0≤t≤1, |x|≤1−t and |y|≤t. Let H=√2 and A_min be its least unit-direction projection area. A triangular cylinder has a compact nondegenerate triangle in the plane perpendicular to its unit axis.
Prove A_min=H and construct, for every sufficiently small ε>0, 2⌈2/ε²⌉ cylinders covering K with
Also prove existence of a finite cover with Σᵢ|Bᵢ|/shadowArea(uᵢ)<1/2.
The selected formal target is OAI.TriangularCovering.main.
The asymptotic estimate retains its explicit quadratic coefficient and uniform fourth-order error. Both absolute area and directionwise normalized cost are formal conclusions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Tilting may reduce projected area but leave uncovered gaps. The target requires exact finite coverage and valid triangular bases together with the strict cost saving.
Base area is two-dimensional Euclidean Hausdorff measure converted to ℝ. MainAsymptotic has fixed positive δ,C before all small ε. The broad fourPaperMain is retained as a related published reference; the selected goal remains TriangularCovering.main. Repeated definitions in independent source groups are kept separate.
adc7f1241b42. Goal source.Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.
Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.
Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with
The selected formal target is OAI.TreeEdit.binary_lower_bound.
The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.
The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.
adc7f1241b42. Goal source.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.