OAI Math

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

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

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 divergent reciprocal sum is a sparse largeness condition on integers. The mission asks whether it still forces additive structure of every finite length. The source manuscript presents the surrounding research claim.

Setting

For A⊆ℕ, reciprocalTerm(A,n) is 1/n when n∈A and zero otherwise, using Lean’s total real inverse at n=0. A nonconstant arithmetic progression has terms a+i·d with positive integer d.

Formalization target

Prove

$$\sum_{n\in A}\frac1n\text{ is not summable}\quad\Longrightarrow\quad\forall k\in\mathbb N,\ \exists a\in\mathbb N,\ d\in\mathbb N_{>0},\quad a+id\in A\ (i<k).$$

The starting term a is a natural number and is not separately required positive; the step d is strictly positive.

The selected formal target is OAI.Erdos3.manuscriptReciprocalProgressionTheorem.

Significance and status

The selected endpoint is the reciprocal-sum progression theorem. The manuscript’s quantitative bounds for progression-free subsets motivate it but are not supplied as separate published targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Positive density arguments alone do not cover all sets with divergent reciprocal sums. The hypothesis permits sets whose density tends to zero.

Formalization scope

The formal hypothesis is ¬Summable of a real sequence and ranges over all natural-number sets. All natural lengths k are included, including the degenerate zero and one cases. The n=0 summand equals zero and does not affect divergence. No quantitative constants are asserted here.

Selected references

• OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, 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

Euclidean Ramsey theory asks which finite shapes must occur monochromatically in a sufficiently high dimension. The scale is fixed, so an algebraic criterion must capture exact distances rather than approximate similarity. The source manuscript presents the surrounding research claim.

Setting

A Ramsey configuration a=(aᵢ) has a monochromatic congruent copy under every finite coloring in some dimension depending on the number of colors. Let F be the rational field generated by all coordinates, B=F⊗ℚF, and pᵢ=(1,aᵢ) the augmented coordinate vectors. Multiplication m:B→F sends x⊗y to xy.

Formalization target

For an injective configuration of at least two points affinely spanning ℝᵈ with d≥1, prove

$$\operatorname{Ramsey}(a)\iff\operatorname{FieldCriterion}(a).$$

The criterion asks for a matrix P over B with (pᵢ⊗1)ᵀP(1⊗pᵢ)=0 for every i and m(P_{αβ})=δ_{αβ} on the coordinate-coordinate block.

The selected formal target is OAI.EuclideanRamsey.classification.

Significance and status

The criterion is necessary and sufficient for the stated configurations. Available companion targets describe spherical necessity, positive classes and concrete non-Ramsey circle configurations. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Applying m to the tensor identity loses information because multiplication need not be injective. Equality in the tensor ring, and arbitrary colorings without measurability, are essential.

Formalization scope

The goal uses real Euclidean coordinates and the exact generated intermediate field over ℚ. Congruence preserves all pairwise distances at their original scale. All published companion references are retained as separate groups because they repeat Ramsey definitions. Milestones state their own hypotheses and do not identify every spherical set as Ramsey.

Selected references

• OpenAI, A classification of finite Euclidean Ramsey configurations, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

An oriented graph may have very uneven outdegrees, yet the second-neighborhood conjecture asks for one vertex whose new two-step reach is at least its immediate outdegree. The source manuscript presents the surrounding research claim.

Setting

An oriented graph is a loopless asymmetric relation r on a finite nonempty vertex type. First neighbors satisfy r(v,w). Second neighbors are vertices w distinct from v, not already first neighbors, but reached by some directed path v→u→w.

Formalization target

Prove that some vertex v satisfies

$$|N_1^+(v)|\le|N_2^+(v)|.$$

Every second-neighborhood vertex is counted once, irrespective of how many two-step paths reach it.

The selected formal target is OAI.SeymourSecondNeighborhood.exists_goodVertex.

Significance and status

The statement covers all finite oriented graphs, including disconnected graphs and graphs whose underlying undirected graph is not complete. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Counting length-two walks overcounts repeated endpoints and may include first neighbors. The conclusion concerns the set of vertices at directed distance exactly two.

Formalization scope

The formal relation need not be supplied with decidability; the finite sets are formed classically. Looplessness and asymmetry are explicit hypotheses, and the vertex type is finite and nonempty. GoodVertex is exactly the finite-cardinality comparison.

Selected references

• OpenAI, A proof of Seymour’s second-neighborhood conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.

Setting

A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size $s$ costs $p^s$. An ordinary cover and a fractional cover both have budget $1/2$; a fractional cover assigns weights in $[0,1]$ and supplies total weight at least one inside each member. The expectation thresholds $q$ and $q_f$ are suprema of feasible parameters in $[0,1]$.

Formalization targets

$$q_f(\mathcal F)\le 25\cdot512^4\,q(\mathcal F).$$

For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.

The goal is OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence.

Significance

The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. 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

Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.

Formalization scope

The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.

The shared definitions are supplied by TalagrandExpectationThreshold. 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, Integral and fractional expectation thresholds are equivalent, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

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

A spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.

Setting

A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.

Formalization targets

$$G\text{ finite, simple, cubic, bipartite, planar, and 3-vertex-connected}\ \Longrightarrow\ G\text{ has a Hamiltonian cycle}.$$

Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.

The goal is OAI.Barnette.main.

Significance

A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.

Formalization scope

The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.

The shared definitions are supplied by BarnetteHamiltonian. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Paired states and Hamiltonian cycles in cubic bipartite planar graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.

Setting

An independent set contains no adjacent pair. Write $n$ for the number of vertices, $d=2|E|/n$ for average degree, and $α(G)$ for the largest independent-set size. A graph is clique-free of order $r$ when it contains no $r$ pairwise adjacent vertices.

Formalization targets

$$\forall r\ge4\ \exists c_r>0:\quad \alpha(G)\ge c_r\frac{n\log d}{d}\qquad(d\ge2,\ G\text{ is }K_r\text{-free}).$$

For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.

The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.

Significance

The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.

Formalization scope

The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis $d\ge2$ keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.

The shared definitions are supplied by CliqueFreeLog. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A logarithmic independence bound for clique-free graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Finite matroid packing and covering principles connect disjoint spanning sets with independent covers. The source seeks a concrete obstruction to extending the unrestricted principle to infinite ground sets. The source is OpenAI's September 2026 manuscript.

Setting

A matroid records independent subsets and their closure. A packing/covering partition divides the common ground set into a part with disjoint spanning sets in restrictions and a part covered by independent sets in contractions. Self-duality means equality with the dual on the same labelled ground set.

Formalization targets

$$\exists M_0,M_1\text{ on a countably infinite }E:\quad M_i^*=M_i,\quad I_0\cup I_1\ne E\text{ for every independent pair},\quad\neg\operatorname{HasPackingCovering}(M_0,M_1).$$

The ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.

The goal is OAI.InfiniteMatroidCounterexample.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• partitional intersection counterexample.
• separate covering packing counterexamples.

Significance

The goal simultaneously supplies a countable infinite example, failure of a full independent cover, and failure of every mixed partition. Additional attached statements treat partitional matroids, intersection, and the separate packing and covering assertions. 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

Failure of a full independent cover does not by itself exclude a mixed partition. The matroids must satisfy the infinite independence axioms, including maximal extension, throughout the construction.

Formalization scope

The ground type is the fixed product of integers with finite Boolean-function data. Mathlib matroids have ground set equal to the entire type in the goal. The two source definition groups have overlapping declarations and remain separate reference groups, with no aggregate import.

The shared definitions are supplied by InfiniteMatroid, InfiniteMatroidCorollaries. 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, A Counterexample to the Infinite Matroid Packing/Covering Conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The Heilbronn triangle problem asks how large the smallest triangle in an $n$-point set can be. A positive improvement in the exponent would contradict bounds at every scale arbitrarily close to $n^{-2}$. The source is OpenAI's September 2026 manuscript.

Setting

Points lie in the closed unit square in the real plane. Triangle area is half the absolute determinant of the two displacement vectors, and the lower-bound condition quantifies over all triples of distinct points.

Formalization targets

$$\delta>0,\quad n_j\to\infty,\quad |P_j|=n_j\ge3,\quad\min_{p,q,r\in P_j\text{ distinct}}\operatorname{Area}(pqr)\ge n_j^{-2+\delta}.$$

The Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).

The goal is OAI.Problem355.heilbronn_power_lower_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• almost n minus two refuted.

Significance

The formal goal gives an unbounded sequence of configurations with a fixed explicit power improvement. An attached companion target rules out an eventual almost-$n^{-2}$ upper bound at half that exponent. 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

Avoiding collinear triples is insufficient: every nonzero triangle must also satisfy one uniform quantitative area bound. The exponent must stay positive independently of the size of the configuration.

Formalization scope

The selected goal asserts a sequence tending to infinity, rather than the stronger all-sufficiently-large-sizes statement in the manuscript. The explicit exponent is heilbronnExponent, built from fixed binomial coefficients. Finite sets eliminate repeated points; real powers specify the area scale.

The shared definitions are supplied by HeilbronnTriangle. 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, A power improvement in the Heilbronn triangle lower bound, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The linear Fourier coefficients measure a Boolean function’s correlation with individual inputs. The source studies whether their sum can be controlled solely by the square root of the function’s real polynomial degree. The source is OpenAI's September 2026 manuscript.

Setting

A Boolean function here takes values in $\{-1,1\}$ on a finite sign cube. Fourier coefficients use the uniform distribution. The Fourier degree is the largest support size of a nonzero coefficient; it is unrelated to degree over a field of characteristic two.

Formalization targets

$$\forall C>0\ \exists f:\quad\sum_i\widehat f(\{i\})>C\sqrt{\deg f},\qquad \left\{\frac{\sum_i|\widehat f(\{i\})|}{\sqrt{\deg f}}:\deg f>0\right\}\text{ is unbounded above}.$$

Two things about real Fourier analysis on Boolean cubes, where a Boolean input is read as a sign (false is +1, true is -1), averages are uniform, and degree is the ordinary real Fourier degree, meaning the largest size of a subset s with nonzero Fourier coefficient, the coefficient being the average of f(x) times the product of the signs of the coordinates in s. First, SignedViolations holds: for every real C>0 there is a positive integer n and a function f from {false,true}^n to the reals that takes only the values -1 and 1, is nonconstant, and satisfies C·√(deg f) < Σᵢ f̂({i}), the plain signed sum of its degree-one Fourier coefficients over single coordinates. Second, the set of ratios (Σᵢ |f̂({i})|)/√(deg f), taken over all positive n and all Boolean-valued f on n coordinates with positive Fourier degree, is not bounded above in the reals, so the supremum of these ratios is infinite.

The goal is OAI.SquareRootDegree.main.

Significance

Both signed violations and unbounded absolute ratios are retained. The result concerns failure of every constant multiple, which is stronger than exhibiting one violation of a proposed constant-one inequality. 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

A large ambient dimension is not itself a violation: the denominator depends on degree. The function must remain Boolean and nonconstant while its linear coefficient sum outgrows that denominator.

Formalization scope

Inputs are Fin n → Bool, with false interpreted as $+1$ and true as $-1$. The first clause requires positive dimension and a nonconstant function. The second restricts to positive Fourier degree and uses ¬ BddAbove, avoiding a real-valued infinity convention.

The shared definitions are supplied by SquareRootDegree. 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, Unbounded Violations of the Square-Root Degree Bound, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.