OAI Math

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

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

Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.

Setting

Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.

Formalization target

Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with

$$c_1(W)\ge\exp\!\left(c\sqrt{\log d\,\log\log d}\right).$$

The selected formal target is OAI.TreeEdit.binary_lower_bound.

Significance and status

The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.

Formalization scope

The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.

Selected references

• OpenAI, Tree Constructions for the l1 Distortion of Binary Edit Distance, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Cylinder covers measure coverage cost by perpendicular base area. For a regular tetrahedron, the familiar half-minimum-shadow threshold is tested by a finite family of tilted triangular cylinders. The source manuscript presents the surrounding research claim.

Setting

The reference tetrahedron K has coordinates (x,y,√2t) with 0≤t≤1, |x|≤1−t and |y|≤t. Let H=√2 and A_min be its least unit-direction projection area. A triangular cylinder has a compact nondegenerate triangle in the plane perpendicular to its unit axis.

Formalization target

Prove A_min=H and construct, for every sufficiently small ε>0, 2⌈2/ε²⌉ cylinders covering K with

$$\frac{\sum_i|B_i|}{H}=\frac12-\frac{13}{6000}\varepsilon^2+O(\varepsilon^4),\qquad\sum_i|B_i|<\frac{A_{\min}}2.$$

Also prove existence of a finite cover with Σᵢ|Bᵢ|/shadowArea(uᵢ)<1/2.

The selected formal target is OAI.TriangularCovering.main.

Significance and status

The asymptotic estimate retains its explicit quadratic coefficient and uniform fourth-order error. Both absolute area and directionwise normalized cost are formal conclusions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Tilting may reduce projected area but leave uncovered gaps. The target requires exact finite coverage and valid triangular bases together with the strict cost saving.

Formalization scope

Base area is two-dimensional Euclidean Hausdorff measure converted to ℝ. MainAsymptotic has fixed positive δ,C before all small ε. The broad fourPaperMain is retained as a related published reference; the selected goal remains TriangularCovering.main. Repeated definitions in independent source groups are kept separate.

Selected references

• OpenAI, Finite angular cylinder covers below the half-area bound, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A continuously varying family of line segments suggests a low-cost cylinder cover, but a finite approximation must control both gaps and accumulated base area. The source manuscript presents the surrounding research claim.

Setting

A ruled set consists of segments (s,p+sv(p)) with p in a compact planar label set D and |s|≤L. The basic weighted projection cost is ∫_D(1+|v(p)|²)^(-1/2)dp. The source also defines physical rescalings, square intercept tiles and singular slope fields.

Formalization target

Prove the published FullMain conjunction. Its central finite-approximation clause gives

$$\sum_i |B_i|\le\int_D\frac{dp}{\sqrt{1+|v(p)|^2}}+\varepsilon$$

for every ε>0 under its C¹ hyperbolicity hypotheses. The package additionally contains physical-rescaling, logarithmic, product-cell, orthogonal-grid, smooth nilpotent and singular-tetrahedron assertions.

The selected formal target is OAI.RuledApproximation.fullMain.

Significance and status

The chosen goal supplies a package of finite-cover results with explicit regularity and base-shape requirements. The broad fourPaperMain reference also contains a C¹ nilpotent variant. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Freezing directions can create gaps and a persistent area loss. The final family must be finite and cover every point while the area error is arbitrarily small.

Formalization scope

FullMain uses Euclidean planes and three-space. Some clauses require null-measure boundary or C² regularity; its NilpotentStatement requires smoothness and a square-zero derivative. The singular clause includes its stated p,γ ranges and strict tetrahedron cost below √2/2. These are the selected published clauses; the manuscript’s latest C¹ formulation is not silently substituted for them. Independent definition groups remain separate references.

Selected references

• OpenAI, Finite cylinder approximation of ruled sets, 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

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

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

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

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

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

Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.

Setting

States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.

Formalization target

Prove

$$\tau_{TV}(1/4)\le2n^8,$$

with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).

The selected formal target is OAI.Problem315.switch_chain_main.

Significance and status

The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.

Formalization scope

The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.

Selected references

• OpenAI, Polynomial mixing of the switch chain for every graphical degree sequence, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.