All missions

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.

Motivation

A hypersurface can be abstractly affine space without its defining equation being an ambient coordinate. Distinguishing these two properties is the embedding question behind the Abhyankar–Sathaye problem. The source manuscript presents the surrounding research claim.

Setting

For n ≥ 4, let R=ℂ[X₀,…,Xₙ₋₁]. A polynomial F is a coordinate if a ℂ-algebra automorphism of R sends some variable Xᵢ to F. Its zero fiber is represented by the quotient R/(F).

Formalization target

For every n ≥ 4, find F with

$$R/(F)\cong_{\mathbb C}\mathbb C[X_0,\ldots,X_{n-2}],\qquad F\text{ is not a coordinate}.$$

The source supplies an explicit construction, while this selected goal asks for existence.

The selected formal target is OAI.AbhyankarSathaye.exists_noncoordinate_polynomial.

Significance and status

The target separates the intrinsic affine-space quotient from ambient polynomial equivalence in every dimension at least four. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An isomorphism of the quotient rings need not extend to an automorphism of the ambient ring. Both the quotient isomorphism and the failure of every possible coordinate automorphism must be established.

Formalization scope

The goal uses multivariate polynomials indexed by Fin n, a principal ideal, and ℂ-algebra equivalences. A separate published derivation target and its explicit polynomial definitions are retained as related references. That target concerns n−1 commuting locally nilpotent derivations, their common kernel and ordinary extra-variable partial derivatives; it is not asserted as a logical dependency of the existence goal.

Selected references

• OpenAI, An explicit noncoordinate polynomial with affine three-space zero fibre, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Logarithmic Kodaira dimension measures the supply of pluricanonical forms allowed poles along a boundary. Its behavior in a fibration depends especially on the case where a general fiber has no such nonzero forms. The source manuscript presents the surrounding research claim.

Setting

A stratum-smooth fibration is a surjective connected-fiber morphism of smooth projective complex varieties with reduced simple-normal-crossing boundaries E and D. The pullback of the base boundary is supported in E; the total space and every boundary stratum are smooth away from D.

Formalization target

Very generally on the base, the point lies outside D and every supplied fiber model F satisfies

$$\kappa(F)=-\infty\Longrightarrow\kappa(E)=\kappa(D)+\kappa(F),$$

with every positive-degree logarithmic pluriform section on the total space equal to zero.

The selected formal target is OAI.ReverseLogKodaira.SmoothProjectiveVariety.veryGenerally_fiber_negative_branch.

Significance and status

This is the fiber-negative branch of the manuscript’s wider additivity claim. Its vanishing assertion is part of the goal, not merely explanatory background. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The conclusion concerns all positive tensor degrees and every fiber model over very general points. One fixed fiber or one vanishing space of sections would not suffice.

Formalization scope

The definitions use schemes over ℂ, ideal-sheaf boundaries, exterior powers of Kähler differentials, and rational pluriform lattices. Kodaira dimension takes values in WithBot ℕ∞. Very generally means outside a countable family of proper closed subsets. The nonnegative branches and full reverse inequality are not additional attached targets.

Selected references

• OpenAI, The reverse logarithmic Kodaira inequality and additivity, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A planar prime walk can go around a gap that would block a walk on a line. The Gaussian moat problem therefore asks for an obstruction to every possible bounded-step route through distinct Gaussian primes. The source manuscript presents the surrounding research claim.

Setting

A Gaussian prime is an irreducible element of ℤ[i]. For D ∈ ℝ, two distinct primes are adjacent when their Euclidean distance is at most D. A component contains every prime reachable by a finite path.

Formalization target

Prove the conjunction

$$\text{no injective infinite D-step prime walk exists},\qquad\forall D\;\exists B\;\forall p,\ |\operatorname{component}_D(p)|\le B.$$

The second clause also bounds the length of every finite injective D-step prime chain by B and asserts component finiteness.

The selected formal target is OAI.GaussianMoat.fullMain.

Significance and status

The same B must work for every starting prime at a fixed step bound. The theorem makes no numerical claim about this bound. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Showing that each component is finite does not give a uniform bound across starting points. Every route in two dimensions and primes on the axes remain within the quantification.

Formalization scope

The formal graph uses Mathlib Gaussian integers and complex Euclidean distance. Step bounds range over all real numbers. MainEndpoint and UniformEndpoint are both mandatory clauses of fullMain. Only that published target and its definitions are supplied.

Selected references

• OpenAI, Bounded-Step Walks on Gaussian Primes, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Cubic Gauss sums oscillate even after normalization. Their first moment asks whether this cancellation retains a precise lower-order bias when averaged over arithmetic primes. The source manuscript presents the surrounding research claim.

Setting

Work in the Eisenstein integers ℤ[ω], with ω=exp(2πi/3). A primary prime p is a prime element congruent to one modulo three. N(p)=|p|², G(p) is the normalized cubic Gauss sum, and c*=(2π)^(2/3)/(3Γ(2/3)).

Formalization target

At the real sharp cutoff X, establish

$$\sum_{\substack{p\text{ primary prime}\\N(p)\le X}}G(p)=\frac65c_*\frac{X^{5/6}}{\log X}+o\!\left(\frac{X^{5/6}}{\log X}\right).$$

The two supporting targets compare each fixed angular mode to its explicit model and give cancellation for every nonzero mode.

The selected formal target is OAI.CubicFirstMoment.patterson_firstMoment.

Significance and status

The coefficient and scale specify the first moment, rather than only an order-of-magnitude estimate. Both conjugate prime elements are included when they satisfy the primary-prime predicate. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Pointwise estimates on G(p) do not isolate the X^(5/6)/log X bias. The error must be little-o at that scale with the exact arithmetic normalization.

Formalization scope

The published definitions use residue-class representatives, the cubic residue symbol, the trace exponential phase, and complex-valued cutoff sums. Little-o is taken as real X tends to positive infinity. Angular modes are integers held fixed before the limit.

Selected references

• OpenAI, An unconditional first moment for cubic Gauss sums, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Birational anabelian geometry studies how much of a function field is determined by a small quotient of its absolute Galois group. This mission isolates uniqueness in the reconstruction correspondence. The source manuscript presents the surrounding research claim.

Setting

Fix a prime ℓ. The fields K/k and L/l are essentially finite type extensions of algebraically closed constant fields, have transcendence degree at least two, and have characteristic different from ℓ. The abelian-by-central datum records the pro-ℓ abelian quotient and the commutator pairing. IsomF consists of constant-preserving perfect-closure isomorphisms modulo Frobenius; IsomCUnits quotients bracket-compatible Galois isomorphisms by the encoded ℓ-adic unit relation.

Formalization target

For field-isomorphism classes a and a′ and a Galois-isomorphism class b, prove

$$\operatorname{PhiGraph}(a,b)\;\land\;\operatorname{PhiGraph}(a^{\prime},b)\quad\Longrightarrow\quad a=a^{\prime}.$$

PhiGraph is the relation induced by representatives and a compatible extension to algebraic closures.

The selected formal target is OAI.BogomolovPop.main_graph_injective.

Significance and status

This establishes uniqueness of the field class whenever two representatives produce the same Galois class. The manuscript states a full reconstruction bijection; the selected published Lean target is its graph-injectivity assertion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Equality is required after two different quotient constructions, one generated by Frobenius and one by ℓ-adic scalar limits. Recovering equality of classes must respect both ambiguities and the contravariant Galois action.

Formalization scope

The definition block constructs topological pro-ℓ quotients, closed commutator subgroups, perfect closures and the pullback graph. The theorem quantifies over arbitrary field types with the stated algebraic instances. It does not assert existence, surjectivity or functionality of PhiGraph, and those broader manuscript conclusions are not attached as proved results. Only the existing injectivity target and its definition block are referenced.

Selected references

• OpenAI, The Bogomolov-Pop reconstruction theorem, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Compatibility between reassociation and braiding imposes equations on formal Lie expressions. The question is whether those equations leave precisely the free family of odd-weight generators predicted by the Deligne–Drinfeld conjecture. The source manuscript presents the surrounding research claim.

Setting

Let L be the free Lie algebra over ℚ on x and y, each of weight one. The solution space W satisfies antisymmetry, the three-term relation, and the pentagon equation in the four-strand infinitesimal braid algebra. Its operation is the Ihara bracket {p,q}=Dₚq−D_qp+[p,q]. The free algebra F has generators indexed by k ≥ 0 with weights 2k+3.

Formalization target

Establish a graded bracket-preserving linear equivalence

$$F=\operatorname{Lie}_{\mathbb Q}\langle e_3,e_5,e_7,\ldots\rangle\;\cong\;W,$$

together with mutually inverse continuous maps on the products of weight pieces. The completed maps must preserve the bracket degree by degree, including the finite convolution sum defining its weight-n component.

The selected formal target is OAI.DeligneDrinfeld.main.

Significance and status

The target simultaneously expresses freeness and exhaustion of the full equation space. Finding a free subalgebra alone leaves the exhaustion assertion unresolved. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The pentagon relation couples substitutions in the braid Lie algebra. Constructing odd-weight solutions does not by itself show that all solutions are generated by them, nor that the completed bracket has the required compatibility.

Formalization scope

The published definition block specifies the braid quotient, tangent construction of D, weighted Lie words, rational submodules and product completions. Generator k has weight 2k+3. The factor spaces carry the explicitly supplied discrete topology. The goal is exactly MainStatement, including its inverse, continuity and completed-bracket clauses. The available reference set supplies the definition block and one target, so no unsupported paper lemmas are attached as milestones.

Selected references

• OpenAI, The Deligne-Drinfeld conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.