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?
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.
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.
A set is square-difference-free if no two of its elements differ by a perfect square with . The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing for the largest size of a square-difference-free subset of , the problem is a prototype for polynomial patterns in dense sets: it is the simplest case of finding differences in the image of a polynomial, and it is the model problem on which Fourier-analytic, ergodic and density-increment methods for polynomial configurations are tested. A long-standing gap separates the upper bounds, which until recently saved only a power of (with a slowly growing exponent), from the lower bounds, which are powers and beyond. Whether a fixed power saving holds was posed explicitly by Green and Sawhney.
For a positive integer write . A set is square-difference-free if
that is, for all and all integers . (Differences are taken in ; is allowed since is excluded from the squares.)
In Lean (namespace OAI.SquareDifference), sets are Finset ℤ contained in Finset.Icc 1 N, and IsSquareDifferenceFree A states a - b ≠ (m : ℤ)^2 for all a b ∈ A and m : ℕ with 1 ≤ m.
There are absolute constants and such that for every integer and every square-difference-free ,
Equivalently, every subset of with more than elements contains two elements differing by a nonzero perfect square. The Lean goal is published on the platform with status Open. The statement fixes no numerical value of , so any improvement of the exponent leaves the goal unchanged.
The result itself. Every earlier upper bound saved less than any fixed power of ; the best, due to Green and Sawhney, saved . A fixed power saving changes the nature of the problem: it shows that the extremal exponent lies strictly below , so both upper and lower bounds are now polynomial and the remaining question is the value of the exponent, now known to lie between and . As an immediate consequence (Remark 1.2 of the source), the graph on joining integers differing by a square has chromatic number at least , a polynomial bound for the square-difference coloring problem.
Formalizing it. The statement is elementary and self-contained, involving only finite sets of integers. The proof combines a graph/tuple reformulation, reflection-positivity (chessboard) inequalities for a finite-field probability law, and an induction with fixed finite constructions. A formal proof would certify an argument whose constants are explicitly noted to be extremely small and not computed.
Density-increment arguments, starting from Sárközy's circle-method proof, gain a constant factor of density at each step but lose a power of the length of the progression on which they pass, so after the increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level- approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only . A power saving requires an argument whose loss does not compound with the number of iterations — a single estimate that converts square-difference-freeness into a polynomial density loss.
Finset ℤ inside Finset.Icc 1 N and is a natural number; the bound is uniform in .How efficiently can the edges of a graph be split into cycles? Some single edges must be allowed, since a forest has no cycles at all, and a tree on vertices already needs single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on vertices can have its edge set partitioned into simple cycles and single edges. Equivalently, every graph with all degrees even partitions into cycles. The problem is a basic question about edge decompositions, and the partial bounds , and trace several decades of progress on it.
This mission asks for a formal proof of the linear bound, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A finite simple graph has vertex set of size and edge set of unordered pairs of distinct vertices. A cycle is a closed walk of length at least with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of into parts is a family of pairwise disjoint subsets of with union , where each is either the edge set of a cycle of or a single edge of . Parts may share vertices; isolated vertices need not be covered; for an edgeless graph is allowed.
There is an absolute constant such that for every and every simple graph on vertices,
The value of is left unspecified, which keeps the goal stable under future improvements of the constant (the best possible constant is at least , by complete bipartite examples).
The result itself. The order is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp cycle bound for Eulerian graphs satisfying a large-cut condition. It removes the last iterated-logarithm loss from the Bucić–Montgomery bound.
Formalizing it. The statement uses only Mathlib's SimpleGraph.Walk.IsCycle and edge sets, so it is a clean combinatorial target. A complete development needs Lovász's path-cycle decomposition theorem, the Aharoni–Haxell hypergraph matching theorem, expansion and routing lemmas, and binomial tail bounds; all are reusable in extremal graph theory. No machine-checked proof of any bound is known.
Covering is easy (Pyber's bound), but a cover does not yield a partition: deleting repeated edges can break cycles into many paths. For partitions, the standard strategy decomposes the graph into expanding pieces at a sequence of scales, and paying a cost proportional to the full order at every scale accumulates a factor from the number of scales — this is where the and losses come from. The preprint (Introduction, pp. 2–3) charges the work on a prefix of scales to a single expanding layer and saves a fixed fraction of vertices by identifying pairs, then lifts quotient cycles back with reserved edge-disjoint routes (Lemma 3.1, p. 5); keeping a separate assignment for each original edge throughout is what makes the induction close.
SimpleGraph (Fin n) for arbitrary n (including 0 and edgeless graphs).CycleOrSingleEdge G s: either is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least ), or for an edge .EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.MainStatement: EdgeDecomposition G k .A Hadamard matrix of order is an matrix with entries whose rows are mutually orthogonal, . Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.
The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths are known, and the long-standing Barker-sequence conjecture says there are no others.
Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring .
A real matrix is circulant if there is a function with , indices taken modulo . It is a sign Hadamard matrix if every entry is or and
For a circulant sign matrix with first row , the periodic autocorrelations are ; the Hadamard condition says for .
A Barker sequence of length is with aperiodic autocorrelations
The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.
Combined with the classical odd-length classification, this gives the Barker length list .
Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters exist only for . It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.
The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.
The orthogonality condition is a norm equation in the group ring , and every character sends to a cyclotomic integer of absolute value . Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case with odd and divisible by several primes. The obstruction must combine information from all prime divisors of simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.
RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.IsSignHadamard H is entrywise IsSign (equal to or ) together with H * H.transpose = (n : ℝ) • 1.0 < n, matching the paper's "positive integer ".Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by in absolute value for .A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above , and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction , odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.
An expander graph is a sparse graph in which every set of vertices has a large edge boundary relative to its size. Expanders with bounded degree are a basic tool across combinatorics, computer science and group theory. High-dimensional expanders are simplicial complexes that extend this behavior to faces of every dimension, and coboundary expansion over is the strongest of the standard notions: the coboundary of any set of -faces must be large unless the set is already close to a coboundary. Gromov connected such filling inequalities with topological overlap of maps to Euclidean space. The basic existence question is whether there are arbitrarily large complexes of fixed dimension with bounded vertex degree and uniform coboundary expansion in every degree.
A finite simplicial complex is a downward-closed family of finite sets (faces) of vertices; denotes the faces with vertices. is pure of dimension if it has -faces and every face lies in one. An -cochain is a function ; its coboundary is . Let , with the constant functions. Faces are weighted by
so is the probability that is nonzero on a random -face of a uniformly random top face, and .
In Lean (namespace OAI.CoboundaryExpanders), a Complex has vertex set Fin vertexCount, a Finset of faces that is downward closed and contains every singleton; Pure, Connected (connected -skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts -faces containing .
For every there are , and finite connected pure -dimensional complexes with , every vertex in at most faces of dimension , and
with constants independent of , and . The Lean goal is published on the platform with status Open.
The result itself. Together with the classical graph case and the Chapman–Lubotzky two-dimensional theorem, Theorem 1.1 gives bounded-degree coboundary expanders in every positive dimension, answering the existence question in the form stated by Chapman and Lubotzky. Earlier bounded-vertex-degree constructions gave cosystolic expansion, which permits nonvanishing cohomology, or degree-one expansion only; earlier coboundary expanders in all dimensions had vertex degrees growing with size. Coboundary expansion in all degrees implies vanishing -cohomology below the top dimension, the property Gromov related to topological overlap.
Formalizing it. The definitions are elementary finite combinatorics, so the statement is completely precise; the proof combines group-theoretic coset complexes over , congruence quotients and a quantitative cosystolic input. A formal proof would require formalizing that input (Oppenheim–Valentiner-Branth), which is substantial.
Coboundary expansion requires two things at once: a quantitative isoperimetric inequality against cocycles (cosystolic expansion) and exact vanishing of for every . Random constructions give vanishing cohomology but force growing vertex degree; algebraic bounded-degree constructions (Ramanujan complexes, coset complexes) give the quantitative inequality but typically have nonzero cohomology that cannot be controlled uniformly. A cocycle that is not a coboundary has zero coboundary and positive distance, so any nonzero cohomology class destroys the inequality. The difficulty is a family of bounded-degree complexes whose cohomology vanishes in every degree below , uniformly along the tower.
Fin vertexCount and every vertex is a face; faces are Finsets, and an -face has exactly vertices.ZMod 2-valued; is the constant cochains (reduced cohomology in degree ). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.When does the Erdős–Rényi random graph contain a copy of a prescribed graph ? A necessary condition is visible from first moments: if some subgraph has expected copy count below a constant, then is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.
This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For finite simple graphs let be the number of subgraphs of isomorphic to (ordinary, non-induced copies). is the random graph on with each of the edges present independently with probability . For a graph with at least one edge and at most vertices,
The first is the containment threshold, the second the graph expectation threshold; always . Write for the number of edges.
For every and every finite simple graph with edges and at most vertices,
The constants are explicit and universal; may vary with .
The result itself. The bound says that, up to a universal constant times , the only obstruction to containing is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching while , because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing .
Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of , so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.
The abstract theorem compares with the integral expectation threshold of the family of edge sets containing a copy of , and covers of may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of . Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).
Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real but used only on .expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.criticalThreshold and expectationThreshold are sInf over ; the sets are nonempty (they contain when has at most vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is .A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an -approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness in every -edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.
Background. The maximum-entropy rounding of Asadpour et al. constructs -thin trees. Oveis Gharan and Saberi constructed -thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of -thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.
Graphs are finite undirected loopless multigraphs; parallel copies count separately. For , is the multiset of edges with exactly one endpoint in , and is -edge-connected if for every such . A spanning tree is -thin if for all such . Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.
There is an absolute constant and a deterministic algorithm that, given and a -edge-connected multigraph on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree with
returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.
The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do -thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.
StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).Valid x: , and EdgeConnected k.CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for the output is empty.Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.