Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The spherical perceptron assigns random rewards to vectors of fixed length. The source asks for an exact pressure formula without a convexity or symmetry condition on the single-pattern potential. The source is OpenAI's September 2026 manuscript.
Configurations lie on the sphere of radius , equipped with uniform probability measure. There are independent Gaussian patterns. The variational value minimizes a Brownian stochastic-control functional plus an extended nonnegative entropy over monotone trials.
For a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.
The goal is OAI.SphericalPerceptronFreeEnergy.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected main target proves finiteness of the variational value, convergence of expected pressure, and concentration around the same number. The linear-field formula is attached as a supporting result. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
An infimum involving a possibly infinite entropy must be connected with the actual finite-dimensional spherical integral. The potential is only bounded and continuous, so smoothness cannot be assumed.
Density and inverse temperature are strictly positive. Controls are progressively measurable for the stated Brownian filtration and have finite cost. Dimension is written as to stay positive. The Brownian and cascade-based linear-field definition groups are independent references.
The shared definitions are supplied by PerceptronFreeEnergy, SphericalField. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.
An overlap path is an almost-everywhere class on with a monotone representative taking values in . The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.
For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.
The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.
The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.
The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.
The shared definitions are supplied by IsingFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A diluted spin glass has finitely many interactions per spin on average. The source seeks the exact thermodynamic pressure using a hierarchy of random local-field laws. The source is OpenAI's September 2026 manuscript.
The pressure is the expected logarithm of the partition function divided by the number of Ising spins. A Poisson number of even-arity interactions and independent external fields define the model. The cavity functional uses nested probability laws and iterated logarithmic power means.
For every model of a diluted p-spin glass with Ising spins in {+1,-1} that satisfies the standing admissibility hypotheses, the free-energy density F_N converges, as N tends to infinity, to a variational value, so existence of the thermodynamic limit is part of the conclusion. A model consists of a density α ≥ 0, a probability law on interaction samples (θ, a, b, f), where θ is a real function on spin configurations in {±1}^p, a and b are reals and f assigns to each of the p slots a real function on spins, and a probability law for the external field on ℝ. Admissibility means: p is even and at least 2; α > 0; ‖θ‖ = max_s |θ(s)| and |h| are integrable under the disorder and field laws; almost surely a > 0 and, for every configuration s, exp θ(s) = a(1 + b ∏_l f_l(s_l)) with |b ∏_l f_l(s_l)| < 1; the functions f_1,…,f_p are independent and identically distributed, b is independent of the vector f, every power (−b)^n with n ≥ 1 is integrable, and E[(−b)^n] ≥ 0. No boundedness of interactions, fields or messages is added. F_N is (1/N) times the expectation of log Σ_σ exp(−H), where the number k of interactions is Poisson with mean αN, the k interactions are independent disorder samples, the N fields are independent field samples, and each interaction is placed on p index choices in {1,…,N} (repetitions allowed) averaged uniformly over all choices; here the log-weight of σ is Σ_j θ_j(σ at the chosen indices) + Σ_i h_i σ_i. The limit is the infimum over depths r ≥ 0 of φ_r, itself the infimum, over a nested law ζ in the r-fold hierarchy of probability measures (each level with the weak topology and its Borel σ-field) and exponents 0 < m_1 < … < m_r < 1, of the cavity functional B_r. B_r equals log 2 plus the Poisson(αp)-averaged expectation of the site term, a logarithm of an average over spin ε of exp(hε + Σ_j message_j(ε)), minus α(p−1) times the expectation of the log of the edge weight, with both terms evaluated through iterated log power-means in the exponents m_i.
The goal is OAI.DilutedSpinGlass.mezard_parisi.
The equality identifies the limit with the infimum over all finite hierarchy depths. Existence of the thermodynamic limit is part of the conclusion, not an assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Upper bounds at each hierarchy depth do not yield equality with the infinite-size model. Unbounded disorder requires retaining integrability hypotheses through nested expectations.
The admissibility predicate requires positive density, even arity at least two, first moments, the specified interaction factorization, and positivity and integrability of the relevant powers. The statement adds no boundedness restriction on interactions, fields, or trial messages.
The shared definitions are supplied by DilutedSpin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Escape to infinity can be arbitrarily slow for a general stochastic process. The source asks whether independent uniformly elliptic lattice environments force a positive deterministic speed whenever a direction is transient. The source is OpenAI's September 2026 manuscript.
Uniform ellipticity provides one positive lower bound for all step probabilities, almost surely at every site. Directional transience means the position projected onto a fixed unit vector tends to positive infinity almost surely under the law averaging environment and walk.
The theorem (admitted, not proved here) states that, for every dimension d ≥ 2 and every Borel probability measure ν on the set of transition rows (a row is a probability vector p over the 2d nearest-neighbour directions ±e_i of ℤ^d, with entries nonnegative and summing to 1), the following holds. Suppose ν is uniformly elliptic, meaning there is κ > 0 with p(e) ≥ κ for every direction e, for ν-almost every row p. Let ℓ be a unit vector in ℝ^d (ℓ·ℓ = 1), and suppose the walk is directionally transient in direction ℓ. Here the environment assigns to each site of ℤ^d an independent ν-distributed row, the walk starts at the origin and at each step moves from its current site x in direction e with probability given by the row at x, and the annealed law averages over the environment and the walk. Directional transience means that, almost surely under this annealed law, the inner product of the walk position X_n with ℓ tends to +∞ as n → ∞. The conclusion is that there exists a vector v ∈ ℝ^d with v·ℓ > 0 such that the walk has asymptotic velocity v, that is, X_n/n → v as n → ∞ almost surely under the annealed law. In other words, directional transience of an i.i.d. uniformly elliptic random walk in random environment in dimension at least two implies ballisticity with a nonzero velocity having positive component along ℓ.
The goal is OAI.DirectionalTransience.directional_transience_implies_ballisticity. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen central target converts almost-sure transience to a velocity statement in every dimension at least two. The separate dimension-at-least-three statement starts from positive probability and identifies the transient hemisphere. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Transience controls eventual direction but not the time spent in traps. A law of large numbers with positive projected velocity needs quantitative control of these delays.
The main statement assumes , a unit direction, and an independent identically distributed uniformly elliptic environment. The supporting hemisphere target assumes and a nonzero direction. Their original definition groups stay separate.
The shared definitions are supplied by DirectionalBallisticity, VelocityHemisphere. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A random environment can favor different directions at different sites. The source asks whether escape in one prescribed real direction can have an intermediate probability after averaging over the environment. The source is OpenAI's September 2026 manuscript.
A transition row assigns probabilities to the nearest-neighbor steps of the integer lattice. Rows at different sites are independent and have the same law. Strict ellipticity means every step probability is positive almost surely, without a common positive lower bound.
For every dimension d ≥ 3, a random walk in an i.i.d. random environment on the lattice ℤ^d obeys a directional zero-one law. Here a row at a site is a probability vector p on the 2d nearest-neighbour steps (coordinate direction i in Fin d, sign + or −), with each p(e) in [0,1] and the entries summing to 1. The environment assigns an independent row to every site, each drawn from a probability measure μ on rows, and the strict ellipticity hypothesis on μ says that μ-almost every row gives every one of the 2d steps strictly positive probability. Given the environment, the walker at site x moves to x plus the unit vector of step e with probability p_x(e); the annealed law of the path started at 0 averages over both the environment and the walk. For any nonzero real vector ℓ in ℝ^d, the escape event is that the path X satisfies Σᵢ Xₙ(i)·ℓᵢ → +∞ as n → ∞, that is, the walk tends to infinity in the direction ℓ. The conclusion is that the annealed probability of this event, starting from 0, is either exactly 0 or exactly 1.
The goal is OAI.DirectionalZeroOne.directional_zero_one.
The target gives a directional zero–one law under positivity alone. It makes no moment or uniform ellipticity assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Revisiting sites reuses the same random transition row, so path increments are not independent under the averaged law. Ordinary zero–one laws for independent increments do not directly apply.
Lean builds the annealed path measure through a Markov kernel on environment-position pairs. The starting site is the origin, the direction is any nonzero real vector, and escape means the scalar projection tends to positive infinity.
The shared definitions are supplied by DirectionalWalk. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.
A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on , while the same spins are pinned on and a target event is prescribed on .
A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).
The goal is OAI.BufferedIsing.finite_graph_comparison.
The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.
The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.
The shared definitions are supplied by BufferedIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
On an expanding infinite graph, the appearance of an infinite open cluster and the appearance of a unique one can occur at different densities. The source seeks a nonempty interval where infinitely many infinite clusters coexist. The source is OpenAI's September 2026 manuscript.
In bond percolation, edges are independently retained with probability . The critical threshold records appearance of infinite clusters; records uniqueness. The intermediate operator threshold records boundedness on of the two-point connection kernel.
For a bond graph G, given by a map from an edge type E to unordered pairs of vertices in an infinite vertex type V, that is connected, locally finite (each vertex lies in finitely many edges) and quasi-transitive (finitely many vertex representatives such that every vertex is the image of one under an automorphism of G acting on vertices and edges), and whose vertex isoperimetric constant hV(G), the infimum over nonempty finite vertex sets A of |outer vertex boundary of A|/|A|, is strictly positive, the MainConclusion holds for Bernoulli bond percolation on G. Writing pc for the infimum of parameters p at which an infinite cluster occurs with positive probability, pu for the infimum of p at which there is almost surely exactly one infinite cluster, ptwo for the supremum of p at which the two-point function τ_p(x,y)=P_p(x connected to y) is the matrix kernel of a bounded operator on ℓ²(V), and operatorNorm(p) for the infimum of operator norms of such operators, valued in [0,∞], the conclusion has four parts. First, the supremum of operatorNorm(p) over p<pc equals operatorNorm(pc). Second, operatorNorm(pc) is finite. Third, pc<ptwo≤pu. Fourth, there exist p₁<p₂<1 with pc<p₁ such that, for almost every i.i.d. uniform [0,1] edge labelling, for every p in [p₁,p₂] the configuration of edges with label at most p has infinitely many infinite clusters. The proof is omitted (sorry) in the source.
The goal is OAI.Percolation.BenjaminiSchramm.full_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The full goal also identifies the critical norm as the supremum from below and supplies simultaneous nonuniqueness over a fixed interval under the uniform-label coupling. Supporting statements cover critical laws and Cayley graphs. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A separate almost-sure statement at each parameter does not establish one event valid for every parameter in an interval. Critical operator control must also survive the passage to the threshold itself.
The graph has infinitely many vertices, is connected and locally finite, has finitely many vertex orbits, and has positive vertex isoperimetric constant. Thresholds lie in the unit interval; operator norms may take extended nonnegative values. The independent Cayley definition group is retained separately.
The shared definitions are supplied by BenjaminiSchramm, CayleyPercolation. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Random edge travel times produce a deterministic large-scale shape. The source studies two distinct regularity questions: corners and flat boundary segments. The available exponential target addresses differentiability and the structure of supporting lines. The source is OpenAI's September 2026 manuscript.
In first-passage percolation, travel time is the infimum of path costs on the nearest-neighbor square lattice. A time-constant norm gives the asymptotic travel time in each direction. Its unit ball is the limit shape.
For any probability space (Ω, P) carrying an edge-weight family τ indexed by the edges of the nearest-neighbour lattice ℤ², where each vertex p has an east edge (p,false) and a north edge (p,true), such that the τ(e) are measurable, mutually independent, and each has the exponential distribution with rate 1 (the ExponentialEnvironment hypothesis), there exists a function μ on the plane ℝ² with the following properties. First, μ is a norm: nonnegative, zero only at the origin, subadditive, and satisfying μ(av)=|a|μ(v) for all real a. Second, μ is the time constant: for every v in ℝ², almost surely the first-passage time from (0,0) to the lattice point (⌊tv₀⌋,⌊tv₁⌋), defined as the infimum of path costs over nearest-neighbour step sequences (east, west, north, south) that sum the edge weights along the path, divided by t, converges to μ(v) as t→∞. Third, μ is Fréchet differentiable at every nonzero point. Fourth, at every point v with μ(v)=1 there is exactly one linear functional ℓ with ℓ(v)=1 and ℓ(w)≤μ(w) for all w. Fifth, the unit sphere of μ is a C¹ curve in the sense that near each point v with μ(v)=1 there is an open neighbourhood U and a C¹ function g on U whose zero set in U is exactly the set where μ=1, with g having a nonzero Fréchet derivative at each of those zeros. Sixth, for each boundary point v of the unit ball {μ≤1}, there is a unique line L that is the level set {z : g(z)=g(v)} of some nonzero continuous linear functional g that attains its maximum over the unit ball at v, so each boundary point has a unique supporting line. Seventh, every boundary point v of the unit ball has a C¹ curve chart: an open neighbourhood U of v and a C¹ map γ:ℝ→ℝ² with nowhere vanishing derivative, together with a function θ continuous on U, such that γ takes values in the boundary within U, θ(γ(t))=t for all t, and γ(θ(z))=z for each boundary point z in U.
The goal is OAI.PlanarFPP.manuscriptMain. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen target supplies the norm and its limiting interpretation, unique normalized supporting functionals, unique supporting lines, and boundary charts. The Gamma-law differentiability statement is retained as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Pointwise convergence to a norm does not imply differentiability of that norm. Excluding corners requires additional information about nearby directions, and the chart conclusion requires regularity beyond mere continuity.
The main target uses independent rate-one exponential weights. It does not assert strict convexity, despite the broader manuscript title; strict convexity is not added implicitly. The Gamma target has arbitrary positive shape and rate. Each original definition group remains independent.
The shared definitions are supplied by GammaPassage, PlanarFirstPassage. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A finite algebra has a lattice of congruences, ordered by inclusion. The source studies which finite lattices arise in this way, and the available goal captures its colored-graph characterization. The source is OpenAI's September 2026 manuscript.
A congruence is an equivalence relation preserved by every basic operation of an algebra. A graph witness assigns lattice-valued colors to pairs of finitely many vertices, with symmetry, diagonal, triangle, separation, and seed-connectivity conditions.
For any finite type Lat carrying a lattice structure with a least element ⊥, Lat is Representable if and only if it HasGraphWitness. Representable means that there is a positive size n and an algebra on Fin n (a finite list of operations, each of some finite arity, acting on the carrier) such that Lat is order-isomorphic to the poset of congruences of that algebra, where a congruence is an equivalence relation compatible with every operation: if corresponding arguments are related coordinatewise, the outputs are related; congruences are ordered by the inherited order on equivalence relations. HasGraphWitness means that there is a positive size n and a Lat-valued coloring color of ordered pairs from Fin n satisfying five conditions: color is symmetric; color(a,b)=⊥ exactly when a=b; color(a,b) ≤ color(a,m) ⊔ color(m,b) for all a, b, m; whenever lower ≰ upper in Lat, some pair has color ≤ lower but not ≤ upper; and for every nonempty finite set of seed pairs, any pair whose color is at most the join of the seed colors is connected to the seeds. Connected is the equivalence closure of the relation Marked, where a,b are Marked if some self-map p of the vertices satisfies color(p x,p y) ≤ color(x,y) for all x,y and sends some seed pair (s,t) to (a,b).
The goal is OAI.FiniteCongruence.graph_criterion.
The equivalence provides a finite combinatorial certificate for representation as an entire congruence lattice. It is the characterization component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Representing a lattice inside a congruence lattice is weaker than obtaining all congruences. The witness’s seed-connectivity condition must capture this fullness and work in both directions.
The lattice is finite and has a least element. The algebra carrier and graph witness carrier each have positive finite size. Operations have finite arities, and representation is an order isomorphism. The manuscript’s undecidability conclusions are not among the attached targets.
The shared definitions are supplied by FiniteCongruenceGraph. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The odd-characteristic version of direct finiteness has different coefficient constraints from the binary case. The source fixes one odd prime and links a group-algebra counterexample to a cellular automaton. The source is OpenAI's September 2026 manuscript.
For a finitely supported coefficient function on a group, the cellular map sends a configuration to . The prime is the smallest prime factor of , where is a fixed central binomial coefficient.
The defined proposition MainClaim holds. Here sourceM is the central binomial coefficient C(1200,600), and sourcePrime is the smallest prime factor of (sourceM!)²+1. MainClaim asserts that this number p is prime and odd, and that there exist a finite field K of characteristic p with exactly p⁴ elements and a finitely generated group G containing a nontrivial element of finite order, together with two elements a and b of the group algebra K[G] such that ab = 1 but ba ≠ 1. Moreover, for the map cellular(b) sending x : G → K to g ↦ Σ_u b(u)·x(g·u), the sum running over the support of b, this map is injective but not surjective. The formal statement is admitted in the source rather than proved here.
The goal is OAI.OddKaplansky.main_theorem.
The conclusion combines a scalar one-sided inverse with failure of surjectivity of a finite-memory linear map. It specifies the characteristic and field size without claiming the construction works at every odd prime. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The group must retain nontrivial torsion while supporting the required finite sums. Matrix-level relations and an arbitrary choice of characteristic do not meet this target.
The goal unfolds MainClaim. It proves primality and oddness of the fixed sourcePrime, then existentially supplies the finite field, finitely generated group, nontrivial finite-order element, and algebra elements. The cellular convention uses right-translated inputs .
The shared definitions are supplied by OddKaplansky. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The determinant of a nonsingular integer matrix has absolute value at least one. The source examines the proposed counterpart for integer matrices over group rings, where the determinant is defined by an operator trace. The source is OpenAI's September 2026 manuscript.
The left regular operator associated to a group-ring matrix acts on by finite convolution. Its Fuglede–Kadison determinant in the invertible case is the exponential of half the real trace of the logarithm of its positive square.
The defined proposition MainStatement holds, i.e. there exist a group G that is finitely generated, an integer n ≥ 1, an n×n matrix A with entries in the integral group ring ℤ[G], and a bounded ℂ-linear operator T on the Hilbert space l²(G)^n (square-summable complex functions on Fin n × G) such that four conditions hold. First, the image of A in the rational group ring ℚ[G] (obtained by applying the integer-to-rational map to every coefficient) is an invertible matrix over ℚ[G]. Second, T is exactly the left-regular operator of A, meaning (Tξ)(i,h) = Σ_j Σ_g a_{ij}(g) ξ(j, g⁻¹h), where a_{ij}(g) ∈ ℤ is the coefficient of g in the entry A_{ij}. Third, T is invertible as a bounded operator on l²(G)^n. Fourth, its Fuglede–Kadison determinant fkDet(T) = exp(Re tr(log(T*T))/2) satisfies 0 < fkDet(T) < 1, where tr(S) = Σ_i ⟨e_i, S e_i⟩ is the unnormalized trace summing over the basis vectors e_i supported at the identity element of G in component i, and log is the continuous functional calculus logarithm.
The goal is OAI.GroupRingDeterminant.main.
The goal gives a square-matrix obstruction with both a rational group-ring inverse and a bounded operator inverse. This keeps the logarithm in the invertible setting. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The trace logarithm is not an ordinary finite-dimensional determinant polynomial. The algebraic matrix and bounded regular operator must be shown to match exactly before the determinant estimate is meaningful.
The group is finitely generated and . Lean uses complex square-summable functions on Fin n × G, the unnormalized matrix trace, and continuous functional calculus for the logarithm. Invertibility is explicit on both the rational matrix and the operator.
The shared definitions are supplied by GroupRingDeterminant. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Finite-dimensional linear algebra makes a one-sided inverse two-sided. The source asks whether finite support in a group algebra can replace finite dimension and presents a characteristic-two counterexample. The source is OpenAI's September 2026 manuscript.
The group algebra consists of finitely supported functions on a group with convolution multiplication. A ring is directly finite if always implies .
There exist a finite field K of characteristic 2 and a finitely presented group G such that G contains an element g of odd prime order ℓ (that is, orderOf g = ℓ with ℓ prime and odd), and the group algebra K[G] (the monoid algebra of G over K) contains elements a_out and b_out with a_out · b_out = 1 but b_out · a_out ≠ 1. Thus K[G] fails to be directly finite, giving a counterexample to direct finiteness. The statement is existential: it does not name a specific K, G, or prime ℓ, and the proof is admitted in the source.
The goal is OAI.KaplanskyCounterexample.finitelyPresented_counterexample. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected statement includes finite presentation and an element of odd prime order in the group. The weaker finitely generated formulation is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A matrix counterexample does not automatically provide scalar elements in a group algebra. The formal target requires genuine finitely supported scalar elements and verification of both products.
The field and group are existentially quantified, with the finite-field, characteristic, and finite-presentation structures carried explicitly. No claim that the field is exactly the two-element field is made. Odd-prime torsion is part of the conclusion.
The shared definitions are supplied by KaplanskyDirectFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Multiplicity measures the growth of infinitesimal neighborhoods in a local ring. The manuscript addresses Lech’s flat-local-map inequality; the available formal target isolates its complete-domain Frobenius-complex component. The source is OpenAI's September 2026 manuscript.
For a local domain of dimension , Hilbert–Samuel multiplicity is the limit of . A short complex has finite free terms in degrees through zero, finite-length homology, and nonzero zeroth homology. Its Frobenius scalar extensions define a normalized Euler-characteristic sequence.
The defined proposition DuttaDomainClaim holds, in universe u. That claim says: let D be a commutative Noetherian local domain (in universe u) that is complete in the adic topology of its maximal ideal, with prime characteristic p, and let F be a cochain complex of D-modules indexed by the integers that is a short complex. Short means every term F^i is free and finitely generated, F^i is zero whenever i < -dim D or i > 0, every homology module of F has finite length, and the homology of F in degree 0 is nonzero. Here dim is the Krull dimension (taken as 0 if it is the bottom value). Let F_n denote F after extending scalars along the n-fold iterate of the Frobenius map of D. The conclusion has three parts. First, every homology module of every F_n has finite length. Second, the sequence a_n = p^(-n dim D) * chi(F_n) converges as n tends to infinity, where chi(G) is the alternating sum, over i from 0 to dim D, of (-1)^i times the length of the homology of G in degree -i; this limit is the Dutta multiplicity of F. Third, the Hilbert-Samuel multiplicity of D, defined as the limit of (dim D)! times the length of D/m^N divided by N^(dim D) as N tends to infinity, is at most the Dutta multiplicity of F.
The goal is OAI.Lech.dutta_domain.
The goal formalizes the lower bound by Dutta multiplicity together with the convergence and finite-length statements needed to interpret it. This is a precise component of the paper’s multiplicity program. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Lengths of homology after Frobenius extension must be controlled before normalized Euler characteristics can be used. A definition by a chosen limit does not by itself establish convergence.
The ring is a complete Noetherian local domain in prime characteristic. The goal is DuttaDomainClaim, not the unrestricted flat local homomorphism inequality. Dimensions and lengths use the natural-number conversions in the supplied definitions, and convergence is an explicit conclusion.
The shared definitions are supplied by DuttaDomain. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The linear Fourier coefficients measure a Boolean function’s correlation with individual inputs. The source studies whether their sum can be controlled solely by the square root of the function’s real polynomial degree. The source is OpenAI's September 2026 manuscript.
A Boolean function here takes values in on a finite sign cube. Fourier coefficients use the uniform distribution. The Fourier degree is the largest support size of a nonzero coefficient; it is unrelated to degree over a field of characteristic two.
Two things about real Fourier analysis on Boolean cubes, where a Boolean input is read as a sign (false is +1, true is -1), averages are uniform, and degree is the ordinary real Fourier degree, meaning the largest size of a subset s with nonzero Fourier coefficient, the coefficient being the average of f(x) times the product of the signs of the coordinates in s. First, SignedViolations holds: for every real C>0 there is a positive integer n and a function f from {false,true}^n to the reals that takes only the values -1 and 1, is nonconstant, and satisfies C·√(deg f) < Σᵢ f̂({i}), the plain signed sum of its degree-one Fourier coefficients over single coordinates. Second, the set of ratios (Σᵢ |f̂({i})|)/√(deg f), taken over all positive n and all Boolean-valued f on n coordinates with positive Fourier degree, is not bounded above in the reals, so the supremum of these ratios is infinite.
The goal is OAI.SquareRootDegree.main.
Both signed violations and unbounded absolute ratios are retained. The result concerns failure of every constant multiple, which is stronger than exhibiting one violation of a proposed constant-one inequality. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
A large ambient dimension is not itself a violation: the denominator depends on degree. The function must remain Boolean and nonconstant while its linear coefficient sum outgrows that denominator.
Inputs are Fin n → Bool, with false interpreted as and true as . The first clause requires positive dimension and a nonconstant function. The second restricts to positive Fourier degree and uses ¬ BddAbove, avoiding a real-valued infinity convention.
The shared definitions are supplied by SquareRootDegree. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
The Heilbronn triangle problem asks how large the smallest triangle in an -point set can be. A positive improvement in the exponent would contradict bounds at every scale arbitrarily close to . The source is OpenAI's September 2026 manuscript.
Points lie in the closed unit square in the real plane. Triangle area is half the absolute determinant of the two displacement vectors, and the lower-bound condition quantifies over all triples of distinct points.
The Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).
The goal is OAI.Problem355.heilbronn_power_lower_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The formal goal gives an unbounded sequence of configurations with a fixed explicit power improvement. An attached companion target rules out an eventual almost- upper bound at half that exponent. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Avoiding collinear triples is insufficient: every nonzero triangle must also satisfy one uniform quantitative area bound. The exponent must stay positive independently of the size of the configuration.
The selected goal asserts a sequence tending to infinity, rather than the stronger all-sufficiently-large-sizes statement in the manuscript. The explicit exponent is heilbronnExponent, built from fixed binomial coefficients. Finite sets eliminate repeated points; real powers specify the area scale.
The shared definitions are supplied by HeilbronnTriangle. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Random triangle deletion constructs a partial triangle packing. Its terminal uncovered edges measure how efficiently this process covers pairs, and the source seeks the leading constant rather than only the growth exponent. The source is OpenAI's September 2026 manuscript.
Start from the complete graph on vertices. At each step choose a remaining triangle uniformly and remove its three edges. A triangle-free state stays fixed. The terminal leave is the edge count at the end.
For the random triangle-removal process, three limits hold as n tends to infinity. The process starts from the complete graph on n vertices, with graphs represented as sets of 2-element subsets of Fin n. At each step, if the current graph G contains triangles (3-subsets all of whose pairs are edges of G), one triangle is chosen uniformly at random and its three edges are deleted; if there is no triangle, the graph stays unchanged. Running this for C(n,2) steps gives the terminal law on graphs, and expectation and probability are taken with respect to it. Writing normalizedLeave(G) = |E(G)| / n^(3/2) and sharpConstant c = 1/(2√2), the theorem asserts: first, the expected value of (normalizedLeave(G) − c)² tends to 0; second, for every ε > 0, the probability that |normalizedLeave(G) − c| > ε tends to 0; and third, the expected number of edges of the terminal graph divided by n^(3/2) tends to c.
The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.
The three conclusions record mean-square concentration, concentration in probability, and the limiting normalized expectation. The exact leading constant is part of the target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Early evolution estimates need to remain informative near termination, where triangles become scarce. A high-probability estimate alone need not control the second moment required here.
Graphs are finite sets of pairs from Fin n, with transitions given by probability mass functions. Running for the initial edge count guarantees that the absorbing terminal law is reached. Expectations are finite sums and all limits are along natural tending to infinity.
The shared definitions are supplied by TriangleRemoval. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Finite matroid packing and covering principles connect disjoint spanning sets with independent covers. The source seeks a concrete obstruction to extending the unrestricted principle to infinite ground sets. The source is OpenAI's September 2026 manuscript.
A matroid records independent subsets and their closure. A packing/covering partition divides the common ground set into a part with disjoint spanning sets in restrictions and a part covered by independent sets in contractions. Self-duality means equality with the dual on the same labelled ground set.
The ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.
The goal is OAI.InfiniteMatroidCounterexample.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The goal simultaneously supplies a countable infinite example, failure of a full independent cover, and failure of every mixed partition. Additional attached statements treat partitional matroids, intersection, and the separate packing and covering assertions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Failure of a full independent cover does not by itself exclude a mixed partition. The matroids must satisfy the infinite independence axioms, including maximal extension, throughout the construction.
The ground type is the fixed product of integers with finite Boolean-function data. Mathlib matroids have ground set equal to the entire type in the goal. The two source definition groups have overlapping declarations and remain separate reference groups, with no aggregate import.
The shared definitions are supplied by InfiniteMatroid, InfiniteMatroidCorollaries. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.
An independent set contains no adjacent pair. Write for the number of vertices, for average degree, and for the largest independent-set size. A graph is clique-free of order when it contains no pairwise adjacent vertices.
For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.
The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.
The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.
The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.
The shared definitions are supplied by CliqueFreeLog. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.
A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.
Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.
The goal is OAI.Barnette.main.
A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.
The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.
The shared definitions are supplied by BarnetteHamiltonian. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
High probability under independent coordinate sampling need not give a family any closure under unions. Discrete convexity asks whether a bounded number of its members nevertheless cover most sets in the stronger sense of inexpensive containment certificates. The source is OpenAI's September 2026 manuscript.
On Bernoulli product space , each coordinate is present independently with probability . For a family , the exceptional family consists of sets contained in no union of members of . A family is -small when it has containment generators with total cost at most .
For every positive integer N, every density p with 0<p<1, and every family D of subsets of the ground set {0,...,N-1} (an arbitrary family, with no monotonicity assumption), if the product measure of D under independent Bernoulli(p) coordinates, namely the sum over s in D of p^|s|(1-p)^(N-|s|), is at least 1 - 1/2^75, then the family of exceptional sets is small. Here the exceptional family for k=2^75 consists of all subsets S of the ground set that are contained in no union of k members of D, where the k members are given as an arbitrary tuple of exactly k entries of D, repeats allowed and with no disjointness required. A family A is small at density p if there is a family G of generator sets that covers A, meaning every member of A contains some member of G, and whose cost, the sum over I in G of p^|I|, is at most 1/2.
The goal is OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity.
The conclusion supplies explicit containment witnesses at the original density. A small probability for the exceptional event alone would not provide such a cover. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
The family is arbitrary, so monotonicity cannot be used as an extra hypothesis. The same universal number of unions must work for all dimensions and all densities strictly between zero and one.
Lean uses finite families of finite subsets of Fin N, with and . A tuple has exactly entries; repetitions and overlaps are allowed. The cover cost counts each generator once. The separate two-union density-loss corollary is outside this goal.
The shared definitions are supplied by TalagrandDiscreteConvexity. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.
A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size costs . An ordinary cover and a fractional cover both have budget ; a fractional cover assigns weights in and supplies total weight at least one inside each member. The expectation thresholds and are suprema of feasible parameters in .
For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.
The goal is OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence.
The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.
The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.
The shared definitions are supplied by TalagrandExpectationThreshold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An oriented graph may have very uneven outdegrees, yet the second-neighborhood conjecture asks for one vertex whose new two-step reach is at least its immediate outdegree. The source manuscript presents the surrounding research claim.
An oriented graph is a loopless asymmetric relation r on a finite nonempty vertex type. First neighbors satisfy r(v,w). Second neighbors are vertices w distinct from v, not already first neighbors, but reached by some directed path v→u→w.
Prove that some vertex v satisfies
Every second-neighborhood vertex is counted once, irrespective of how many two-step paths reach it.
The selected formal target is OAI.SeymourSecondNeighborhood.exists_goodVertex.
The statement covers all finite oriented graphs, including disconnected graphs and graphs whose underlying undirected graph is not complete. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Counting length-two walks overcounts repeated endpoints and may include first neighbors. The conclusion concerns the set of vertices at directed distance exactly two.
The formal relation need not be supplied with decidability; the finite sets are formed classically. Looplessness and asymmetry are explicit hypotheses, and the vertex type is finite and nonempty. GoodVertex is exactly the finite-cardinality comparison.
adc7f1241b42. Goal source.Euclidean Ramsey theory asks which finite shapes must occur monochromatically in a sufficiently high dimension. The scale is fixed, so an algebraic criterion must capture exact distances rather than approximate similarity. The source manuscript presents the surrounding research claim.
A Ramsey configuration a=(aᵢ) has a monochromatic congruent copy under every finite coloring in some dimension depending on the number of colors. Let F be the rational field generated by all coordinates, B=F⊗ℚF, and pᵢ=(1,aᵢ) the augmented coordinate vectors. Multiplication m:B→F sends x⊗y to xy.
For an injective configuration of at least two points affinely spanning ℝᵈ with d≥1, prove
The criterion asks for a matrix P over B with (pᵢ⊗1)ᵀP(1⊗pᵢ)=0 for every i and m(P_{αβ})=δ_{αβ} on the coordinate-coordinate block.
The selected formal target is OAI.EuclideanRamsey.classification.
The criterion is necessary and sufficient for the stated configurations. Available companion targets describe spherical necessity, positive classes and concrete non-Ramsey circle configurations. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Applying m to the tensor identity loses information because multiplication need not be injective. Equality in the tensor ring, and arbitrary colorings without measurability, are essential.
The goal uses real Euclidean coordinates and the exact generated intermediate field over ℚ. Congruence preserves all pairwise distances at their original scale. All published companion references are retained as separate groups because they repeat Ramsey definitions. Milestones state their own hypotheses and do not identify every spherical set as Ramsey.
adc7f1241b42. Goal source.Drawing all edges between two vertex classes creates unavoidable intersections. The Zarankiewicz target asks for the exact best crossing count with both part sizes variable. The source manuscript presents the surrounding research claim.
The complete bipartite graph has vertex type Fin m⊕Fin n and one edge for every pair in Fin m×Fin n. Admissible plane drawings use simple continuous arcs, distinct vertices, finitely many proper double crossings and no triple crossings.
For every m,n>0, prove there is a drawing with exactly
crossing points, and every admissible drawing has at least Z(m,n) crossings.
The selected formal target is OAI.Zarankiewicz.mainTarget_proof.
The formal target includes both an attaining drawing and the universal lower bound. Small positive part sizes remain in scope. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The best known construction alone cannot establish optimality. The lower bound must allow arbitrary continuous edge arcs and repeated crossings of a pair of edges.
Proper intersections use local coordinate-axis charts. Counted objects are crossing points, not merely pairs of edges that meet. The formula is implemented by axisPairs(r)=(r/2)((r−1)/2) in natural arithmetic. Tangencies, overlaps and triple crossings are excluded by the drawing model.
adc7f1241b42. Goal source.The complete graph forces many crossings in any plane drawing. The mission seeks the exact ordinary crossing number rather than one drawing’s upper bound. The source manuscript presents the surrounding research claim.
An admissible drawing uses distinct vertex points and injective continuous edge paths whose interiors avoid vertices. Intersections are finitely many proper double crossings, with no triple crossing. Every crossing point is counted, including repeated meetings of a pair of edges.
For n≥3, prove
The selected formal target is OAI.Paper170.complete_graph_crossing_number.
The target fixes the exact minimum across the full continuous-drawing class. It does not restrict edges to straight segments or impose a special layout. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An explicit drawing establishes only an upper bound. The equality also requires a bound valid for all admissible topological drawings.
The graph uses ordered endpoint pairs with increasing indices. Proper crossings are defined through local open partial homeomorphisms taking the two traces to coordinate axes. The ordinary crossing number is the natural infimum of crossing counts; hill uses natural subtraction and division. The selected theorem starts at n=3.
adc7f1241b42. Goal source.