Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity , a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to , does it act geometrically on hyperbolic three-space ? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.
The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.
Let be a group with a finite symmetric generating set and Cayley graph with graph distance . is hyperbolic if there is such that every point on a side of a geodesic triangle lies within of the union of the other two sides. A geodesic ray based at is a sequence with ; two rays are equivalent if stays bounded. The boundary is the set of equivalence classes with the quotient of the topology of pointwise convergence.
is the upper half-space with distance , and is its full isometry group, including orientation-reversing isometries. A homomorphism gives a proper action if is finite for every compact , and a cocompact action if translates of one compact set cover .
The Lean statement OAI.CannonRelease.cannon is open on the platform.
The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in . For torsion-free , the quotient is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.
By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.
CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number working for all geodesic triangles given as walks of length equal to graph distance.ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.EuclideanSpace ℝ (Fin 3); is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on ) or Theorem 2.5 (the uniformization criterion) are welcome.
Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like and ), axioms () and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.
A specification consists of a type of sorts, an axiom relation and a rule relation ; neither is assumed functional. Expressions are
up to renaming of bound variables. β-reduction is the compatible closure of , with steps allowed everywhere, including inside the annotation of a λ and both parts of a Π. Typing is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to ). A context is valid if each declared type is typed by a sort in the preceding prefix, and is legal in if or for some .
The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.
For every specification ,
Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.
Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.
The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.
Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.Beta.S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.Turing reducibility compares sets of natural numbers by their information content: if an oracle Turing machine with oracle computes the characteristic function of . Identifying mutually reducible sets gives the Turing degrees , partially ordered by . A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.
After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.
An oracle is a function (a set of natural numbers). means that the characteristic function of is partial recursive relative to . This is a preorder; its quotient by is the set of Turing degrees, partially ordered by . An automorphism of is a bijection with
No definability, Borel or continuity hypothesis is imposed on .
The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.
Rigidity says that the order alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.
Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as , where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.
ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values and ).Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting .A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on and , and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.
At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height . Physics heuristics (Nienhuis's Coulomb gas and the conjectured scaling limit with boundary exponent ) predict that this crossing mass decays like . Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.
The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to , and the first horizontal-displacement moment of paths returning to the starting side is comparable to (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where indexes the horizontal band. Let be the strip of bands. A path starts in the triangle up 0 0 (just above bottom port ), visits distinct triangles, moves between adjacent ones, and stays in bands . Its length is the number of visited triangles and its critical weight is with . An arch ends at up k 0 with (bottom port ); a bridge ends at a down triangle of the top band. Put and
Write if for all with fixed constants .
For every all sums above are finite, and with constants independent of ,
and is nonincreasing in .
The result itself. It establishes the predicted crossing power with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.
Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.
The boundary identity (Lemma 4.2, p. 15) does not determine the power: it only gives between orders and . The preprint's route computes the arch moment first, as one coefficient of a ratio of Pfaffians (Proposition 4.1, p. 13), converts it into a positive -fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and . A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.
ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. .Comparable f g asks for constants with for every ; powers are real rpow.Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.
A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the -regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer after proving it for large below a non-explicit constant (Nam–Sly–Zhang 2022).
This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 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 the infinite -regular tree with vertex set ; concretely, is the set of finite words over with no two equal consecutive letters, and is adjacent to . Put for . The free zero-field Ising law on is determined by its marginals on finite connected subtrees :
Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability . A spin law is a factor of IID if it is the law of for i.i.d. uniform labels and a measurable such that, for each fixed automorphism , almost surely, where .
For every integer and every ,
The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every . The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ( excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.
Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.
Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range . The Nam–Sly–Zhang approach observes and expresses the posterior through innovations , which are independent Brownian motions; but being Brownian does not make a function of , and that is the central step (pp. 2–3). At criticality the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).
TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.Measure.infinitePi of Lebesgue measure on ; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.HasFreeIsingLaw θ μ prescribes on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).θ = Real.tanh β with and ; at both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.Random 3-SAT, a conjunction of random three-literal clauses on variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near . Once a limiting threshold is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given , outputs a rational within of ? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.
The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of , beyond existence.
For , a proper random 3-clause chooses three distinct variables uniformly from and gives each an independent fair sign. Let be the conjunction of independent such clauses (sampled with replacement from the possibilities; the empty formula is satisfiable) and
A real is computable if a single algorithm, on input , halts with a rational satisfying .
There is such that for every fixed real
and one finite deterministic Turing machine, on input , halts with a rational with , using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.
The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of (Theorem 4.4) for the same proper-clause model.
The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.
Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.
ProperClause n k is Fin n → Option Bool with exactly defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to .MainStatement asserts with the two strict-side limits at , a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and for all .Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.
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 (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.
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.
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.
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.
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 ).
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.
For integers the Ramsey number is the least such that every simple graph on vertices contains a clique of order or an independent set of order . Ramsey's theorem guarantees these numbers are finite. In the off-diagonal regime, is fixed and ; the classical upper bounds give , while for a long time lower-bound constructions did not reach the power . Once the power was settled, the remaining question was the power of .
A graph on vertices is a SimpleGraph (Fin N). The Lean development defines
RamseyProperty s t N: every graph on Fin N has an -clique, or its complement has a -clique (an independent set of size );ramsey s t := sInf {N | RamseyProperty s t N}, the Ramsey number .All logarithms are natural; real powers of use Real.rpow.
For every integer there is such that for every and every sufficiently large (threshold depending on )
This is Theorem 1.1 of the source, formalized as main (s) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. Together with the companion preprint and the earlier results for on the polynomial exponent, the theorem identifies the exact power of in up to for each fixed : the classical AKS upper bound is sharp in its logarithmic exponent. It does not give a matching constant-factor lower bound. The main new ingredient is a prime-indexed construction (Theorem 1.2 of the source): for fixed and large primes , a -free graph on vertices with independence number below , built from random incident point–hyperplane flags of .
Formalizing it. The upper half is classical (Proposition 7.3 of the source restates the AKS estimate for all fixed ). The lower half is a long argument combining finite projective geometry, entropy of a selected subsequence, and incidence bounds in positive characteristic; formal verification would independently check an unrefereed claim.
Bradač's projective graph has the right number of vertices but its independent sets were only controlled up to logarithmic exponent . Improving to requires bounding long independent sequences in a random stream of flags. A union bound over sequences loses too much, and a sequence selected from the random stream need not have independent or uniform flags. The source pays for this with an entropy lower bound on the selected sequence and a compression upper bound, which in turn requires a description theorem for sparse point–hyperplane pairs in arbitrary dimension (repeated projections and a high-rank two-row description based on a finite-field Zariski-closure inequality of Nie and Wang).
SimpleGraph (Fin N); independent sets are cliques of the complement graph. ramsey is an sInf, equal to because the defining set is nonempty by Ramsey's theorem.MainBounds s fixes one (depending on ) before quantifying over ; natural subtraction s - 1, s - 2 is harmless because . MainLimit s is a Filter.Tendsto over natural .For integers the Ramsey number is the least such that every simple graph on vertices contains either a complete subgraph or an independent set of vertices. Determining how grows when is fixed and is one of the central problems of extremal and probabilistic combinatorics: upper bounds come from counting and local density arguments, lower bounds require explicit or random constructions of -free graphs with no large independent set, and for decades the two sides did not even agree on the power of .
A graph on vertices is a SimpleGraph (Fin n). A -clique is a set of pairwise adjacent vertices and a -independent set a set of pairwise non-adjacent vertices. The Lean development defines
RamseyProperty s t n: every simple graph on Fin n has an -clique or a -independent set;ramsey s t := sInf {n | RamseyProperty s t n}, the Ramsey number .All logarithms are natural.
There is an absolute constant such that for every and all sufficiently large (threshold depending on )
and consequently
This is Theorem 1.1 of the source, formalized as SharpBounds ∧ SharpExponent. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. The theorem determines up to a factor , the first case beyond in which the logarithmic exponent of a fixed off-diagonal Ramsey number is known. It shows that the classical upper-bound exponent is the truth for , and it leaves open only a constant-factor asymptotic for . The lower-bound construction (random incident point–hyperplane pairs in projective space , ordered by position) together with its entropy/compression analysis is the new part.
Formalizing it. The upper bound is an elementary argument (triangle-free independent-set bounds plus random sampling), stated separately in the source as Theorem 2.1 for all ; its formalization is a self-contained milestone. The lower bound is a long probabilistic and finite-geometric argument whose formal verification would independently certify an unrefereed claim.
The lower bound needs a -free graph on about vertices with no independent set of size . Random graph processes lose logarithmic factors and even the power of ; Bradač's projective graph has the right power but its independent sets were only controlled to logarithmic exponent . The obstacle is to bound long independent sequences in a random stream of flags: a direct union bound over sequences is far too weak, and the selected sequence can have a heavily biased law. The source handles this with an entropy lower bound and a matching compression (description) upper bound that relies on a new theorem about sparse point–hyperplane incidences.
SimpleGraph (Fin n); cliques and independent sets use Mathlib's IsNClique and IsNIndepSet. ramsey is an sInf, which is the true Ramsey number because the defining set is nonempty by Ramsey's theorem; a proof must use that nonemptiness rather than the junk value 0.SharpBounds fixes one before ; the threshold may depend on . The power is Real.rpow. SharpExponent is a Filter.Tendsto statement over natural with real logarithms.The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted -positivity for incomparability graphs of -free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a -graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in with nonnegative integer coefficients. The -refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.
Let be weakly increasing with . The natural unit interval graph has vertices and edges with . A proper coloring gives different colors to adjacent vertices, and counts edges with . The chromatic quasisymmetric function is
For a partition , with . Let be the set of permutations (as words ) such that every adjacent descent is an edge, and the number of inversions , , with an edge.
In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is in variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define and ; a PermutationWitness is a map together with the identity below in every number of variables, using Mathlib's MvPolynomial.esymmPart.
For every and every natural unit interval graph on there is a map with
In particular every elementary coefficient of lies in . The goal is published on the platform with status Open.
The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at , via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.
Formalizing it. The statement is a finite polynomial identity for each , and , fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.
The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at , and Hikita's probabilistic formula has rational -weights that are only positive at real , not coefficientwise. A proof over must produce, for each elementary partition and each power of , a nonnegative integer count, uniformly over all graphs.
h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are in either order.Fin r and the identity is required for every , which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree .Polynomial ℕ, so nonnegativity in is built into the statement; the witness theta is an arbitrary function on the finite set . The source's additional assertion that is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.Kazhdan–Lusztig polynomials are integer polynomials attached to pairs of elements of a Coxeter group. They were introduced through the canonical basis of the Hecke algebra (Kazhdan–Lusztig, 1979). For Weyl groups they compute local intersection cohomology of Schubert varieties, and they enter the Kazhdan–Lusztig conjectures on characters of highest-weight representations. Their definition uses the simple generators of the group, yet in every known example seemed to depend only on the Bruhat interval as an abstract partially ordered set. The combinatorial invariance conjecture, attributed to Lusztig and Dyer, asserts this: if two Bruhat intervals, possibly in different Coxeter groups, are isomorphic as posets, their Kazhdan–Lusztig polynomials coincide.
This mission asks for a formal proof of the conjecture, 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 Coxeter system is a group with a generating set of involutions subject only to relations . Write for word length in . A reflection is a conjugate of an element of . Bruhat order is the partial order generated by whenever is a reflection and ; the interval is finite and graded of rank , even when is infinite. The equal-parameter R-polynomials and Kazhdan–Lusztig polynomials are the unique families with , unless , the recursion: for with ,
the degree bound for , and the inversion formula
Let and be arbitrary Coxeter systems, in and in . If is an isomorphism of posets (a bijection preserving and reflecting order), then
The isomorphism carries no labels or root data; the groups may be infinite and noncrystallographic.
The result itself. It shows that a Kazhdan–Lusztig polynomial, defined algebraically from the Hecke algebra, is determined by a finite poset. Restricting to subintervals gives the same for every with , and hence for the R-polynomials (Corollary 6.1, p. 29). For Weyl groups this means that local intersection cohomology of Schubert varieties is determined by the Bruhat poset. It settles a question open since the 1980s that had been verified only for lower intervals, short intervals, low ranks, and single coefficients.
Formalizing it. Mathlib has Coxeter systems and their length function but no Bruhat order, Hecke algebra, or Kazhdan–Lusztig theory. The proof uses reflection orders (Dyer's path formula, Theorem 2.2, p. 7), Braden–MacPherson moment-graph sheaves over a reflection-faithful real realization (Theorem 2.3, p. 8), and the Elias–Williamson character theorem as external inputs. Building these would be a substantial, reusable contribution to formal representation theory.
The defining recursion uses a simple generator with , but a poset isomorphism need not carry simple generators or reflections to anything recognisable, and need not respect root labels. Dyer's reconstruction recovers all reflection edges of the Bruhat graph from the order (Theorem 3.4, p. 12) but not their labels. Lanini's moment-graph invariance requires compatible label automorphisms, which an abstract isomorphism does not provide. The preprint therefore keeps the two realizations separate, transports reflection orders through maximal dihedral subintervals (Proposition 3.5, p. 13), counts later edges exactly, and compares images of edges in two different sheaves by a reciprocal inequality that is then forced to be an equality (Sections 5–6).
CoxeterSystem M W for arbitrary index types and groups; the two systems may live in different universes.BruhatLE is the reflexive–transitive closure of with a reflection and , i.e. strong Bruhat order (not weak order). Interval cs u b carries this order; ι is an order isomorphism ≃o.klPolynomial is the second component of Classical.epsilon (NormalizedKL cs), where NormalizedKL encodes exactly the normalization above (R-recursion with left multiplication, diagonal and vanishing conditions, , and the inversion formula with Polynomial.reflect). Existence and uniqueness of such families is the classical Kazhdan–Lusztig theorem, and a proof of the goal has to establish them, since otherwise Classical.epsilon returns an arbitrary pair.finsum; intervals are finite, so this is the ordinary sum.Welcome contributions: Bruhat order and its basic properties (subword property, finiteness of intervals), R-polynomials, and existence and uniqueness of Kazhdan–Lusztig polynomials for arbitrary Coxeter systems.
A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number is the minimum size of a cover, and the matching number is the maximum number of pairwise disjoint edges. In an -partite -uniform hypergraph the vertices are split into parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts
For it is Kőnig's theorem, so it proposes a higher-dimensional analogue of the most basic min–max theorem of bipartite matching theory. In the intersecting case () it asks for a cover of size , and it is equivalent to Gyárfás's conjecture that monochromatic trees cover any -edge-coloured complete graph.
Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through ; Haxell and Scott (2012) proved for (doi:10.37236/1175); Francetić, Herke, McKay and Wanless (2017) handled linear intersecting hypergraphs through rank nine (doi:10.1016/j.ejc.2016.10.004); Bishnoi, Das, Morris and Szabó (2021) treated -intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever is a prime power; equality examples were studied by Mansour, Song and Yuster (2009, doi:10.1007/s00373-008-0821-9), Aharoni, Barát and Wanless (2016, doi:10.1007/s00373-015-1575-9) and Abu-Khazneh, Barát, Pokrovskiy and Szabó (2019, doi:10.1016/j.jcta.2018.07.011). Clow, Haxell and Mohar disproved Lovász's stronger matching-reduction conjecture at (doi:10.1007/s00493-026-00220-3), without contradicting Ryser's inequality.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims intersecting counterexamples for ranks .
A finite hypergraph is a finite set of edges, each a finite set of vertices. It is -partite -uniform if there is a map assigning each vertex one of parts such that every edge contains exactly one vertex of each part. It is intersecting if it is nonempty and any two distinct edges share a vertex, so . Every edge of an intersecting hypergraph is itself a cover, so always; a counterexample to Ryser's conjecture in the intersecting case needs .
There are a prime with and such that for every prime , , an intersecting -partite -uniform hypergraph with and exists.
There is such that for every prime with there is such that for every odd , with , there is a finite intersecting -partite -uniform hypergraph with
In particular infinitely many ranks fail. Lean: OAI.RyserOdd.eventualOddFailures_and_infinite, open on the platform.
The theorem would disprove Ryser's conjecture in its intersecting case, and through the standard transfer (Corollary 1.2) also Gyárfás's monochromatic tree-cover conjecture, for the ranks . The value is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime , with balanced parts); the two constructions are independent apart from three elementary estimates. Thresholds are not numerical. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
The truncated-plane examples sit exactly at , and covers may mix vertices from different parts, so enlarging individual parts does not help. One must insert exceptional edges that destroy every cover of size while preserving the intersecting property. Ruling out all small covers requires showing that any small cover contains almost a full pencil of lines, which over needs an incidence bound with a power saving (a Bourgain–Katz–Tao-type sum–product estimate) valid in fields whose proper subfields are small. This is where odd exponents and the congruence enter.
Hypergraph V := Finset (Finset V) over a finite type V with decidable equality.RPartiteUniform r H: some part : V → Fin r with exactly one vertex of each part in every edge. Uniform r H: every edge has r vertices.Intersecting: distinct edges meet. matchingNumber is the maximal size of a pairwise disjoint subfamily; coverNumber is sInf of cover sizes, and existence of a cover is asserted separately so the sInf is not the empty-set default.ExplicitFailureAt r packages all of these with , and ; the goal asserts it for the stated ranks and that the set of failing ranks is infinite.Needed infrastructure: finite fields and their projective planes, incidence and sum–product estimates, and probabilistic selection arguments. Contributions formalizing Theorem 2.1 (uniform incidence saving), Lemma 3.2 (line covers after random deletions) or Theorem 4.1 (compatible translates from independent pools) are welcome.
A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number is the minimum size of a cover, and the matching number is the maximum number of pairwise disjoint edges. An -partite -uniform hypergraph has disjoint vertex parts, and every edge takes exactly one vertex from each part. Ryser's covering conjecture asserts that every such hypergraph satisfies
For this is Kőnig's theorem for bipartite graphs, so the conjecture is a proposed higher-dimensional Kőnig theorem. Its intersecting case (, bound ) is equivalent to Gyárfás's conjecture that every -edge-coloured complete graph can be covered by monochromatic trees, which connects it to Ramsey-type covering problems.
The source of this mission, an OpenAI preprint dated September 27, 2026, claims counterexamples to the conjecture itself, already in the intersecting case and with all parts of equal size.
Fix . A -partite -uniform hypergraph on parts is given by its edge set, each edge choosing one vertex in every part. It is intersecting if it has at least one edge and any two edges share a vertex (necessarily in the same part). A vertex is nonisolated if it lies in some edge. For an intersecting hypergraph , so Ryser's conjecture predicts .
The natural extremal example comes from the affine plane : one part per direction, one vertex per line, one edge per point. It is intersecting with , attaining the conjectured bound.
There is such that for every prime there exists a finite intersecting -partite -uniform hypergraph with
and every vertex lies in an edge. Lean: OAI.Balanced.main_result, open on the platform.
Since and , the theorem would disprove Ryser's conjecture for infinitely many , in its intersecting case. The value is the largest possible for an intersecting -uniform hypergraph (any edge is a cover), and the part sizes are the smallest compatible with , so the examples are extremal in both respects. Via the standard transfer (Corollary 1.2) they also disprove Gyárfás's tree-cover conjecture for colours. The threshold is not explicit. A companion preprint of the same family gives counterexamples over extension fields without balance. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
The affine-plane example sits exactly at the conjectured bound, and its minimum covers are rigid (parallel classes). Raising by one requires adding edges that destroy every -element cover while keeping the hypergraph intersecting and keeping only vertices per part; adding a new part, as Abu-Khazneh et al. did, changes and only reaches equality. Verifying that no cover of size survives requires controlling all small sets of lines, which the paper does with stability results for line covers in prime-order planes and a probabilistic selection.
PartiteHypergraph r n has vertex set Fin r × Fin n and edges a Finset (Fin r → Fin n); an edge contains the vertices .Intersecting: edges nonempty and any two edges agree in some coordinate. Nonisolated: every lies in some edge. HasCoverNumber H k: some cover has exactly vertices and every cover has at least .MainResult: ∃ q₀, ∀ q ≥ q₀, q.Prime → ∃ H : PartiteHypergraph (q+1) (q+1), Intersecting ∧ Nonisolated ∧ HasCoverNumber (q+1).ZMod q.Contributions formalizing the deterministic reduction (Proposition 2.1), the stability of affine line covers (Lemma 3.3, building on Szőnyi–Weiner), or the selection step (Proposition 5.1) are welcome, as is the monochromatic tree-cover corollary.
In 1933 Borsuk asked whether every bounded set of positive diameter in can be split into pieces of strictly smaller diameter. The answer is yes in dimensions and for smooth convex bodies, and a regular simplex shows that pieces may be necessary. Kahn and Kalai showed in 1993 that the answer is no in high dimensions, and since then the question has been: in which dimensions does Borsuk's assertion first fail? The smallest known counterexample dimension measures how far our understanding of diameter partitions extends; it has been reduced from to by combinatorial constructions, while the assertion is open in all dimensions between and the current record.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a counterexample in dimension .
For a bounded set of positive diameter, is the least number of subsets of strictly smaller diameter that cover (covers and partitions give the same number). Borsuk's assertion in is that for every such .
Let be the real symmetric matrices with the Frobenius norm . The trace-one hyperplane in is a -dimensional affine Euclidean space. For a unit vector , is the orthogonal projector onto the line . Two such projectors are at distance exactly when the lines are orthogonal.
The set
is compact, has Frobenius diameter , and cannot be covered by ten subsets of diameter strictly less than . Hence and Borsuk's assertion fails in dimension . The Lean statement OAI.BorsukNine.main_theorem is open on the platform.
The theorem lowers the smallest known counterexample dimension for Borsuk's conjecture from to , and the paper extends it to compact counterexamples in every dimension (Corollary 7.1). Unlike previous counterexamples, which are finite point sets built from codes or strongly regular graphs, the witness is a continuum: the image of real projective -space under the projector embedding. The theorem does not determine the smallest failing dimension (the assertion remains undecided in dimensions to ) or the exact value of .
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would combine metric geometry, an algebraic-topological degree argument and a finite combinatorial obstruction.
Previous counterexamples use finite sets where a counting argument (Frankl–Wilson type) forces many parts; such counting gives nothing for a -dimensional continuum. For , a cover by ten small sets corresponds to ten nonnegative functions on summing to one, with orthogonal lines never sharing a positive coordinate. One would like to use the minimal number of vertices of a triangulation of (Walkup: eleven), but the positive-support complex arising from such functions is not a triangulation, so its face structure has to be derived from the map itself.
EuclideanSpace ℝ (Fin 4); matrices are EuclideanSpace ℝ (Fin 4 × Fin 4), whose norm is the Frobenius norm. projector u has entries .projectorSet is the image of the unit sphere; traceOneSymmetric is the set of symmetric matrices of trace .HasTenSmallCover: ten subsets of projectorSet covering it, each with Metric.diam < √2. Requiring the pieces to lie in loses no generality, and keeps Metric.diam away from its default value for unbounded sets.IsCompact projectorSet, containment in traceOneSymmetric, Metric.diam projectorSet = √2, and ¬ HasTenSmallCover.A complete development needs partitions of unity, mod-two degree of odd maps on spheres, local preimage counting, and a finite combinatorial case analysis on labelled supports. The finite combinatorial part (Sections 5–6) and Lemma 2.4 (reduction to strict gaps) are self-contained and welcome first contributions.
A measure-preserving transformation of a probability space acts on square-integrable functions by the Koopman operator , a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on , the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by on ? Equivalently, is there a single function whose bilateral orbit under is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.
Let and let be normalized Lebesgue (Haar) measure on . A bijection is a diffeomorphism if and lift locally to maps of . It is volume preserving if for every measurable . Let be the closed subspace of complex square-integrable functions with integral zero, and . Let be Haar measure on the circle and the first Fourier character.
In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.
There exist a volume-preserving diffeomorphism of and a real-valued such that
moreover is ergodic, and there is a unitary with
The goal is published on the platform with status Open.
The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is , and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time- maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).
Formalizing it. The statement exercises Mathlib's spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the topology and in spectral norms.
Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map , requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.
Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; is an Equiv.Perm with Smooth T and Smooth T.symm (local lifts), and MeasurePreserving T μ μ.Lp ℂ 2 μ with zero integral; is real-valued almost everywhere. The orbit is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by .W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if , no polynomial-time algorithm achieves a factor below in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached , leaving a gap between and .
This mission asks for a formal proof that the threshold is exactly , as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time -approximation for every fixed , and hence, under , an infimal approximation factor of exactly . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
An instance consists of points with a rational distance table that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set , a facility set (index sets that may overlap), and an integer , encoded in binary. A feasible solution is a nonempty with . An algorithm is an -approximation if it always outputs a feasible with , and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.
For every fixed there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible with
If , then
The infimum is not asserted to be attained.
The result itself. It closes the approximability of metric -median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search (), bi-point rounding (, ) to . It shows that the FPT factor of Cohen-Addad et al. is achievable in polynomial time. The case has a different and still separate lower-bound question.
Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.
Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max--Coverage gap.
Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size .FactorCorrect α I out requires that mask to describe a nonempty with and .Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.approximationFactors is the set of admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.