Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Add random clauses one at a time to a Boolean formula on variables until it first becomes unsatisfiable. The index of that first failure is the satisfiability hitting time of random -SAT. Its mean, divided by , converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is , but quantitative widths have remained far from the scale suggested by lower bounds. This mission asks for the order of the variance of for every fixed .
The source of this mission is an OpenAI preprint dated September 27, 2026.
Fix and . A proper -clause is an OR of literals on distinct variables; let be independent uniform choices among the signed proper clauses (signs fair, whole clauses may repeat). Put
and, for fixed , the capped hitting time . Since each assignment survives a clause with probability , is a.s. finite with all moments. Write
There are constants with
and for every fixed a constant with ; if then also for large . Hence for . Lean: OAI.RandomKSAT.variance_main, open on the platform.
The killing-probability exponent in the lifetime bound (Proposition 2.3) cannot be decreased, and the block-error term in the replacement lemma cannot be improved to uniformly. Lean: OAI.RandomKSAT.sharpness.
For the theorem determines the variance of the hitting time up to constants, so the transition window has width in the variance sense, matching Wilson's lower bound and improving Carenini's variance bound. For it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of about at scale .
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.
The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter -clauses to its lifetime under -clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.
Clause n k is a dependent pair of a -element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).firstFailure ω is the least with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.blockKill u s S g is the probability that independent proper -clauses kill , and lifetime u k S is .Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.
A random -SAT formula on Boolean variables is a conjunction of independent random clauses, each an OR of literals on distinct variables. As the clause density grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random -SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed the transition happens at a limiting density that does not drift with .
The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.
Fix . For , a proper -clause chooses distinct variables among uniformly and gives each an independent fair sign, so each of the clauses is equally likely. Let be independent such clauses (sampled with replacement: two positions may hold the same clause) and
The ratio is the clause density.
For every fixed integer there is such that
No assertion is made at , and the value of is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.
The theorem settles, for every fixed , the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large (Ding–Sly–Sun) and for . Existence is a prerequisite for questions about the value of , its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
A sharp-threshold theorem gives a narrow window at each but no control of how the window's center moves with . Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.
ProperClause n k is a function Fin n → Option Bool with exactly defined entries; some b at is the literal satisfied when .Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals under the uniform product law.HasLimitingThreshold k asserts with limits for and for at .Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.
A uniform spanning tree of a finite connected graph is a spanning tree chosen uniformly at random. On an infinite graph one takes limits along finite pieces: the free uniform spanning forest (FUSF) is the weak limit of uniform spanning trees of an increasing sequence of finite connected subgraphs, with no boundary identification. Uniform spanning forests connect random walks, electrical networks, determinantal processes and -Betti numbers of groups.
A random object on a graph is a factor of IID if it can be produced by one measurable rule from independent uniform labels on the vertices, in a way that commutes with all graph symmetries. Such representations are the measure-theoretic analogue of local algorithms, and they are central in ergodic theory of group actions. Whether the FUSF is a factor of IID was raised by Lyons at Oberwolfach in 2013, and Timár's 2025 paper describes the unrestricted question as open.
The source of this mission, an OpenAI preprint dated September 25, 2026, proves the unrestricted statement with one rule for all graphs.
Let be an infinite, connected, locally finite, simple, undirected graph. For a finite connected subgraph , let be the uniform law on spanning trees of . For finite connected subgraphs whose edges exhaust , the laws (edges outside absent) converge weakly; the limit on does not depend on the exhaustion (Proposition 2.2).
A rule takes a graph, real vertex labels and an edge. It is equivariant if for every isomorphism , and root independent if it uses no distinguished vertex.
A law on , finite, is strongly Rayleigh if whenever all ; on a countable set, every finite marginal must be strongly Rayleigh.
The Lean statement OAI.Problem336.fusf_is_factor_iid is open on the platform.
Theorem 1.1 answers the FUSF factor question without amenability, transience, unimodularity, degree bounds or moment assumptions, and with a single rule for all graphs; Corollary 1.2 gives the factor statement under every unimodular random graph law. Theorem 1.3 and Corollary 1.4 extend the method to all invariant strongly Rayleigh and determinantal processes on countable groups, addressing the regular-action case of the Lyons–Thom question. The paper asserts an ordinary Borel factor, not a finitary one.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Formalization would also provide uniform spanning trees, the free forest limit, strongly Rayleigh measures and determinantal laws as reusable Lean objects.
Previous constructions use structure that is absent in general: Wilson's algorithm works for the wired forest on transient graphs, and Timár's construction needs monotone limits along a hyperfinite exhaustion. A factor must produce one exact sample of the infinite-volume law while controlling all edges jointly, and equivariance forbids any choice of root or ordering. The paper's route observes the forest through independent Brownian noises and must show that the posterior drift has a uniformly Lipschitz response to the observations even when the fields are unbounded over the graph.
ℕ → ℕ → Bool; edges are pairs ; a connected graph on is automatically infinite. Equivariance is invariance under every permutation of applied to graph, labels and edge.RuleBorel is joint measurability of in the product σ-algebras.IsVertexIID requires the label coordinates to have independent Uniform finite-dimensional laws (with this forces a probability measure).HasFUSFLaw asks that every cylinder probability (edges in present, edges in absent) be the limit of the corresponding uniform-spanning-tree ratio along every exhaustion by finite connected subgraphs covering all edges.ProbabilityMeasure (Γ → Bool), left translation , i.i.d. labels in Set.Icc 0 1 via Measure.infinitePi, and Hermitian kernels with on finitely supported vectors.A complete development needs the matrix-tree theorem and Kirchhoff formulas, weak limits on , Brownian motion and a Borel Picard iteration for the decoder, and the Borcea–Brändén–Liggett theory. Contributions formalizing Proposition 2.2 (free exhaustion limit), Lemma 2.3 (finite-field forest response) and Proposition 4.2 (sampling from independent Brownian paths) are welcome.
Whether identical classical particles in , interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.
Particles live in ; a radial pair potential is a function (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube and ,
The potential is stable if for all configurations. The canonical free energy at density is
The packing constant is , where is the largest number of points in at mutual distance ; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at with the right one strictly smaller, and non-differentiability.
At the single density : there are a bounded continuous stable with for and such that exists for all and
There are a bounded continuous , constants with
an open interval and one such that for every the free energy exists and is finite for every , and
This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.
The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an tail; the fixed power margin here needs a quantitative range estimate not present there.
Formalizing it. The statement fixes the model completely (free boundary conditions on , Lebesgue measure without temperature normalization, , particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.
The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.
EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with , and decay with are separate conjuncts.IsPackingDensity p (a limit), and is required; packingNumber is a sSup over a bounded set of naturals.IsCanonicalFreeEnergy φ ρ f asserts for every , so is determined on ; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.Whether a single species of classical particles in , interacting only through a stable radial pair potential, can undergo a phase transition is one of the long-standing existence questions of rigorous statistical mechanics; it appears in Simon's list of problems in mathematical physics (Simon 1984). A phase transition is detected as a loss of regularity of the thermodynamic free energy. Lattice models and continuum models with extra structure (several species, many-body terms, hard cores, box-restricted interactions) were handled long ago; ordinary pair potentials finite at every positive separation remained the difficult case.
A radial pair potential is on with . It is admissible if is Borel measurable, is finite and locally bounded on , and
With and free boundary conditions, the canonical partition function is
and the canonical free-energy density at density is
In Lean, radialPotential φ takes values in EReal (value ⊤ at the origin), energy is the pair sum, partition φ β L N is the integral above, and HasCanonicalFreeEnergy φ f says for all .
There exist an admissible with as , a free-energy function realizing the canonical limit for every , a nonempty open interval and one such that for every the one-sided -derivatives exist and
This is Theorem 1.1 of the source (MainStatement). The goal is published on the platform with status Open.
The result itself. The theorem exhibits a genuine one-species pair potential, finite at every positive separation and with all cross-cube interactions retained, whose canonical free energy is not in temperature at a fixed density, with one critical temperature for an entire interval of densities. It does not concern the Lennard–Jones potential, does not identify the coexisting states as liquid/vapor/solid, and does not give a power-law tail ; formulations of the historical problem that require such a margin are not resolved by it. A companion preprint (A radial continuum phase transition with algebraic decay) gives a bounded potential with tail .
Formalizing it. The statement is fully explicit about the model, normalization, and boundary conditions, so a formal proof would remove any ambiguity about which version of the problem is solved. It requires thermodynamic limits for superstable continuum systems, convex-analytic facts about pressures, and a Kac/Lebowitz–Penrose comparison with uniform estimates, none of which is currently in Mathlib.
Density coexistence for a grand-canonical system does not by itself produce a temperature corner at a fixed density; one needs two supporting slopes of the pressure with the same density coordinate and different energy coordinates. Classical tools for transitions (Peierls arguments, reflection positivity, Kac limits) either need lattice structure, many-body terms, or a limit in which the potential itself changes. Here a single fixed potential must be built through infinitely many attractions at growing ranges, and the convex supporting-slope information must survive every approximation step while preserving stability and integrable tails.
EuclideanSpace ℝ (Fin 3); the potential is EReal-valued with ⊤ at the origin, and the Boltzmann weight is when the energy is ⊤. Stability is stated in EReal, which also rules out ⊥.Nat.floor; the limit is over real .HasDerivWithinAt on Iic βc and Ici βc, so both are finite real numbers; is pinned by HasCanonicalFreeEnergy for every , so it cannot be chosen freely near .In the low-temperature phase of the Sherrington–Kirkpatrick (SK) spin glass, the Gibbs measure is believed to split into many nearly separated pieces, and local dynamics such as heat-bath (Glauber) updates should take a very long time to move between them. Worst-case slow mixing (some bad starting state) is a weak statement: it says nothing about what happens when the chain is started from a typical equilibrium sample, which is how such chains are used in practice. This mission asks for a much stronger obstruction: for most equilibrium configurations held fixed as starting points, the dynamics is still far from equilibrium after a stretched-exponential time.
The source of this mission is an OpenAI preprint dated September 24, 2026. It covers the entire range , at zero field, for typical rather than worst-case starts.
For and independent standard Gaussians , put
In continuous-time heat-bath dynamics each site has a rate-one clock; when site rings, its spin becomes with probability , where . Let be its kernel and the discrete kernel that resamples one uniformly chosen site. For a fixed start ,
Let . For every fixed ,
The order matters: is drawn from and then held fixed as the starting state. Lean: OAI.SK.main, open on the platform; it writes the joint probability as the disorder average of the Gibbs mass of slow starts.
The theorem shows that throughout the low-temperature phase, a Gibbs-sampled start carries information that local updates cannot erase in time ; in particular (Corollary 1.2) every polynomial time scale is too short from a typical start. This separates the zero-field low-temperature SK model from the high-temperature and large-field regimes, where polynomial mixing holds. The exponent is not claimed to be optimal; numerical studies suggest .
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Integrating the transition kernel over the starting state recovers at every time, so averaging arguments are useless; the obstruction must be established start by start, for a set of starts of Gibbs mass tending to one. Free-energy barrier criteria in the style of Ben Arous–Jagannath do not apply to the pure quadratic SK covariance. The proof needs quantitative Parisi-type comparisons for constrained replica overlaps, and a mechanism ("locking") that forces small overlaps with a third replica to stay put when two replicas overlap substantially.
hamiltonian J x = (∑_{i<j} J_{ij} x_i x_j)/√n; disorderLaw n is the product of standard Gaussians over pairs .heatBath β J x y is the one-step kernel: average over sites of the conditional resampling probability, nonzero only when agrees with off (so holding is included).discreteKernel iterates it; continuousKernel β J t = ∑_k e^{-nt}(nt)^k/k! · K^k, the uniformized rate- chain, equivalent to rate-one clocks per site.continuousBadMass β n and discreteBadMass β n are of the Gibbs mass of starts with distance at time timeScale n = exp(n^κ) (resp. its floor).Infrastructure: finite Markov chains, Gaussian interpolation (Guerra–Talagrand bounds for constrained overlaps), Parisi functional regularity, and Gaussian concentration. The paper's Theorem 2.4 (quantitative free-energy comparison), Proposition 4.4 (absolute-overlap locking) and Proposition 6.1 (stretched-exponential coverage) are natural intermediate targets.
The Sherrington–Kirkpatrick (SK) model is the mean-field spin glass, and is its equilibrium critical point. Physicists expect critical slowing down: at a phase transition, local dynamics needs time growing polynomially in the system size to relax. For the SK model this was studied through linearized mean-field theory, dynamical equations for correlation and response, and simulations of equilibrium autocorrelations on an time scale. Rigorous results on Glauber dynamics had concentrated on high temperature, where mixing is fast. This mission asks for a rigorous total-variation obstruction at : most equilibrium configurations, used as starting states, are still far from equilibrium after time.
The source of this mission is an OpenAI preprint dated September 24, 2026.
At and zero field, let be independent for and
A heat-bath update at site resamples from its conditional law given the other spins. In continuous time every site has an independent rate-one clock (generator ); in discrete time each step updates a uniformly chosen site (kernel ). For a fixed start , and are the total-variation distances to .
For every deterministic with and every deterministic integer ,
Lean: OAI.CriticalSK.realized_equilibrium_initial_states, open on the platform.
With , and : for every , with probability tending to one,
For every fixed ,
with a separate Lean target for the lower bounds alone.
The theorem shows that at criticality the slow direction is visible from typical equilibrium starts, not only from adversarial ones, and pins the time scale to the spectral edge of the coupling matrix. Theorem 1.2 identifies the covariance scale , contrasting with bounded covariance at every . A companion OpenAI preprint uses Theorems 1.1 and 1.2 as inputs for matching upper bounds .
The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.
Averaging over the starting state gives back the stationary law, so the obstruction must be proved start by start. The slow observable is the projection on the top eigenvector of the coupling matrix; the difficulty is the static estimate that this projection is rarely small on the scale under the Ising Gibbs law. This requires edge-of-spectrum random matrix estimates, a precise comparison between the Ising law and a tilted spherical law, and control of the conditioning on the sphere.
hamiltonian W x = ∑_{i<j} W_{ij} x_i x_j; disorderLaw n is the product of gaussianReal 0 (1/n) over pairs .siteKernel W i is the heat-bath kernel on configurations agreeing off ; discreteKernel = n^{-1}∑_i siteKernel; continuousKernel W t = exp(t ∑_i (siteKernel W i - 1)).continuousGoodMass/discreteGoodMass are the Gibbs masses of starts with distance ; convergence in probability is written as for all .covarianceNorm is the Euclidean operator norm; linearRayleigh is a real sSup over nonzero (the quotient is bounded and the set nonempty).sInf over times at which all starts are within .Infrastructure: finite continuous-time Markov chains (matrix exponentials), GOE edge estimates, tridiagonal models, spherical integrals. The intermediate results Proposition 3.1, Theorem 5.3 and Proposition 5.4 are natural further milestones.
The Sherrington–Kirkpatrick (SK) model (1975) is the basic mean-field spin glass: Ising spins interact through independent Gaussian couplings of variance , so each spin is weakly coupled to every other one with random signs. The model is the testing ground for questions about disordered systems, about sampling from Gibbs measures, and about the performance of Markov chain Monte Carlo. A central question is whether Glauber (heat-bath) dynamics, which resamples one spin at a time from its conditional law, relaxes at a rate independent of the system size. Equivalently: does the Gibbs measure satisfy a dimension-free Poincaré inequality with respect to the heat-bath Dirichlet form?
The equilibrium high-temperature phase is , where the free energy equals its annealed value (Aizenman, Lebowitz and Ruelle 1987). Dynamical results had reached only part of this range.
The source of this mission is an OpenAI preprint dated September 24, 2026, which treats every fixed .
Fix . Let be a symmetric matrix with zero diagonal and independent entries for . The zero-field Gibbs law on is
Let be the conditional expectation under given all spins except ; it averages over and its -th flip with Gibbs weights. The unscaled Dirichlet form is
The discrete heat-bath chain picks a uniform site and resamples it, with transition operator ; its spectral gap is over nonconstant .
There is a finite constant such that
and consequently the discrete heat-bath chain has spectral gap at least with probability tending to one. Lean: OAI.SKGap.sk_main, open on the platform.
The theorem gives a size-independent relaxation time for continuous-time heat-bath dynamics (rate-one clocks) throughout the high-temperature phase, for every observable simultaneously on one disorder event. It extends the dynamical picture from to the full equilibrium range , where only linear-observable (covariance) control was previously known. A Poincaré inequality is the input for mixing bounds and for companion results on cutoff and critical slowing down.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Dobrushin-type influence bounds fail because the sum of absolute couplings at a site grows like ; any argument must exploit cancellations from the random signs. Covariance bounds control only linear observables, while the Poincaré inequality must hold for all -dimensional families of test functions at once. The natural route through stochastic localization runs into rare observation events: an event of exponentially small probability can still carry most of the variance of a particular test function, and invertibility of the field equation must hold at every sufficiently accurate solution along the observation path.
Fin n → Bool, with spinValue mapping to ; couplings are indexed by pairs (Edge n) and symmetrized with zero diagonal by coupling.hamiltonian g 0 x = ½ ∑_{i,k} x_i J_{ik} x_k; mass, expectation, variance are exact finite sums over .conditionalExpectation g h i f x is the two-point Gibbs average over and its -th flip; dirichlet is the unscaled form .disorderLaw β n = Measure.pi (fun _ => gaussianReal 0 (β^2/n)) over the edges (variance ).discreteGap g is the infimum of over with positive variance.MainStatement β asserts a single for which both the Poincaré event and the gap event have probability tending to .Formalization needs Gaussian product measures, finite Gibbs measures and heat-bath operators, and the analysis behind the proof: matrix concentration, TAP/AMP-type field recursions and stochastic localization. Formal versions of the paper's intermediate results (for example Proposition 8.3, the terminal observation gap) are welcome.
The classical model (for , the classical Heisenberg model) places a unit vector at each site of the square lattice and favours alignment of neighbouring spins. It is the basic lattice model of a system with continuous symmetry. In two dimensions the Mermin–Wagner theorem rules out spontaneous magnetization at every positive temperature, but it does not say how fast spins decorrelate. For (the plane rotator) correlations decay only polynomially at low temperature — the Berezinskii–Kosterlitz–Thouless phase. For , Polyakov's 1975 renormalization-group argument predicts mass generation: exponential decay of correlations at every positive temperature, the lattice analogue of asymptotic freedom in four-dimensional non-Abelian gauge theory. A rigorous proof at low temperature has long been a central question of rigorous statistical mechanics.
Let be a finite subgraph of the nearest-neighbour square lattice , and let be edge strengths with . Put a spin at each vertex. The free-boundary Gibbs measure is
where is the uniform probability measure on the unit sphere and is the normalizing integral. There are no boundary spins and no external field. The two-point function is , and is Euclidean distance.
For every integer and every there are and such that, for every finite nearest-neighbour subgraph of , every and all ,
The constants depend only on and and may deteriorate as . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Uniformity over all finite subgraphs and strengths gives the same bound for free-boundary limits on boxes (Corollary 1.2 of the source) and for their subsequential infinite-volume limits, hence finite susceptibility. It confirms rigorously, for the spin two-point function, the mass-generation prediction for at arbitrarily low temperature, the regime left open by high-temperature and large- results, and contrasts sharply with the case. The source does not claim a transfer-matrix gap for all local observables, correlation-length asymptotics, or uniqueness of Gibbs states.
Formalizing it. The statement is a uniform estimate on explicit finite-dimensional integrals; a formal proof would certify a result the physics literature has expected since 1975. Groundwork includes Gibbs measures on products of spheres, rotation (Ward) identities, and random-cluster/sign-cluster representations, reusable for other lattice spin models.
Mermin–Wagner and McBryan–Spencer type arguments only show that order is destroyed and give polynomial bounds; they allow a zero decay rate and cannot distinguish from . Any proof must use the non-Abelian nature of the symmetry group, since the conclusion fails for . Exponential decay at high temperature (small ) follows from expansions, but at large spins are strongly aligned over long distances and no small parameter is available. Reducing to three components by conditioning produces random, dependent couplings, so the three-component estimate must hold uniformly over all strength arrays.
ℤ × ℤ; a LatticeGraph is a finite vertex set with a finite set of positively oriented nearest-neighbour edges (each undirected edge represented once). Strengths are functions G.edges → ℝ with , so deleting edges and weakening couplings are covered.Metric.sphere 0 1 of EuclideanSpace ℝ (Fin n); the single-site law is the normalized sphere measure (toSphere of Lebesgue measure); the configuration law is the product measure.correlation is the ratio of integrals ; the partition function is strictly positive, so the division is genuine.Random planar maps are graphs embedded in the sphere, chosen at random; they are the discrete models of two-dimensional quantum gravity. Decorating a map with a Fortuin–Kasteleyn (FK) random-cluster configuration with parameter couples the geometry of the map to a statistical-mechanics model (percolation, Ising, Potts), and the coupling changes the large-scale shape of the map. For the maps are expected to converge to Liouville quantum gravity surfaces; for the cluster weight is so strong that the map is predicted to become tree-like at large scales. This mission concerns that tree-like regime.
The source of this mission, an OpenAI preprint dated September 24, 2026, proves the finite-volume CRT prediction for every .
A rooted planar map is a connected graph embedded in the oriented sphere, up to orientation-preserving homeomorphism, with a distinguished dart (oriented edge); loops and multiple edges are allowed. For an edge subset , is the number of connected components of , isolated vertices included. For and , sample with according to
Let be graph distance on using all edges and .
For a standard normalized Brownian excursion on , ; the quotient by with the pushforward of Lebesgue measure is the Brownian CRT .
The Gromov–Hausdorff–Prokhorov (GHP) distance between compact metric probability spaces is the infimum, over isometric embeddings into a common space, of the maximum of the Hausdorff distance of the images and the Lévy–Prokhorov distance of the pushed-forward measures.
in distribution for the GHP topology, as through all positive integers. The Lean statement OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt is open on the platform.
The theorem establishes the tree side of the geometric phase transition of FK planar maps at in the natural finite-volume setting: the law is conditioned on the total size, the metric uses every edge, and the measure is the degree measure. Feng's infinite-volume result does not imply it, and a limit of an unconditioned encoding walk gives neither conditioning nor metric control. Together with companion results for , it completes the picture surface versus tree.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would also build reusable infrastructure: combinatorial maps as rotation systems, the GHP topology, and the Brownian CRT, none of which is in Mathlib.
The FK weight of a nonseparable block depends on its shape, not only on its size, so the block-weighted map results with uniform blocks do not apply, and exponential moments of block sizes are not available. The proof must show that the block tree is a critical Galton–Watson tree with finite offspring variance, and that graph distance along every ancestral path is asymptotically a constant times the depth, uniformly over all paths, using only a second moment.
Fin (2*(n+1)) (edge involution without fixed points, vertex rotation), connected, with (genus zero), modulo isomorphisms fixing dart 0. The Lean index corresponds to edges, and the scale is .Finsets of edge orbits; clusterCount counts components including isolated vertices; loops are omitted from adjacency only.MetricMeasureData packages a carrier, a distance and a measure; Valid means a compact metric probability space with Borel σ-algebra. ghpEDist is the infimum over pseudometrics on the disjoint union extending both distances.F continuous for ghpEDist at valid objects.A complete development needs Sheffield's inventory bijection or an equivalent finite word identity, Tutte's block decomposition, conditioned Galton–Watson tree limits with finite variance (Aldous; Broutin–Marckert), and GHP comparison lemmas. Contributions formalizing Proposition 2.2 (finite word identity), Proposition 4.3 (exact finite representation), Theorem 5.5 (uniform marked path sums) and Lemma 6.3 (metric and mass comparison) are welcome.
Plethysm — decomposing into irreducible -representations — is one of the oldest open problems in the representation theory of the general linear group, and it is central to geometric complexity theory, where the coordinate rings of Chow varieties of products of linear forms control lower-bound arguments. Foulkes' conjecture (1950) predicts that for there is a -equivariant injection . A natural candidate is supplied by a specific map, the canonical Foulkes–Howe map ; its surjectivity yields such an embedding by complete reducibility. Its image is the degree- part of the coordinate ring of the Chow variety of decomposable -forms, so surjectivity for large is a statement about that variety's normalization. The question is from which degree on the map is surjective, uniformly in .
Let be a finite-dimensional complex vector space and its symmetric algebra. is the span of products of vectors. For (, ), the canonical Foulkes–Howe map is the linear map determined by
where the outer products on the left and right are taken in and respectively. Equivalently: identify with symmetric tensors via averaging, multiply such tensors in , and project back. That this formula is well defined on is part of the content.
For every finite-dimensional complex and integers , , there is a unique linear map
satisfying the displayed formula on monomials, and is surjective.
The bound is not claimed to be sharp; the content is a stabilization degree polynomial in and independent of . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. Surjectivity gives, by complete reducibility, a -equivariant embedding for (Corollary 4 of the source), e.g. the sixth-power comparison for . It answers positively the request for a polynomial bound in Landsberg's Problem 7.19, and it says that the coordinate ring of the Chow variety of decomposable -forms agrees with its normalization in every degree . Since the canonical map is known to fail to be injective at and , an explicit range of surjectivity is the right kind of statement for this specific map.
Formalizing it. The statement is purely algebraic and uniform in , , . A formal proof would need multilinear algebra over symmetric algebras (symmetric powers of symmetric powers), which is reusable for plethysm and invariant-theory projects.
Surjectivity is equivalent to the vanishing of every symmetric -linear form on whose diagonal vanishes on products of vectors. The naive induction on fails because the factors in different slots share a common product and cannot be varied independently; the dimension of also grows the space of such forms without bound, so arguments using a fixed basis or dimension count do not give a uniform bound. Brion's effective bound depends on , and regularity bounds for the normalization do not locate the top degree of the quotient that controls stabilization.
SymPow n V of Mathlib's SymmetricAlgebra ℂ V spanned by products of vectors, and is SymPow b (SymPow a V).IsFoulkesMap a b V μ states the monomial formula above, with the normalizing factor and the sum over -tuples of permutations of Fin a.The Hattori–Stallings trace refines the rank of a finitely generated projective module over a group ring into one complex number per conjugacy class of . These numbers enter group-ring Euler characteristics, where they retain information that an ordinary numerical Euler characteristic forgets. Bass's trace conjecture (complex group-ring form) predicts that the trace of every projective module vanishes at every conjugacy class of an element of infinite order. For torsion-free groups this forces the trace to be an integer rank, and that in turn implies the Kaplansky idempotent conjecture: a group ring of a torsion-free group over a field of characteristic zero has no idempotents other than and . Both questions date from the 1960s–1970s and were previously known only for restricted classes of groups (linear, elementary amenable, amenable, hyperbolic, or groups satisfying the Farrell–Jones conjecture).
This mission asks for a formal proof of the complex Bass trace conjecture for all discrete groups, with the torsion-free consequences as a milestone, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a group and its complex group ring. is the Grothendieck group of finitely generated projective right -modules. An idempotent matrix represents the module ; its Hattori–Stallings trace is the class of in , extended additively to . Identifying this quotient with finitely supported functions on conjugacy classes (sum the coefficients over each class), is the coefficient of at the class .
For the corollary: is torsion-free if its only element of finite order is . The canonical trace is , the augmentation is , , and applies entrywise. is the coefficient at , and is the augmentation rank.
Let be torsion-free. (i) For every and idempotent , ; hence and . (ii) For every commutative unital domain of characteristic zero, every with is or .
For every group , every and every of infinite order,
equivalently, is supported on conjugacy classes of finite-order elements.
The result itself. Theorem 1.1 holds for arbitrary groups, with no amenability, finiteness, assembly-map or homological-dimension hypothesis. Combined with Linnell's restriction it gives the integral Bass conjecture (Corollary 9.1, p. 29) and, via Berrick–Chatterji–Mislin, statements about homotopy idempotents on manifolds (Corollary 9.2, p. 29). Corollary 1.2 settles Kaplansky's idempotent conjecture in characteristic zero, including over commutative domains rather than only fields. The analytic Kadison–Kaplansky statement in and the positive-characteristic idempotent problem are not addressed.
Formalizing it. The statements need only group rings (MonoidAlgebra), matrices, projective modules and conjugacy classes, all in Mathlib, so both are precise algebraic targets. The proof combines finite path sums in the group with a Pfaffian cocycle (Sections 7–8) and a geometric vanishing theorem for sparse simplicial cycles built from separating filtrations, simplicial volume estimates and free actions on Cantor-type spaces (Sections 2–6). None of this exists in Mathlib; the sparse-chain vanishing theorem (Theorem 2.1, p. 6) is of independent interest. No machine-checked proof of either conjecture, even for special group classes, is known.
Previous proofs pass through analytic completions or assembly maps and therefore need hypotheses on the group (amenability, hyperbolicity, Farrell–Jones), or through cyclic homology and need finite homological dimension of the reduced centralizers. The preprint turns an idempotent and an infinite-order element into simplicial cycles of every even dimension with connected supports in one graph of bounded degree, and a cocycle evaluating to (Propositions 7.3 and 8.3, pp. 24–27). The difficulty is to show that invariant cocycles vanish on such sparse cycles in high dimension for an arbitrary acting group , with no bound on its homological dimension (Theorem 2.1, p. 6): naive filling arguments need either amenability or finite dimensionality.
Module (MonoidAlgebra ℂ G)ᵐᵒᵖ structure, by isomorphism and direct-sum relations (ModuleK0); the Hattori–Stallings trace factors through a presentation of each module by an idempotent matrix. Its values are ConjClasses G →₀ ℂ.BassTrace.K0.Group), matrixTrace (sum of identity coefficients of diagonal entries) and augmentedMatrix; part (ii) quantifies over every commutative domain R with CharZero R.TorsionFree G is the usual condition (every finite-order element is ).In the representation theory of finite-dimensional algebras, vanishing of groups is the standard way of detecting projectivity homologically. The Auslander–Reiten conjecture (1975) asserts that a finitely generated module over an Artin algebra is projective as soon as
It arose from Auslander and Reiten's work on the generalized Nakayama conjecture and sits in a web of homological conjectures (Nakayama, Tachikawa, Gorenstein-projective, Auslander–Gorenstein) that were long expected to hold. A module is Gorenstein-projective if it is a cokernel in a doubly infinite exact complex of finitely generated projectives that stays exact under ; the Gorenstein-projective conjecture is the restriction of the Auslander–Reiten conjecture to such modules.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims an explicit counterexample to both conjectures. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
Let be the field of rational functions in three algebraically independent variables over . A finite-dimensional -algebra is an Artin algebra. For a left -module , is computed in the abelian category of left -modules. denotes the Jacobson radical. is Gorenstein-projective when for an exact complex of finitely generated projective modules such that every map into a projective that vanishes on the image of factors through . For a field extension , write and .
There exist a finite-dimensional -algebra and a finite-dimensional nonprojective left -module such that
is Gorenstein-projective, as -algebras, and . All of these conclusions hold again for and for every field extension .
The result itself. The theorem refutes the Auslander–Reiten conjecture for Artin algebras and the Gorenstein-projective conjecture; by extending scalars to an algebraic closure it also refutes them over an algebraically closed field of characteristic two. Since is then a nonprojective generator with no positive self-extensions, the generator formulation fails too. The structural data ( simple modules, split, ) place the example just outside the radical-cube-zero class where the conjecture is now known. The commutative case is not resolved.
Formalizing it. A formal proof would require Ext in module categories (available in Mathlib via Abelian.Ext), complete resolutions, triangular matrix algebras, trivial extensions and Hochschild cocycles, and base change of Ext under field extension. The counterexample is concrete, so much of the verification reduces to finite linear algebra over plus an infinite periodic-type resolution with uniform kernel formulas.
All positive results exploit some finiteness or rigidity (complete intersections, Cohen–Macaulay domains, radical cube zero, Auslander's condition), and the natural candidates for counterexamples (Schulz's quantum exterior algebra modules) have self-extensions that only vanish eventually, with . Vanishing in every positive degree, simultaneously against and , is the hard requirement. The preprint (Section 1.2, pp. 3–4) converts a suitable stable map over a symmetric algebra into a module over a triangular algebra (Proposition 3.1, p. 6), uses powers of for a resolution with uniform kernels, and kills every positive self-extension with two independent twists , using that has infinite multiplicative order.
FractionRing (MvPolynomial (Fin 3) (ZMod 2)), and the goal also asserts that the three generators are algebraically independent over .System (types in Type, with Ring, Algebra K, Module, and IsScalarTower K Λ Z instances). Conclusions asserts finite dimensionality over , ¬ Module.Projective Λ Z, the totally acyclic witness, Subsingleton of Abelian.Ext in ModuleCat for all against and against , a -algebra isomorphism , and .E with Algebra K E in an arbitrary universe; the module structure on must satisfy , which pins it to the standard one.For a field and a group , the group algebra consists of finite formal sums with , multiplied by extending the group law bilinearly. If has finite order , then , so has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if is torsion-free, has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).
A group is torsion-free if with implies . It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or ) for is a path-connected space with whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions . A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.
The coefficient field is , and is Mathlib's MonoidAlgebra (ZMod 2) G.
There exist a group and such that
This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over , a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force to be a domain. It implies that fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.
Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional ) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's lattice (Mian–Siddique 2026).
Writing down whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.
TorsionFree G is the plain group-theoretic notion (, implies ); finite presentability is Group.IsFinitelyPresented.HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space with a finite CW structure on all of , no cells above dimension , at least one -cell, a group isomorphism , and a surjective covering map from a contractible space onto (so is aspherical). Requiring a -cell excludes only the case of free groups, whose group algebras are domains.Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is -far from avoiding a pattern contains at least copies of , then sampling a number of rows and columns polynomial in detects the pattern with constant probability. Whether removal bounds are polynomial determines whether testers are efficient. For binary matrices whose rows and columns carry a fixed order, qualitative removal is known, and the polynomial version was conjectured.
A binary matrix of order is a map (in Lean BinaryMatrix n := Fin n → Fin n → Bool). For a binary pattern , an ordered copy of in is a pair of strictly increasing maps with for all : zeros must match as well as ones, and rows and columns are chosen independently. is the number of ordered copies, and is -free if . The normalized distance to -freeness is
where every cell may be changed in either direction.
The polynomial ordered binary matrix-removal conjecture asserts that for each fixed there are such that whenever , for all and .
The pattern is explicit: with and , the anchor has for , , and otherwise, and
For every there exist , and a binary matrix with
This is the "consequently" clause of Theorem 1.1 of the source, i.e. the negation of the conjecture for this fixed (here ). The source proves more: for every , with and , an explicit has and . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. A single explicit pattern shows that ordered binary matrix removal can be super-polynomial, answering the finite-family question of Alon and Ben-Eliezer negatively and disproving the singleton conjecture recorded by Gishboliner and Shapira. It also gives a testing lower bound (Corollary 5.1): a canonical row–column sampler needs sampled positions per axis on these examples. Earlier non-polynomial examples needed a third symbol in the host; here the host is binary. The example separates hitting all existing copies (a set of cells meets them) from repairing the matrix (at least edits are needed).
Formalizing it. The statement is fully finite and explicit, so a formal proof would certify both the construction and the two counting estimates. The construction is intricate (tree-indexed blocks with interleaved orders, a 66-cell pattern), which is exactly where a machine check adds confidence.
Two estimates pull in opposite directions. The distance bound must hold against every binary repair, including repairs that create new copies elsewhere; the obvious argument — delete one cell per copy — fails because changing cells can create copies, and the source must show any repair needs at least edits. The copy bound requires locating every ordered copy of the 66-cell pattern in the unedited host, not only the designated anchors, which forces a rigidity analysis of how the anchor can embed.
Fin n → Fin n → Bool; ordered copies are pairs of StrictMono maps Fin k → Fin n, counted by copyCount. fixedH : BinaryMatrix 66 encodes with 0-based indices (the anchor rule becomes etaBit (u-32) (v-58) for , ).fixedMinEdits A is the minimum Hamming distance from to an -free matrix (the all-zero matrix is -free, so the minimum is attained by a genuine matrix, and the sentinel is never selected); fixedDistance divides by .Real.rpow; are arbitrary positive reals, and are existentially chosen, so the statement is exactly the failure of the conjectured inequality for this . It is weaker than the explicit quantitative family of Theorem 1.1; a stronger milestone recording and the bound would be welcome.In a Maker–Breaker achievement game, two players alternately claim cells of a board; Maker wins by owning every cell of some copy of a fixed shape, and Breaker only tries to prevent this. Polyomino achievement games on the infinite square grid, introduced by Frank Harary, ask which small polyominoes are winners (Maker can force a copy) and which are losers (Breaker can prevent it forever). The six-cell shape Snaky is the long-standing hard case: Maker was known to win with a one-stone handicap or in higher dimensions, but the ordinary planar game without handicap remained undecided.
The source of this mission, an OpenAI preprint dated September 25, 2026, settles the ordinary planar game: Snaky is a winner, within 21 Maker moves.
The board is , initially empty. Snaky is
An allowed copy is with and one of the eight signed permutation matrices (rotations by quarter turns and reflections; no scaling). Maker moves first; then Breaker and Maker alternate, each claiming one previously unclaimed cell. Maker wins when it owns all cells of an allowed copy.
A Maker policy is a rule that, given the current position, returns an unclaimed cell. In the fixed-endpoint formulation, the policy keeps claiming fresh cells even after a win, and one asks that after Maker's -th claim its set of cells contain an allowed copy whenever Breaker's first replies were legal.
A pure computation on a printed certificate of 616 cards: card counts, 1,837 placement terms, required-set/envelope/height data of four interface cards, and uniform bounds for all cards.
The Lean statement OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states is open on the platform.
Theorem 1 decides the ordinary planar Snaky game, recorded as undecided by Sieben (2008), and gives an explicit bound of 21 Maker moves (a win by the 41st individual turn). It also gives a win on the finite board (Corollary 6), and removes the handicap from the earlier handicap-one strategies. The paper does not claim the bound 21 is optimal or address the strong game in which both players seek a copy.
The result is proved in an OpenAI preprint that has not been peer reviewed. Its correctness rests on a soundness lemma for a composition rule together with large finite certificates checked by standalone programs. A machine-checked proof would replace this combination of informal soundness argument and external computation by a single certified statement.
The board is infinite and Breaker may play anywhere, so no finite game-tree search applies directly: a proof must cover all Breaker replies, including those far from the action. Pairing strategies, the usual tool for proving shapes are losers, are known to fail for Snaky, but that does not give Maker a strategy. The certificate approach needs a composition rule whose soundness accounts for arbitrary previous ownership on both sides; the move count must be the number of actual Maker claims, including any replacement moves.
ℤ × ℤ; snaky is the six-cell set above and HasSnaky M asks for r : Fin 8, t : Cell with snaky.image (placement r t) ⊆ M, where orient lists all eight signed permutations.Policy is a function of a move counter, the Maker set and the Breaker set; it must never return an owned cell. playState σ N β ∅ ∅ k is the position after Maker claims and Breaker replies.LegalRepliesBeforeFinal σ N β ∅ ∅ constrains only the first Breaker replies; the theorems conclude a copy of , exactly Maker cells, and disjointness of the two players' sets throughout.Array Entry and computes rowAt i (required set, envelope, height) by the composition recursion; it is a decidable statement about explicit finite data.A trivializing reading is ruled out: the policy is required to be legal on all inputs, and Breaker's replies are arbitrary legal cells of the infinite board. A complete development needs a soundness proof for the composition rule (Lemma 3) and verified evaluation of the certificates; the policy, game and certificate infrastructure is shared between the 21- and 35-move statements. Contributions formalizing Lemma 3, Proposition 5 (the 21-move certificate identities) and Corollary 6 are welcome.
Given points in the plane with no three on a line, a halving line is a line through two of the points that leaves exactly half of the remaining points on each side. How many halving lines can an -point set have? The question is the middle case of the -set problem: count the -element subsets that a line can cut off. It controls the complexity of levels in line arrangements, and through them the running time of many algorithms in computational geometry (levels, ham-sandwich cuts, -th order Voronoi diagrams).
The gap between the bounds is one of the best known in discrete geometry: the upper bound has been since 1998, while the best constructions give only .
The source of this mission is an OpenAI preprint dated September 25, 2026, which claims the first power saving below .
Let be distinct points of with no three collinear. For , the orientation is the usual determinant; its sign says on which side of the line the point lies. For even , an unordered pair is a halving pair if exactly points lie strictly on each side of the line ; is the number of halving pairs.
A configuration is generic if moreover its -coordinates are distinct, the slopes of the segments are distinct, and no point where two of these segments properly cross lies on a third segment. Fix a rank . For a slope , mark the points with smallest value of . As increases from to , the marked set changes by exchanging one point for another; each change is a switch, and is the total number of switches. A switch at rank happens at the slope of exactly when points lie strictly below the line . At the middle rank, switches are halving pairs.
The Lean statement OAI.PlanarHalving.power_bounds is the conjunction of these two clauses and is open on the platform. Neither nor is specified, so the goal asserts only the shape of the improvement and survives any later numerical sharpening.
A power saving is the first improvement of the exponent in Dey's bound since 1998. The uniform version over all ranks gives, through shallow cuttings, a -sensitive bound for planar -sets and for the complexity of the -level in an arrangement of lines (Corollary 1.3). The saving is non-quantitative: the paper's compactness argument gives no numerical .
The result is proved in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify a long compactness argument (limiting measures, rank coordinates, differentiation of monotone functions) whose ineffective nature makes informal checking hard.
Dey's argument decomposes the halving graph into convex chains and applies the crossing lemma; both ingredients are tight on their own, so a power saving must show that configurations nearly attaining the crossing-lemma bound cannot exist. The bound must also hold uniformly over all ranks , because restricting a block of switches to the points that take part in it changes the rank. Since the lower-bound constructions are far below , there is no extremal example to guide the argument.
ℝ × ℝ, configurations are P : Fin n → Point; GeneralPosition P is injectivity plus nonvanishing orient for every triple of distinct indices.halvingCount P counts pairs i < j with sideCount P i j = (n-2)/2 and sideCount P j i = (n-2)/2, where sideCount counts points with strictly positive orientation. Natural-number division is harmless because is even.Generic P adds distinct first coordinates, distinct slopes of index pairs, and the condition that no proper crossing of two determined open segments lies on a third closed segment.switchCount P k counts pairs i < j with 0 < k < n and exactly k - 1 points strictly below the line through P i, P j in the order . Ranks and therefore contribute zero, as in the paper.slope divides by the -difference; the generic hypothesis makes it nonzero.A complete development needs the crossing lemma, convex-chain decompositions of the rotating-line process, weak compactness of finite Borel measures, the Radon–Nikodym and Lebesgue differentiation theorems, Rademacher-type differentiability of monotone functions, and planar Jordan-curve separation. Contributions formalizing Dey's bound, Theorem 2.1 (uniform activity packing) and Proposition 8.1 (the fixed-scale recurrence) are welcome.
A set is square-difference-free if no two of its elements differ by a perfect square with . The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing for the largest size of a square-difference-free subset of , the problem is a prototype for polynomial patterns in dense sets: it is the simplest case of finding differences in the image of a polynomial, and it is the model problem on which Fourier-analytic, ergodic and density-increment methods for polynomial configurations are tested. A long-standing gap separates the upper bounds, which until recently saved only a power of (with a slowly growing exponent), from the lower bounds, which are powers and beyond. Whether a fixed power saving holds was posed explicitly by Green and Sawhney.
For a positive integer write . A set is square-difference-free if
that is, for all and all integers . (Differences are taken in ; is allowed since is excluded from the squares.)
In Lean (namespace OAI.SquareDifference), sets are Finset ℤ contained in Finset.Icc 1 N, and IsSquareDifferenceFree A states a - b ≠ (m : ℤ)^2 for all a b ∈ A and m : ℕ with 1 ≤ m.
There are absolute constants and such that for every integer and every square-difference-free ,
Equivalently, every subset of with more than elements contains two elements differing by a nonzero perfect square. The Lean goal is published on the platform with status Open. The statement fixes no numerical value of , so any improvement of the exponent leaves the goal unchanged.
The result itself. Every earlier upper bound saved less than any fixed power of ; the best, due to Green and Sawhney, saved . A fixed power saving changes the nature of the problem: it shows that the extremal exponent lies strictly below , so both upper and lower bounds are now polynomial and the remaining question is the value of the exponent, now known to lie between and . As an immediate consequence (Remark 1.2 of the source), the graph on joining integers differing by a square has chromatic number at least , a polynomial bound for the square-difference coloring problem.
Formalizing it. The statement is elementary and self-contained, involving only finite sets of integers. The proof combines a graph/tuple reformulation, reflection-positivity (chessboard) inequalities for a finite-field probability law, and an induction with fixed finite constructions. A formal proof would certify an argument whose constants are explicitly noted to be extremely small and not computed.
Density-increment arguments, starting from Sárközy's circle-method proof, gain a constant factor of density at each step but lose a power of the length of the progression on which they pass, so after the increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level- approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only . A power saving requires an argument whose loss does not compound with the number of iterations — a single estimate that converts square-difference-freeness into a polynomial density loss.
Finset ℤ inside Finset.Icc 1 N and is a natural number; the bound is uniform in .How efficiently can the edges of a graph be split into cycles? Some single edges must be allowed, since a forest has no cycles at all, and a tree on vertices already needs single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on vertices can have its edge set partitioned into simple cycles and single edges. Equivalently, every graph with all degrees even partitions into cycles. The problem is a basic question about edge decompositions, and the partial bounds , and trace several decades of progress on it.
This mission asks for a formal proof of the linear bound, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A finite simple graph has vertex set of size and edge set of unordered pairs of distinct vertices. A cycle is a closed walk of length at least with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of into parts is a family of pairwise disjoint subsets of with union , where each is either the edge set of a cycle of or a single edge of . Parts may share vertices; isolated vertices need not be covered; for an edgeless graph is allowed.
There is an absolute constant such that for every and every simple graph on vertices,
The value of is left unspecified, which keeps the goal stable under future improvements of the constant (the best possible constant is at least , by complete bipartite examples).
The result itself. The order is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp cycle bound for Eulerian graphs satisfying a large-cut condition. It removes the last iterated-logarithm loss from the Bucić–Montgomery bound.
Formalizing it. The statement uses only Mathlib's SimpleGraph.Walk.IsCycle and edge sets, so it is a clean combinatorial target. A complete development needs Lovász's path-cycle decomposition theorem, the Aharoni–Haxell hypergraph matching theorem, expansion and routing lemmas, and binomial tail bounds; all are reusable in extremal graph theory. No machine-checked proof of any bound is known.
Covering is easy (Pyber's bound), but a cover does not yield a partition: deleting repeated edges can break cycles into many paths. For partitions, the standard strategy decomposes the graph into expanding pieces at a sequence of scales, and paying a cost proportional to the full order at every scale accumulates a factor from the number of scales — this is where the and losses come from. The preprint (Introduction, pp. 2–3) charges the work on a prefix of scales to a single expanding layer and saves a fixed fraction of vertices by identifying pairs, then lifts quotient cycles back with reserved edge-disjoint routes (Lemma 3.1, p. 5); keeping a separate assignment for each original edge throughout is what makes the induction close.
SimpleGraph (Fin n) for arbitrary n (including 0 and edgeless graphs).CycleOrSingleEdge G s: either is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least ), or for an edge .EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.MainStatement: EdgeDecomposition G k .An expander graph is a sparse graph in which every set of vertices has a large edge boundary relative to its size. Expanders with bounded degree are a basic tool across combinatorics, computer science and group theory. High-dimensional expanders are simplicial complexes that extend this behavior to faces of every dimension, and coboundary expansion over is the strongest of the standard notions: the coboundary of any set of -faces must be large unless the set is already close to a coboundary. Gromov connected such filling inequalities with topological overlap of maps to Euclidean space. The basic existence question is whether there are arbitrarily large complexes of fixed dimension with bounded vertex degree and uniform coboundary expansion in every degree.
A finite simplicial complex is a downward-closed family of finite sets (faces) of vertices; denotes the faces with vertices. is pure of dimension if it has -faces and every face lies in one. An -cochain is a function ; its coboundary is . Let , with the constant functions. Faces are weighted by
so is the probability that is nonzero on a random -face of a uniformly random top face, and .
In Lean (namespace OAI.CoboundaryExpanders), a Complex has vertex set Fin vertexCount, a Finset of faces that is downward closed and contains every singleton; Pure, Connected (connected -skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts -faces containing .
For every there are , and finite connected pure -dimensional complexes with , every vertex in at most faces of dimension , and
with constants independent of , and . The Lean goal is published on the platform with status Open.
The result itself. Together with the classical graph case and the Chapman–Lubotzky two-dimensional theorem, Theorem 1.1 gives bounded-degree coboundary expanders in every positive dimension, answering the existence question in the form stated by Chapman and Lubotzky. Earlier bounded-vertex-degree constructions gave cosystolic expansion, which permits nonvanishing cohomology, or degree-one expansion only; earlier coboundary expanders in all dimensions had vertex degrees growing with size. Coboundary expansion in all degrees implies vanishing -cohomology below the top dimension, the property Gromov related to topological overlap.
Formalizing it. The definitions are elementary finite combinatorics, so the statement is completely precise; the proof combines group-theoretic coset complexes over , congruence quotients and a quantitative cosystolic input. A formal proof would require formalizing that input (Oppenheim–Valentiner-Branth), which is substantial.
Coboundary expansion requires two things at once: a quantitative isoperimetric inequality against cocycles (cosystolic expansion) and exact vanishing of for every . Random constructions give vanishing cohomology but force growing vertex degree; algebraic bounded-degree constructions (Ramanujan complexes, coset complexes) give the quantitative inequality but typically have nonzero cohomology that cannot be controlled uniformly. A cocycle that is not a coboundary has zero coboundary and positive distance, so any nonzero cohomology class destroys the inequality. The difficulty is a family of bounded-degree complexes whose cohomology vanishes in every degree below , uniformly along the tower.
Fin vertexCount and every vertex is a face; faces are Finsets, and an -face has exactly vertices.ZMod 2-valued; is the constant cochains (reduced cohomology in degree ). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.When does the Erdős–Rényi random graph contain a copy of a prescribed graph ? A necessary condition is visible from first moments: if some subgraph has expected copy count below a constant, then is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.
This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For finite simple graphs let be the number of subgraphs of isomorphic to (ordinary, non-induced copies). is the random graph on with each of the edges present independently with probability . For a graph with at least one edge and at most vertices,
The first is the containment threshold, the second the graph expectation threshold; always . Write for the number of edges.
For every and every finite simple graph with edges and at most vertices,
The constants are explicit and universal; may vary with .
The result itself. The bound says that, up to a universal constant times , the only obstruction to containing is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching while , because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing .
Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of , so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.
The abstract theorem compares with the integral expectation threshold of the family of edge sets containing a copy of , and covers of may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of . Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).
Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real but used only on .expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.criticalThreshold and expectationThreshold are sInf over ; the sets are nonempty (they contain when has at most vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is .A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost control, can be augmented cheaply into tours, which gave an -approximation (doi:10.1287/opre.2017.1603). Goddyn's thin tree conjecture asks whether high edge connectivity alone forces an -thin spanning tree, independently of the number of vertices; the strong form asks for thinness in a -edge-connected graph.
Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives edge-disjoint spanning trees in a -edge-connected graph (doi:10.1112/jlms/s1-36.1.445, doi:10.1112/jlms/s1-36.1.221), so each cut is used about times on average, but no single tree need be good for every cut. Oveis Gharan and Saberi proved the bound for planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan obtained thinness in general (2015, arXiv:1411.4613), using the Marcus–Spielman–Srivastava interlacing-families method (doi:10.4007/annals.2015.182.1.8). Klein and Olver handled any prescribed laminar family of cuts (2023, doi:10.1109/FOCS57990.2023.00011), and Klein, Olver and Yeoh controlled all near-minimum cuts (2026, doi:10.4230/LIPIcs.ICALP.2026.129). Constant-factor ATSP approximations were obtained by other means (Svensson–Tarnawski–Végh 2020, doi:10.1145/3424306; Traub–Vygen 2022, doi:10.1137/20M1339313), but the thin tree question stayed unresolved.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the strong thin tree conjecture.
Let be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset , let be the set of edges with exactly one endpoint in . is -edge-connected if for every such . For an edge set , . A spanning tree is -thin if for every nonempty proper .
There is a universal constant such that for every , every finite loopless -edge-connected multigraph with at least two vertices has a spanning tree with
Lean: OAI.StrongThinTree.strongThinTree, open on the platform.
The order is optimal (two vertices joined by parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the loss of Anari–Oveis Gharan. It shows that connectivity alone controls all cuts at once, and gives a structural route to ATSP integrality-gap bounds through thin trees. An algorithmic version (deterministic polynomial-time construction) is the subject of the companion mission in this family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Averaging over a Nash–Williams–Tutte packing controls each cut on average but not all cuts simultaneously: there are exponentially many cuts and a union bound over them loses a factor depending on . Spectral approaches control all cuts via a matrix inequality, but spectrally thin trees need not exist when some edges have large effective resistance, which is why previous spectral arguments lost factors. One must instead keep a large tree packing on low-resistance edges through a sequence of sparsifications whose relative losses stay bounded.
MultiGraph n m: vertices Fin n, edges Fin m with endpoint maps and a looplessness proof; parallel edges are distinct edges.cut G T S: the edges of T with exactly one endpoint in S. Connected G T: every nonempty proper S is crossed by T. SpanningTree G T: T connected and every proper deletion disconnects.EdgeConnected G k: every nonempty proper cut has at least k edges.MainStatement: ∃ C > 0, ∀ k ≥ 1, ∀ n ≥ 2, ∀ G k-edge-connected, ∃ T spanning tree, ∀ S nonempty proper, |cut T S| ≤ (C/k)|cut G S| (real arithmetic).Needed infrastructure: graph Laplacians and effective resistance, the Nash–Williams–Tutte theorem, the Marcus–Spielman–Srivastava mixed-characteristic-polynomial bound, and a Brouwer-type fixed point theorem (the paper proves the finite-dimensional case via Sperner's lemma). Contributions formalizing Theorem 2.3 (Nash–Williams–Tutte), Theorem 3.2, Theorem 4.1, Proposition 6.2 or Theorem A.1 are welcome.
For integers the Ramsey number is the least such that every simple graph on vertices contains a clique of order or an independent set of order . Ramsey's theorem guarantees these numbers are finite. In the off-diagonal regime, is fixed and ; the classical upper bounds give , while for a long time lower-bound constructions did not reach the power . Once the power was settled, the remaining question was the power of .
A graph on vertices is a SimpleGraph (Fin N). The Lean development defines
RamseyProperty s t N: every graph on Fin N has an -clique, or its complement has a -clique (an independent set of size );ramsey s t := sInf {N | RamseyProperty s t N}, the Ramsey number .All logarithms are natural; real powers of use Real.rpow.
For every integer there is such that for every and every sufficiently large (threshold depending on )
This is Theorem 1.1 of the source, formalized as main (s) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. Together with the companion preprint and the earlier results for on the polynomial exponent, the theorem identifies the exact power of in up to for each fixed : the classical AKS upper bound is sharp in its logarithmic exponent. It does not give a matching constant-factor lower bound. The main new ingredient is a prime-indexed construction (Theorem 1.2 of the source): for fixed and large primes , a -free graph on vertices with independence number below , built from random incident point–hyperplane flags of .
Formalizing it. The upper half is classical (Proposition 7.3 of the source restates the AKS estimate for all fixed ). The lower half is a long argument combining finite projective geometry, entropy of a selected subsequence, and incidence bounds in positive characteristic; formal verification would independently check an unrefereed claim.
Bradač's projective graph has the right number of vertices but its independent sets were only controlled up to logarithmic exponent . Improving to requires bounding long independent sequences in a random stream of flags. A union bound over sequences loses too much, and a sequence selected from the random stream need not have independent or uniform flags. The source pays for this with an entropy lower bound on the selected sequence and a compression upper bound, which in turn requires a description theorem for sparse point–hyperplane pairs in arbitrary dimension (repeated projections and a high-rank two-row description based on a finite-field Zariski-closure inequality of Nie and Wang).
SimpleGraph (Fin N); independent sets are cliques of the complement graph. ramsey is an sInf, equal to because the defining set is nonempty by Ramsey's theorem.MainBounds s fixes one (depending on ) before quantifying over ; natural subtraction s - 1, s - 2 is harmless because . MainLimit s is a Filter.Tendsto over natural .For integers the Ramsey number is the least such that every simple graph on vertices contains either a complete subgraph or an independent set of vertices. Determining how grows when is fixed and is one of the central problems of extremal and probabilistic combinatorics: upper bounds come from counting and local density arguments, lower bounds require explicit or random constructions of -free graphs with no large independent set, and for decades the two sides did not even agree on the power of .
A graph on vertices is a SimpleGraph (Fin n). A -clique is a set of pairwise adjacent vertices and a -independent set a set of pairwise non-adjacent vertices. The Lean development defines
RamseyProperty s t n: every simple graph on Fin n has an -clique or a -independent set;ramsey s t := sInf {n | RamseyProperty s t n}, the Ramsey number .All logarithms are natural.
There is an absolute constant such that for every and all sufficiently large (threshold depending on )
and consequently
This is Theorem 1.1 of the source, formalized as SharpBounds ∧ SharpExponent. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. The theorem determines up to a factor , the first case beyond in which the logarithmic exponent of a fixed off-diagonal Ramsey number is known. It shows that the classical upper-bound exponent is the truth for , and it leaves open only a constant-factor asymptotic for . The lower-bound construction (random incident point–hyperplane pairs in projective space , ordered by position) together with its entropy/compression analysis is the new part.
Formalizing it. The upper bound is an elementary argument (triangle-free independent-set bounds plus random sampling), stated separately in the source as Theorem 2.1 for all ; its formalization is a self-contained milestone. The lower bound is a long probabilistic and finite-geometric argument whose formal verification would independently certify an unrefereed claim.
The lower bound needs a -free graph on about vertices with no independent set of size . Random graph processes lose logarithmic factors and even the power of ; Bradač's projective graph has the right power but its independent sets were only controlled to logarithmic exponent . The obstacle is to bound long independent sequences in a random stream of flags: a direct union bound over sequences is far too weak, and the selected sequence can have a heavily biased law. The source handles this with an entropy lower bound and a matching compression (description) upper bound that relies on a new theorem about sparse point–hyperplane incidences.
SimpleGraph (Fin n); cliques and independent sets use Mathlib's IsNClique and IsNIndepSet. ramsey is an sInf, which is the true Ramsey number because the defining set is nonempty by Ramsey's theorem; a proof must use that nonemptiness rather than the junk value 0.SharpBounds fixes one before ; the threshold may depend on . The power is Real.rpow. SharpExponent is a Filter.Tendsto statement over natural with real logarithms.The unit-distance problem of Erdős asks how many pairs among points in the plane can be at distance exactly one. By rescaling, this is the same as asking how often a single distance can repeat. It is one of the central extremal questions of combinatorial geometry and a benchmark for incidence methods. The bound of Spencer, Szemerédi and Trotter (1984) has resisted improvement of its exponent for four decades, and the same exponent is sharp for the closely related Szemerédi–Trotter point–line incidence theorem, so any improvement must use geometry specific to circles in the Euclidean plane.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a fixed power saving: for some absolute . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
For a finite set let
the number of unordered pairs of distinct points at Euclidean distance one, and let
The maximum exists because .
There are absolute constants and such that
Equivalently, for an absolute . The goal leaves and unspecified, so it is stable under any later numerical improvement.
The result itself. It answers the long-standing question of whether the Spencer–Szemerédi–Trotter exponent can be lowered by a fixed amount. Combined with the recent lower bounds along a sequence, it confines the true exponent to an interval strictly inside . Because point–line incidences do attain , the result also isolates a genuine difference between unit circles and lines in incidence geometry.
Formalizing it. The proof combines random cuttings in the Clarkson–Shor framework, an entropy-based prediction lemma, the product formula and absolute heights of algebraic numbers, and an algebraic obstruction using derivations and valuations of function fields. A formal proof would add these to Mathlib and would also require the bound itself (via the crossing lemma) as background. No machine-checked unit-distance bound beyond trivial ones is known.
Every known proof of uses only two combinatorial properties of unit circles (two circles meet in at most two points; two points lie on at most two unit circles), and those properties are shared by systems attaining , so no argument using only them can save a power. The saving must exploit arithmetic or algebraic rigidity of the Euclidean metric. In the preprint the scheme is a contradiction argument on a hypothetical sequence with unit pairs among points: transfer to number fields, measure edge-jump profiles at all absolute values, and show that either a bounded-scale configuration violates a determinant identity (Proposition 4.4, p. 19) or a dense pair graph with low-height rectangle products arises, which is excluded algebraically (Proposition 8.1, p. 42). The hard step is transferring concentration from predicted states to actual points under the true edge and history laws (Lemma 6.2, p. 29).
EuclideanSpace ℝ (Fin 2); unitPairCount X counts elements of X.sym2 (unordered pairs, diagonal included but never at distance ) with dist = 1.u n is the natural-number sSup of unitPairCount X over -element Finsets; the set is nonempty and bounded by , so it is the true maximum.∃ C β : ℝ, 0 < C ∧ 1 ≤ β ∧ β < 4/3 ∧ ∀ n, (u n : ℝ) ≤ C * n ^ β with real-power exponent. At both sides vanish.