All missions

Motivation

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.

Setting

On Bernoulli product space $2^{[N]}$, each coordinate is present independently with probability $p$. For a family $D$, the exceptional family $E_k(D)$ consists of sets contained in no union of $k$ members of $D$. A family is $p$-small when it has containment generators with total cost at most $1/2$.

Formalization targets

$$\mu_p(D)\ge1-2^{-75}\quad\Longrightarrow\quad E_{2^{75}}(D)\text{ is }p\text{-small}.$$

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.

Significance

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.

Difficulty

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.

Formalization scope

Lean uses finite families of finite subsets of Fin N, with $N\ge1$ and $0<p<1$. A tuple has exactly $2^{75}$ 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.

Selected references

• OpenAI, Talagrand’s discrete-convexity conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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.

Setting

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.

Formalization target

For every m,n>0, prove there is a drawing with exactly

$$Z(m,n)=\left\lfloor\frac m2\right\rfloor\left\lfloor\frac{m-1}2\right\rfloor\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor$$

crossing points, and every admissible drawing has at least Z(m,n) crossings.

The selected formal target is OAI.Zarankiewicz.mainTarget_proof.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, The crossing number of complete bipartite graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For n≥3, prove

$$\operatorname{cr}(K_n)=\frac14\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor\left\lfloor\frac{n-2}2\right\rfloor\left\lfloor\frac{n-3}2\right\rfloor.$$

The selected formal target is OAI.Paper170.complete_graph_crossing_number.

Significance and status

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.

Difficulty

An explicit drawing establishes only an upper bound. The equality also requires a bound valid for all admissible topological drawings.

Formalization scope

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.

Selected references

• OpenAI, The crossing number of complete graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Construct a positive-size finite simple host G with at least one edge such that

$$t(H,G)<p(G)^{66},\qquad p(G)=\frac{2|E(G)|}{|V(G)|^2}.$$

The selected formal target is OAI.SidorenkoCounterexample.main.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, A counterexample to Sidorenko's conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove one integer C≥1 works for every finite nonempty simple graph:

$$\chi_{list}(G)\le C\,h(G).$$

The constant is chosen before the graph, the vertex type and all color lists.

The selected formal target is OAI.LinearListHadwiger.main_theorem.

Significance and status

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.

Difficulty

A coloring from one chosen palette need not respect independently assigned lists. The proof must cover arbitrary color types and list assignments.

Formalization scope

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.

Selected references

• OpenAI, A linear list-coloring bound in terms of the Hadwiger number, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

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

$$\min\{d:\text{an integer tile without a periodic complement exists in }\mathbb Z^d\}=3.$$

The selected formal target is OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality.

Significance and status

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.

Difficulty

Excluding periodic integer translation sets does not automatically exclude Euclidean tilings with noninteger shifts. The latter universal quantifier is a separate clause.

Formalization scope

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.

Selected references

• OpenAI, A translational tile with no fully periodic tiling in dimension three, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Construct a system satisfying

$$T\text{ is ergodic},\qquad h_{KS}(T)<\infty,\qquad T\text{ has no smooth positive-volume model}.$$

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.

Significance and status

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.

Difficulty

Failure of a particular embedding does not exclude all measure-theoretic conjugacies and all dimensions. Conjugacy is allowed after discarding invariant null sets.

Formalization scope

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.

Selected references

• OpenAI, A zero-entropy system without a smooth positive-volume model, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Construct q>0 and such a nonbijective f with

$$h_{top}(f)=0,\qquad\exists v\in H_2(M;\mathbb R)\setminus\{0\},\ f_*v=2v,$$

and prove 0<log 2≤log ρ_total(f), with 5≤2q+3.

The selected formal target is OAI.Problem340.exists_C1_entropy_counterexample.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, A C^1 Counterexample to the Entropy Conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove

$$\exists k_0>0\;\forall k\ge k_0,\qquad h_{area}(T_k)>0.$$

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.

Significance and status

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.

Difficulty

Large derivatives in some regions do not establish positive metric entropy for area measure. The claim concerns long-term orbit statistics with possible cancellations.

Formalization scope

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.

Selected references

• OpenAI, Positive Metric Entropy for the Standard Map at Large Parameters, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For the least query budget q(d) achieving total-variation error at most 1/10, prove

$$\forall\varepsilon>0\;\exists C,\quad q(d)\le Cd^\varepsilon\quad(d\ge2),$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Subpolynomial query complexity for well-conditioned log-concave sampling, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For every n≥4, construct one n-state witness A for that language such that every complement automaton B satisfies

$$|Q_B|\ge\frac12\,2^{\lfloor(n-4)/127\rfloor}-1.$$

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.

Significance and status

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.

Difficulty

The lower bound ranges over every finite state type and every competing automaton. Producing one inefficient complement construction would not establish it.

Formalization scope

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.

Selected references

• OpenAI, An exponential state lower bound for two-way nondeterministic complementation, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For n≥1 and 1≤d≤n, prove

$$\operatorname{AS}(\operatorname{sign}p)\le8d\sqrt n$$

for every multilinear p of total degree at most d.

The selected formal target is OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Average sensitivity of polynomial threshold functions, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove that every positive real power is eventually exceeded:

$$\forall C>0\;\exists n_0\ge4\;\forall\text{ even }n\ge n_0,\qquad n^C<\operatorname{psdRank}(n).$$

The separate lift target gives the same superpolynomial lower bound for every exact affine PSD lift.

The selected formal target is OAI.PerfectMatchingPSD.main.

Significance and status

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.

Difficulty

Factors are unrestricted real PSD matrices, with no rank-one or symmetry requirement. Lower bounds for nonnegative rank alone do not rule them out.

Formalization scope

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.

Selected references

• OpenAI, Exponential PSD rank of positively shifted matching matrices, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

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

$$\dim H,\quad|\operatorname{encode}(H)|,\quad\operatorname{time}(H)\le C(n+s+1)^k,$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Polynomial Hitting Lists for Noncommutative Rational Formulas, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For all n,s≥1, every characteristic-zero field F and every formula f of size at most s, prove

$$f\ne0\quad\Longrightarrow\quad f(T_1,\ldots,T_n)\ne0,$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, One Rational Matrix Hitting Point for Noncommutative Formulas, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For every labeled matroid, construct a distribution-independent rule and seed law such that every prefix is feasible and, for every measurable arrival permutation,

$$\mathbb E[\operatorname{reward}]\ge2^{-310}\mathbb E[\operatorname{OPT}].$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove dim(ambient)=23, p(e)=1, and

$$p\text{ is homogeneous of degree }20,\qquad\deg p=20,$$

with every line polynomial real-rooted. For every N>0 and linear symmetric pencil L, prove

$$\operatorname{cone}(p,e)\ne\{x:L(x)\succeq0\}.$$

The selected formal target is OAI.Paper256.main_result.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, A nonspectrahedral hyperbolicity cone, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

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

$$cn\log n\le A_n\le Cn\log n\qquad(n\ge n_0).$$

The selected formal target is OAI.CoveringOrder.optimal_order.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Translative covering densities of order n log n, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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).

Formalization target

Establish one absolute constant C>0 with

$$\forall n\ge2\;\forall K,\quad\exists L,\quad K+L=\mathbb R^n,\qquad\frac{|K|}{\operatorname{covol}(L)}\le Cn\log n.$$

The lattice may depend on K and n.

The selected formal target is OAI.SingleLatticeCovering.single_lattice_covering.

Significance and status

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.

Difficulty

A union of a few lattice cosets is not itself the required single lattice. Density control must accompany exact coverage of every point.

Formalization scope

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.

Selected references

• OpenAI, A single-lattice covering bound of order n log n, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For n≥1, prove the equality classification

$$|K|\,|K^\circ|=\frac{4^n}{n!}\quad\Longleftrightarrow\quad K\text{ is a linear Hanner body}.$$

The lower-bound inequality is retained as a separate supporting target.

The selected formal target is OAI.SymmetricMahler.symmetric_mahler_equality.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, The symmetric Mahler conjecture and its equality cases, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

For every 0<η<1, construct a compact E⊆[0,1] with

$$|E|>1-\eta,\qquad\forall x\in\mathbb R\;\forall s\ne0\;\exists n\ge1,\quad x+s2^{-n}\notin E.$$

The same E must avoid every translation and both signs of dilation.

The selected formal target is OAI.Problem310.dyadic_affine_avoidance.

Significance and status

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.

Difficulty

Excluding a countable collection of copies does not handle the continuum of scales and centers. Finite initial segments cannot replace the entire sequence.

Formalization scope

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.

Selected references

• OpenAI, The dyadic case of the Erdős similarity conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove

$$\forall\eta>0\;\exists N_0\ge1\;\forall N\ge N_0\;\exists\varepsilon,\quad\sup_{|z|=1}|P_N(z)|\le(1+\eta)\sqrt N.$$

All sufficiently large integer lengths are required, rather than a subsequence.

The selected formal target is OAI.AsymptoticallyMinimalLittlewood.main.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, Asymptotically minimal maxima of real Littlewood polynomials, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

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.

Setting

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.

Formalization target

Prove that there exist real ε and C with 0<ε<1/4 such that

$$M(-1,f,r)\le C(1-r)^{-1/4+\varepsilon}$$

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.

Significance and status

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.

Difficulty

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.

Formalization scope

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.

Selected references

• OpenAI, A strict inverse-first-power bound for univalent functions, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

The size of the derivative of a conformal map can concentrate near a domain boundary. Brennan-type integrability and inverse-square integral means quantify how severe that concentration can be. The source manuscript presents the surrounding research claim.

Setting

A schlicht function is an injective holomorphic map f on the unit disk with f(0)=0 and f′(0)=1. M(f,t,r) is the circle average of |f′|ᵗ at radius r, and B(t) is the supremum of the associated extended-real boundary growth exponents.

Formalization target

Prove the four-part MainStatement, including

$$M(f,-2,r)\le C_\varepsilon(1-r)^{-1-\varepsilon},\qquad B(-2)=1,$$

uniformly for schlicht f and 1/2 ≤ r < 1. For conformal bijections φ:W→𝔻 on the specified simply connected domains, prove area integrability of |φ′|ˢ for 4/3<s<4; for univalent disk maps prove integrability of |f′|ᵗ for −2<t<2/3.

The selected formal target is OAI.Brennan.main_theorem.

Significance and status

The goal packages the uniform circle bound, exact spectrum value and both area-integrability formulations. A separate endpoint target records sharp failure for the Koebe map and its inverse. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A growth bound with a constant depending on f does not supply the stated uniform estimate. Boundary behavior must also support the precise open exponent intervals.

Formalization scope

Planar Lebesgue area, a left-hand limit r→1, and extended-real spectra are fixed. W must be open, connected, simply connected and have nontrivial spherical boundary. Main and sharp-endpoint definitions are independent published groups with repeated names, so references coexist without one aggregate import.

Selected references

• OpenAI, Brennan's conjecture and sharp inverse-square integral means, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Algebraic ampleness and positivity of a smooth Hermitian metric are different kinds of positivity for a vector bundle. The target asks for one concrete family where they separate. The source manuscript presents the surrounding research claim.

Setting

The quadric surface is ℙ¹×ℙ¹. Rank-two algebraic bundles are specified by principal affine charts and regular 2×2 transition matrices. For a bundle G, E(m) is its coordinatewise m-th-power pullback twisted by the polarization O(1,1).

Formalization target

Construct G and a family E(m) such that

$$m>0\Longrightarrow E(m)\text{ is ample},\qquad m\ge m_0\Longrightarrow E(m)\text{ has no strictly Griffiths-positive smooth metric},$$

for one positive integer m₀, with the required pullback-twist identities for every positive m.

The selected formal target is OAI.QuadricCounterexample.main_theorem.

Significance and status

The assertion compares two precise positivity conditions on the same family. The goal is existential and does not provide a numerical threshold m₀. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Proving ampleness supplies projective sections, whereas excluding every positive metric is a quantified differential-geometric obstruction. Testing one candidate metric cannot settle nonexistence.

Formalization scope

The reference defines ℙ¹ as the one-point compactification of ℂ, bundles by cocycles, ampleness through symmetric sections giving a closed projective embedding, and strict positivity by a matrix Hessian expression. SourceMainTheorem retains all of these conventions. Only the published definition block and target are attached.

Selected references

• OpenAI, Ample rank-two bundles on the quadric surface without Griffiths-positive metrics, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.