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.
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?
Random 3-SAT, a conjunction of random three-literal clauses on variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near . Once a limiting threshold is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given , outputs a rational within of ? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.
The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of , beyond existence.
For , a proper random 3-clause chooses three distinct variables uniformly from and gives each an independent fair sign. Let be the conjunction of independent such clauses (sampled with replacement from the possibilities; the empty formula is satisfiable) and
A real is computable if a single algorithm, on input , halts with a rational satisfying .
There is such that for every fixed real
and one finite deterministic Turing machine, on input , halts with a rational with , using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.
The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of (Theorem 4.4) for the same proper-clause model.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.
ProperClause n k is Fin n → Option Bool with exactly defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to .MainStatement asserts with the two strict-side limits at , a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and for all .Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.
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.In Bernoulli bond percolation on a graph , each edge is kept (open) independently with probability . As grows, an infinite connected component of open edges appears at the critical probability . The criticality problem asks whether an infinite cluster can already exist at . A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and , there is no infinite cluster at . The question contains the famous open case of and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.
The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.
A graph here has vertex set and a set of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on . Examples include and every Cayley graph of a finitely generated group.
For , let be the law of a random set containing each bond independently with probability . The cluster of is the set of vertices joined to by a finite path of bonds in (including ). Define
For every infinite, connected, locally finite, quasi-transitive graph ,
The hypothesis is necessary, since at every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.
Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives on for every (Corollary 10.1, p. 39), including the long-open case . With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at on every such graph.
The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour . A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.
The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.
BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.criticalProbability is sInf in unitInterval of ; if the set were empty this would be , which hpc excludes.percolates is the event that some cluster is infinite; the conclusion says it has measure at .A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.
Bernoulli percolation is the simplest model of a random medium: each edge (or each vertex) of a lattice is independently kept open with probability , and one studies the connected components (clusters) of open edges or vertices. As increases, an infinite cluster appears at a critical parameter . Whether an infinite cluster already exists at decides whether the phase transition is continuous, and it is the basic question about critical behaviour. On the nearest-neighbour cubic lattice it has been a central open problem of probability and statistical physics since the 1980s; the dimensions where it was settled were and sufficiently high .
The source of this mission is an OpenAI preprint dated September 24, 2026, giving a self-contained argument for both bond and site percolation on .
Vertices are ; and are nearest neighbours if for a coordinate vector .
Let be the product law, , and
defined separately for bonds () and sites ().
The Lean statement OAI.CriticalZ3.critical_no_infinite is the conjunction of these two almost-sure statements. It is open on the platform.
Theorem 1.1 gives continuity of the percolation probability at the transition: as (the paper derives this on p. 1 from the theorem and finite-box approximation). It is the three-dimensional case of the Benjamini–Schramm criticality question and of the classical problem, which had resisted both planar methods (which rely on duality unavailable in three dimensions) and the lace expansion (which needs high dimension). The site statement is not a formal consequence of the bond statement: site bits become hyperedges with an endpoint convention that must be preserved.
The result is proved in an OpenAI preprint, which has not been peer reviewed. A public announcement reports a Lean formalization of the bond case on ; no machine-checked proof of this exact statement exists on the platform, and the site case is not covered by that announcement's formalization. A formal proof here would certify both models in one development.
The natural route is renormalization: show that if an infinite cluster exists at , then good finite-box events have high probability, persist at some , and can be glued into an infinite cluster at . The gluing step is where the obvious argument fails. Positive correlation (Harris–FKG) controls the probability that two increasing events both occur, but here one needs the probability of reaching a relay set and then a target, conditioned on an explored region; without a comparison inequality of the form the losses compound. Slab results do not suffice: extinction at each slab threshold plus convergence of thresholds does not give extinction on .
Vertex := Fin 3 → ℤ; bonds are pairs (x, i) representing the edge from x to step x i = x + e_i, so each edge appears once.bondLaw p and siteLaw p are Measure.infinitePi of bernoulliMeasure true false, giving mass to "open"; parameter clamps into .Relation.ReflTransGen of the open-adjacency relation; siteCluster ω x is empty unless ω x = true, matching the endpoint convention.bondCritical and siteCritical are sInf of . The statement does not assume ; it is a known fact for , and a solver may need to prove it to rule out the empty-set convention.A complete development needs product Bernoulli measures on countable index sets, monotone coupling, increasing events and Harris–FKG, the finite hyperedge comparison inequality, and a planar boundary-counting lemma. The percolation infrastructure is reusable for the quasi-transitive generalization in the same family. Contributions formalizing Proposition 2.1 (joint connection comparison), Corollary 2.3 (failure comparison), Lemma 4.1 (extension estimate) and Lemma 5.1 (neighbouring-box relay) are welcome.
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 ).The irreducible complex representations of the symmetric group are the Specht modules , indexed by partitions . How a tensor product (with diagonal action) decomposes is recorded by the Kronecker coefficients
for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase , a partition of , has a tensor square containing every irreducible representation of .
A partition is a Mathlib YoungDiagram. The Lean development builds concretely: for a tableau (a bijection between and the cells), the polytabloid is the signed sum over the column group of of the permuted indicator of the row word of , inside the space of functions on words ; Specht t is the -span of the -orbit of . The coefficient kronecker a b t is the complex dimension of the space of -intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells with , i.e. .
For every integer and every partition ,
equivalently contains every irreducible representation of . This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram with as many cells as staircase m). The goal is published on the platform with status Open.
The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every already occurs in the submodule generated by one explicit tensor of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every , an irreducible representation of whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).
Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of .
Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all ) or higher powers (cube, fourth power) leave exceptional constituents. An induction on must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.
staircase m has cells , with cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map exists.The irreducible complex representations of the symmetric group are indexed by partitions and written (Specht modules). Decomposing a tensor product (with the diagonal action) into irreducibles is governed by the Kronecker coefficients
which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.
For a Young diagram with cells, fix a bijection between and the cells (a tableau). The Lean development realizes inside the space of functions on words ( = number of rows), with acting by permuting letters: the polytabloid is the signed sum, over the column group of , of the permuted indicator of the row word of , and Specht t is the -span of the -orbit of . The Kronecker coefficient kronecker a b t is finrank of the space of -intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape .
For every positive integer with there is a partition such that
so the tensor square contains every irreducible representation of . The Lean statement asserts, for one Young diagram with cells: positivity of kronecker for every target diagram with cells; irreducibility of spechtRep for ; and that every finite-dimensional irreducible complex representation of admits an injective intertwining map into . This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.
The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.
Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible , and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.
Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and are genuine exceptions.
YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of in the tensor square.Let be a finite-dimensional algebra over a field. A finite-dimensional module is self-orthogonal if for every . Tachikawa's second conjecture asserts that over a self-injective algebra every self-orthogonal module is projective. It belongs to the cluster of homological conjectures around quasi-Frobenius algebras and dominant dimension recorded in Tachikawa's 1973 monograph, alongside the Nakayama, generalized Nakayama and Auslander–Reiten conjectures. Since automatically when is self-injective, it is exactly the self-injective case of the Auslander–Reiten conjecture. Enomoto and Marczinzik showed that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture, so the two were expected to stand or fall together.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a counterexample over a symmetric algebra. 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 rational function field in three algebraically independent variables. Write . A finite-dimensional -algebra is symmetric if as -bimodules, where ; equivalently there is a -linear isomorphism with . Symmetric algebras are self-injective. For a finite-dimensional left -module , is computed in the category of left -modules.
There exist a finite-dimensional associative unital symmetric -algebra and a finite-dimensional unital left -module such that is not projective and
In particular Tachikawa's second conjecture is false, and since is self-injective the same pair is a symmetric counterexample to the Auslander–Reiten conjecture.
The result itself. The theorem disproves Tachikawa's second conjecture in the strongest natural class (symmetric algebras). Through an associated endomorphism algebra, the preprint further claims counterexamples to the classical, generalized and strong Nakayama conjectures, the Auslander–Gorenstein conjecture and the Wakamatsu tilting conjecture, persisting under every field extension (Corollary 1.2, p. 4), together with consequences for finitistic dimensions (Corollary 1.3, p. 5). Those corollaries are not part of this mission's goal. A companion preprint gives an explicit eight-simple triangular counterexample to the Auslander–Reiten conjecture.
Formalizing it. The statement uses only notions already in Mathlib (finite-dimensional algebras, projective modules, Abelian.Ext in ModuleCat), so it is a clean target. The proof needs trivial extensions , totally acyclic complexes, stable categories of symmetric algebras, Koszul computations of -algebras, and Hochschild bar complexes; these are reusable throughout representation theory.
Known non-examples come close but fail: Schulz's quantum exterior modules have vanishing higher self-extensions but nonzero ; Böhmler and Marczinzik have a commutative self-injective example with only . Vanishing in every positive degree requires controlling an infinite resolution. In the preprint, the passage to a symmetric algebra also requires vanishing of the negative part of a complete self-extension complex (condition (1.1), p. 2), which is what the transfer through the trivial extension , (Proposition 3.2, p. 12) consumes. Producing it needs two twists acting by distinct scalars on every nonzero homogeneous self-map space, and genuine bimodule lifts of stable maps (Proposition 6.1, p. 21).
FractionRing (MvPolynomial (Fin 3) (ZMod 2)), i.e. with independent variables.SymmetricOver k A asks for a -linear equivalence e : A ≃ₗ[k] Module.Dual k A with e (a*b) c = e b (c*a) and e (a*b) c = e a (b*c), i.e. a bimodule isomorphism .Counterexample asserts existence of A : Type with Ring and Algebra k structures, Module.Finite k A, symmetric; and M with compatible Module A, Module k (IsScalarTower), Module.Finite k M, ¬ Module.Projective A M, and Subsingleton (Abelian.Ext (ModuleCat.of A M) (ModuleCat.of A M) n) for all n > 0.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.Every module over a ring has a projective resolution, and its length, the projective dimension, measures how far the module is from being projective. Over a finite-dimensional algebra, some modules have infinite projective dimension; the finitistic dimension conjectures ask whether, among the modules whose projective dimension is finite, these finite values are bounded. The questions were publicized by Bass in 1960 and became central problems in the representation theory of finite-dimensional algebras, tied to many other homological conjectures (Nakayama, Gorenstein symmetry, Auslander–Reiten), each of which would follow from finiteness of the finitistic dimension.
The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample to the little finitistic-dimension conjecture over . A companion OpenAI preprint independently gives a characteristic-two example.
Let be a finite-dimensional unital algebra over . For a left -module , is the minimal length of a projective resolution. The little finitistic dimension is
and the big finitistic dimension is the same supremum over all left modules. Over a finite-dimensional algebra, finitely generated and finite-dimensional modules coincide. The little finitistic-dimension conjecture asserts for every such .
Injective left modules generate if the smallest triangulated subcategory of the unbounded derived category of left modules that contains them and is closed under arbitrary coproducts is the whole category.
The Lean statement OAI.LittleFinitistic.Main.exists_counterexample is open on the platform.
injective left -modules do not generate, and injective right -modules do.
Theorem 1.1 refutes the little finitistic-dimension conjecture: a single finite-dimensional algebra has finitely generated modules with terminating projective resolutions of unbounded length. Since , it also refutes the big version for Artin algebras, and by Rickard's theorem gives an algebra for which injectives do not generate the derived category. Corollary 1.2 shows that finiteness can fail on one side and hold on the other in the most extreme way, in contrast with Cummings' equivalence of universal finiteness and left–right symmetry.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Because many homological conjectures were known to follow from the finitistic-dimension conjecture, an independent check of a counterexample is of direct interest.
Positive results cover large classes (monomial, radical cube zero, representation dimension at most three), so a counterexample must escape all of them. The finitistic dimension of one fixed algebra must be unbounded, which requires encoding an unbounded family of terminating processes into fixed finite data. The paper realizes a "selection process" from an infinite finitely presented group algebra by a single bounded bimodule complex over a finite-dimensional algebra; making this realization uniform in the input module, and turning it into ordinary projective resolutions over a trivial extension, are the main obstacles.
A : Type with [Ring A] [Algebra ℂ A] and FiniteDimensional ℂ A; modules are objects of ModuleCat.{0} A, finiteness is Module.Finite A N.projectiveDimension is Mathlib's CategoryTheory.projectiveDimension, valued in WithBot ℕ∞, equal to ⊤ for infinite dimension; littleFinitisticDimension and bigFinitisticDimension are suprema over modules of finite projective dimension.Aᵐᵒᵖ.InjectivesGenerate uses HasDerivedCategory.standard and quantifies over isomorphism-closed triangulated properties closed under coproducts indexed by Type u and containing all injectives in degree 0.A complete development needs derived tensor products of bimodule complexes, trivial extension algebras and their bar resolutions, finite presentations of group algebras and their finite-dimensional representations, and (for the milestone) Rickard's theorem and Cummings' triangular algebra. Contributions formalizing Proposition 2.1 (selection), Theorem 4.1 (tensor realization) and Proposition 6.1 (bar splitting) are welcome.
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.The Ramsey number is the least such that every red–blue colouring of the edges of contains a red copy of or a blue copy of . For a cycle against a clique there is a simple lower-bound construction: take disjoint red cliques of order with all edges between them blue. It has vertices, no red (each red component is too small) and no blue (a blue clique meets each red clique at most once). In 1978 Erdős, Faudree, Rousseau and Schelp conjectured that this construction is optimal whenever , apart from . Cycle–complete Ramsey numbers are among the few families where exact values are expected over a whole parameter range, and the conjecture has been attacked case by case for decades.
This mission asks for a formal proof of the full conjecture as stated in an OpenAI preprint dated September 25, 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. Part of the proof is a finite case analysis of 3,099 parameter-pattern instances carried out by two exact programs that accompany the paper.
All graphs are finite and simple. is the cycle on exactly vertices and the complete graph on vertices. Identify a red–blue colouring of with its red graph on vertices; the blue graph is the complement . A copy of in is an injective homomorphism (copies need not be induced). The Ramsey property says: every graph on vertices contains or its complement contains . Then
For all integers with ,
and .
The result itself. It completes a programme that over five decades settled the conjecture for , for long cycles, and for all sufficiently large by Keevash–Long–Skokan; the preprint's contribution is the remaining finite but large set of pairs. Since Keevash–Long–Skokan's constant is not explicit, the preprint gives a structural reduction that does not need a numerical value of it.
Formalizing it. The statement uses only Mathlib's cycleGraph, complete graphs, complements and subgraph containment. A formal proof would have to certify both the structural lemmas (independent-set expansion, a large-clique lemma, optimal path systems) and the finite verification of 3,099 pattern instances, which the preprint currently delegates to two programs with deduction traces. Bringing such a computation inside a proof assistant is itself a worthwhile contribution. Neither for general parameters nor any of the previously known infinite families has a machine-checked proof.
The lower bound is the explicit construction above; the work is the upper bound for exact cycle length . Methods that find long cycles (Pósa rotation, Chvátal–Erdős) produce cycles of length at least , not exactly , and forbidding exactly one cycle length gives weak structural information. The preprint passes to a minimal counterexample with independent-set expansion (Lemma 2.2, p. 4), finds a clique of order with (Theorem 3.1, p. 5), and optimizes systems of paths through that clique so that every improvement would close a cycle of order exactly . Cliques of order are excluded by hand (Proposition 8.4, p. 24); the remaining , need the finite verification of Section 9 (Proposition 9.1, p. 26).
RamseyProperty m n N: for every G : SimpleGraph (Fin N), cycleGraph m ⊑ G or (⊤ : SimpleGraph (Fin n)) ⊑ Gᶜ, where ⊑ is Mathlib's subgraph containment (injective homomorphism, non-induced).cycleCliqueRamsey m n = sInf {N | RamseyProperty m n N} in ℕ. If the set were empty, sInf would return 0; the goal's equalities exclude that, so a proof must exhibit the Ramsey property.toNat (harmless since both are at least ), and separately states cycleCliqueRamsey 3 3 = 6.cycleGraph m on Fin m is the -cycle for .Welcome contributions: a verified checker for the pattern enumeration of Section 9, and the classical small cases (, Bondy–Erdős for ).
Many questions about random graphs ask when a property — connectivity, containing a triangle, having a perfect matching — appears in the Erdős–Rényi random graph , where each of the possible edges is present independently with probability . For an increasing property the probability rises from to as grows, and the threshold width measures how quickly: the length of the interval of over which climbs from to . Friedgut and Kalai showed in 1996 that symmetry alone forces every such transition to be narrow, and conjectured the optimal universal width. This question links probabilistic combinatorics with the Fourier analysis of Boolean functions, and the influence inequalities developed for it are now standard tools in theoretical computer science and statistical physics.
Fix an integer and let be the set of unordered pairs of vertices. A graph configuration is a map (in Lean GraphConfig n := GraphEdge n → Bool, where GraphEdge n is the type of 2-element subsets of Fin n). A Boolean function on configurations is
For the graph mean is , the probability that has the property when . For the quantile is
For every , every vertex-invariant, increasing, nontrivial , and every ,
The constant is the source's explicit choice and is not claimed to be sharp; the content is the order with linear dependence on . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The bound is uniform over all monotone graph properties and is of optimal order in for fixed , as the clique example of Friedgut and Kalai shows. It settles the exponent question left open between the bound of 1996 and the bound of 1997. The driving estimate in the source, Theorem 1.2 (variance is at most times total influence, for every and without monotonicity), is a graph-symmetric influence inequality of independent interest; it removes the loss of the 2020 bound and holds at every bias.
Formalizing it. A formal proof would certify a universal statement over all graph properties with an explicit constant. The supporting library — Fourier–Walsh analysis on biased product spaces, pivotal influences, the Margulis–Russo derivative formula, and random restrictions — is reusable for other threshold and influence results, none of which are currently formalized in Mathlib in this form.
The classical route bounds the derivative from below through the largest influence, using only that the symmetry group acts transitively on edges; transitivity alone cannot give better than , because there are transitive families (on non-graph coordinate sets) whose thresholds are that wide. Reaching requires using the vertex structure of the symmetry group, and the bound must hold uniformly for every bias , including very small where hypercontractive estimates degrade. Influence estimates at alone do not suffice, since a width bound requires control throughout the transition interval.
GraphEdge n → Bool; the measure is the explicit finite sum graphMean p f with product weights or ; logarithms are natural (Real.log).graphQuantile a f is sInf of . For a nontrivial increasing , , so this set is nonempty and the infimum is not a junk value; the hypotheses NontrivialGraphProperty and exclude the degenerate cases.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.