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?
A projection game (label cover) asks for labels on the two sides of a bipartite multigraph so that, on each edge, the right label is the image of the left label under a prescribed map. In a 2-to-1 game the left alphabet has labels, the right alphabet , and every edge map has exactly two preimages of each right label. Khot introduced the 2-to-1 and Unique Games conjectures in 2002 (STOC 2002) as hypotheses that yield tight hardness of approximation. The 2-to-1 Games Conjecture with perfect completeness asserts that, for every fixed , it is NP-hard to tell satisfiable 2-to-1 games from games in which every labeling satisfies at most a fraction of edges. Perfect completeness matters for problems whose YES instances must be exactly satisfiable, such as graph coloring: hardness with completeness does not imply it.
This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For an integer , a 2-to-1 instance has finite left and right vertex sets and a nonempty list of edge occurrences , where is given by an explicit table with for every . Parallel occurrences, possibly with different maps, are allowed and counted with multiplicity; there are no weights. A labeling assigns and and satisfies when . The value is the maximum, over labelings, of the fraction of satisfied occurrences. 3-SAT inputs are bit strings that decode to conjunctions of three-literal clauses (repetitions allowed); malformed inputs count as unsatisfiable.
For every fixed rational there are an integer and a deterministic polynomial-time reduction from 3-SAT to 2-to-1 instances with alphabets and such that
The running time is polynomial in the binary input length, with degree and constants depending only on .
The result itself. It removes the conditional hypothesis from perfect-completeness reductions. The preprint derives NP-hardness for maximum -colorable subgraph at soundness through Guruswami and Sinop's reduction (Corollary 1.2, p. 3), and recovers satisfiable Not-Two and three-query PCP hardness (Corollary 1.3, p. 4), the latter already known unconditionally by Håstad (SICOMP 2014). A companion preprint uses it for hardness of finding large independent sets in three-colorable graphs.
Formalizing it. No PCP-style hardness result of this strength has been machine-checked. A complete development needs a perfect-completeness PCP gap (Theorem 2.1, p. 5), projection-game parallel repetition (Theorem 2.2, p. 6), the Grassmann expansion theorem (Theorem 2.3, p. 7) and inverse shortcode estimates (Theorem 2.6, p. 9), on top of a polynomial-time Turing-machine framework. These components are shared with the Unique Games formalization and would be reusable.
Near-perfect completeness does not give perfect completeness: the reductions need not produce any finite satisfiable game. Amplifying a constant-soundness perfect-completeness game by parallel repetition destroys the 2-to-1 structure, since -fold repetition gives preimages per right label. The preprint therefore builds a new tree-structured construction (Section 3) whose joint-partition questions keep two-element fibers and satisfy exact identities, and the soundness analysis must decode labelings through a rank test whose tested rows depend on the decoded form itself (Sections 5–6), before projection-game repetition gives the contradiction (Section 7).
ProjectionTable q is a Vector (Fin q) (2*q) with exactly two preimages of every b : Fin q. Instance q lists edges as a List with a nonemptiness proof, so value = maxSatisfied / edges.length never divides by zero; maxSatisfied is a Finset.sup over all labelings.BinaryGapReduction δ fixes alphabet ≥ 2, a construct map, a Turing.TM2ComputableInPolyTime witness from raw input bits (identity encoding) to the explicit bit encoding gameBits, finite tape alphabets, completeness value = 1 on encodings of satisfiable formulas, and soundness value ≤ δ on all other inputs.value = 1 requires a labeling satisfying every edge.A directed feedback vertex set of a finite digraph is a set of vertices meeting every directed cycle, equivalently one whose removal leaves acyclic; is the minimum size of such a set. The problem arises wherever cyclic dependencies must be broken — deadlock resolution, circuit testing, scheduling — and a topological order of certifies a solution in polynomial time.
The best general approximation guarantee is , originating in Seymour's work on fractional packing of directed circuits (Combinatorica 1995) and made constructive by Even, Naor, Schieber and Sudan (Algorithmica 1998). On the hardness side, NP-hardness was known only for particular constants (via Vertex Cover), while ruling out every constant factor required the Unique Games Conjecture. Whether a constant-factor approximation exists under P ≠ NP alone was open.
This mission asks for a machine-checked proof that approximating DFVS within any fixed factor is NP-hard on unweighted digraphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A digraph is finite and loopless, given by a vertex count and a duplicate-free list of arcs with ; opposite arcs are allowed. A directed cycle is a cyclic sequence of distinct vertices with every successive arc present, including the closing one. is a feedback set if it meets every directed cycle, and is the least size of one.
A language is in NP if there are a polynomial and a deterministic polynomial-time verifier (a multi-stack Turing machine with finite alphabets) with iff some certificate with makes accept.
For every real and every language there is a deterministic polynomial-time map with such that
In Lean this is OAI.DirectedFeedback.main : DirectedFeedback.MainStatement. The preprint states Theorem 1.1 as a reduction from an NP-hard promise problem (the 2-to-1 game gap of Theorem 2.1, p. 5) to ; composing with that promise problem's NP-hardness gives the Lean form, which quantifies over all NP languages directly. A deterministic polynomial-time -approximation would then decide every NP language (proof of Theorem 1.1, p. 28).
The preprint also proves Corollary 8.3 (p. 28) for directed feedback arc set; it is not formalized on the platform.
The result itself. Theorem 1.1 shows that a constant-factor approximation for DFVS exists if and only if P = NP, removing the Unique Games hypothesis from the Guruswami–Manokaran–Raghavendra and Svensson results. It does not determine the true growth of the optimal factor between constants and .
Formalizing it. No machine-checked inapproximability result of this kind is known to exist. A complete development needs the 2-to-1 Games Theorem with imperfect completeness (Theorem 2.1, p. 5, external input), Friedgut's junta theorem in a dyadic fixed-bias form (Theorem 2.2 and Corollary 2.3, p. 6), finite Ramsey theory and von Neumann's minimax theorem, and the preprint's rank-graph construction (Definition 3.1, p. 8; Proposition 3.7, p. 12), pivotality budget (Definition 6.1, p. 20) and weighted soundness (Proposition 7.4, p. 25). An NP and Karp-reduction library on TM2 machines (including Cook–Levin) would be reusable across the whole family of hardness missions.
The central difficulty (Introduction, pp. 3–4) is extracting a game labeling from an arbitrary acyclic remainder: a topological order exists, but it can interleave the many vertices representing one local test arbitrarily. Comparisons in that order must first be made consistent and then read as Boolean functions; Friedgut-type junta bounds must hold at many biases simultaneously for the same random function, so a separate influence bound at each scale does not suffice. The coordinate lists must also be fixed before the tested game edge is drawn, or they do not define a game labeling. Gadget reductions from Vertex Cover cannot go beyond the Vertex Cover constants.
DirectedFeedback.Digraph: n : ℕ, a Nodup list of arcs in Fin n × Fin n, loopless; cycles are injective maps Fin (r+1) → Fin n with all successive arcs (including the wrap-around) present, so 2-cycles count and 1-cycles cannot occur. dfvs is the least cardinality of a feedback Finset.NPVerifier: a polynomial certificate bound and a polynomial-time TM2 verifier with finite alphabets on the unary-framed pair encoding pairBits; no SAT-specific definition is used.GapReduction A L is a polynomial-time TM2 machine (finite alphabets, raw-bit input) producing a GapInstance (digraph plus k > 0), encoded explicitly in unary-framed form by GapInstance.bits; completeness and soundness are as displayed, with soundness compared in ℝ.TM2 verifiers plus the 2-to-1 Games reduction.k > 0 and the strict inequality rule out a trivial reading (e.g. empty graphs with k = 0).Welcome contributions: Friedgut's junta theorem, finite Ramsey and minimax in usable forms, the 2-to-1 Games Theorem, and Cook–Levin for Turing.TM2ComputableInPolyTime.
Min-UnCut asks, for a finite simple graph , for the minimum number of edges whose deletion makes bipartite. Equivalently, for a bipartition let count the edges with both endpoints on the same side, and set . The quantity measures distance from bipartiteness. Although it equals minus the maximum cut, a good multiplicative approximation for Max-Cut gives nothing multiplicative for Min-UnCut on nearly bipartite graphs, which is exactly the regime of interest.
The best known algorithm (Agarwal, Charikar, Makarychev, Makarychev, STOC 2005) achieves an factor. Before the source preprint, NP-hardness was known only for specific constant factors below about , and hardness for every constant factor was known only under the Unique Games Conjecture.
This mission asks for a machine-checked proof that Min-UnCut has no polynomial-time approximation within any constant factor unless P = NP, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A graph is finite, simple, undirected and unweighted, given by a vertex count and a symmetric loopless Boolean adjacency table. A cut is a map ; the parts may be empty or unbalanced. counts unordered edges with , and is its minimum over all cuts.
3SAT formulas are conjunctions of three-slot clauses over natural-number variable names (repeated variables allowed), given to the reduction by a canonical prefix-free binary encoding.
For every fixed integer there is a deterministic polynomial-time reduction to an explicit simple graph and a binary integer with
with graph size and running time polynomial in the bit length of for each fixed . Choosing shows that a deterministic polynomial-time -approximation for any real would imply P = NP. The positive threshold is what separates this from bipartiteness testing. In Lean this is OAI.MinUncut.main : Nonempty MinUncut.Reduction.
The preprint also derives Corollary 1.2 (p. 3): minimum 2CNF clause deletion is NP-hard to approximate within every fixed factor . It is not formalized on the platform.
The result itself. Theorem 1.1 settles the constant-factor approximability of Min-UnCut in the hardness direction without the Unique Games Conjecture, and by an exact cost-preserving transformation the same holds for Min 2CNF Deletion. Together with the algorithm, it places these problems strictly between constant-factor approximable and inapproximable within logarithmic factors (the remaining gap concerns super-constant factors).
Formalizing it. No machine-checked proof of super-constant-type inapproximability for any natural graph problem is known to exist. A complete development needs Håstad's parity gap (Theorem 2.2, p. 6) and uniform parallel repetition (Theorem 2.3, p. 7), used as external inputs, plus the preprint's inner decoding theorem (Theorem 3.2, p. 9), the composition gap for bit comparisons (Proposition 6.1, p. 27) and the finite constructions (Lemmas 7.1 and 7.2, pp. 31 and 34). PCP and parallel-repetition infrastructure would be reusable across many hardness missions.
A natural route is to compose a long-code test with a projection game, as in Håstad's work. The obstacle is extracting a label from an arbitrary folded bit proof with a probability and coefficient size independent of the label alphabet: the alphabet grows as the outer soundness is driven down, and every inner constant must be fixed before it (Introduction, pp. 3–4). In addition, the decoder's choices depend on shared background affine functions, so the outer game's soundness must survive such shared hints. Gadget-based approaches yield only isolated constants (up to about ); unbounded constants previously required the Unique Games hypothesis.
MinUncut.Output packages the graph (vertex count, symmetric loopless Bool adjacency) with a threshold threshold ≥ 1; uncut counts pairs u < v that are adjacent and on the same side, and opt is the minimum over all Fin N → Bool cuts (nonempty, so always defined).MinUncut.Reduction is a single TM2 machine taking the pair (encoded by inputBits) with finite tape alphabets, a polynomial time K bounding the running time in the formula's bit length, and a polynomial size K bounding vertices plus output length; yes/no hold for every K ≥ 2.formulaBits φ, the canonical encoding including variable names.Welcome contributions: Fourier and Gaussian analysis on -affine spaces, the long code with folding, parallel repetition for projection games, and Turing-machine complexity infrastructure.
A vertex cover of a graph is a set of vertices meeting every edge; denotes the minimum size of one. Computing exactly is NP-hard, but a two-line algorithm — take both endpoints of a maximal matching — always returns a cover of size at most . Whether any polynomial-time algorithm achieves a fixed factor is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below and, after the 2-to-2 Games Theorem, below ; factor-two hardness was known only under Khot's Unique Games Conjecture.
This mission asks for a machine-checked proof that every fixed approximation factor below two is NP-hard, as claimed in an OpenAI preprint dated September 23, 2026 (source, Corollary 1.2, p. 1). The preprint's direct reduction starts from ordinary perfect-completeness Label Cover. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count and a duplicate-free list of edges with . A set of vertices is a cover if every edge has an endpoint in , and is the least size of a cover. An -approximation algorithm is a deterministic polynomial-time machine that, on every graph, outputs a duplicate-free list of vertices that covers all edges and has length at most .
3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses; malformed strings are NO instances. A 3SAT decider is a deterministic polynomial-time machine answering membership correctly on every input.
For every integer there is a deterministic polynomial-time reduction from 3SAT to explicit simple graphs with
The ratio of the thresholds is . In Lean: OAI.VertexCover.explicit_cover_gap.
For every real with , an -approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:
In Lean: OAI.VertexCover.every_fixed_factor_below_two. The preprint derives it from Theorem 1.1 in its final section (pp. 23–24) by choosing from and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies as the approximation threshold unless P = NP.
The result itself. The statement removes the Unique Games hypothesis from the Khot–Regev theorem and closes the gap between the elementary factor- algorithm and hardness. The density gap of Theorem 1.1 is also a statement about independent sets: YES graphs have independent sets of density nearly , NO graphs have none of density above .
Formalizing it. No machine-checked proof of any super-constant Vertex Cover hardness bound is known to exist. A complete development requires the perfect-completeness Label Cover theorem (Theorem 2.1, p. 4; PCP theorem plus parallel repetition, used as an external input), the explicit graph construction and its polynomial-time implementation (Proposition 3.3, p. 7), and the preprint's analytic soundness argument. The Label Cover input and a library for polynomial-time gap reductions on TM2 machines are reusable for many other hardness missions.
Soundness requires extracting short lists of candidate labels from an arbitrary large independent set, where each list may depend only on its own position's query. If a list also sees the opposite endpoint of a constraint or its occurrence index, the pair-decoding argument against Label Cover soundness breaks down (Introduction, pp. 3–4). Classical approaches either need the stronger Unique Games source promise (Khot–Regev) or only reach densities near (the 2-to-2 route), which gives factor rather than . Averaging to impose the information restriction can erase all variance; the analytic core is retaining it without any dependence on the label alphabet sizes.
VertexCover.ExplicitGraph: n : ℕ and a Nodup list of pairs in Fin n × Fin n with e.1 < e.2; coverNumber is the least cardinality of a covering Finset (always defined since univ covers).ExplicitGraph.bits (vertex count, all vertex names, edge count, edge endpoints, each with prefix-free binary framing); an approximation's output list is encoded by natListBits.Approximation α bundles a polynomial-time TM2 program on graph encodings with finite tape alphabets, whose output is duplicate-free, in range, covers every edge and has length at most α * coverNumber. ThreeSATDecision is a polynomial-time TM2 decider correct on every input.Approximation α must be correct on every graph.ℝ with strict inequalities as in the source.Welcome contributions: Label Cover hardness (PCP theorem + parallel repetition), Efron–Stein decompositions and variance inequalities on product spaces, and general complexity-theoretic infrastructure for Turing.TM2ComputableInPolyTime.
Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching
(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above , and optimality of was known only under Khot's Unique Games Conjecture.
This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A simple unweighted graph on vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map from the vertices to ; its size is the number of unordered edges with , and is the largest cut size. An algorithm is an -approximation if it always returns a cut of size at least .
3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for consists of rationals and with , and a deterministic polynomial-time map outputting a graph together with a positive integer scale such that
Given such a reduction, an -approximation algorithm would decide 3SAT by comparing its output with .
For every real with , a gap reduction for from 3SAT to simple unweighted Max-Cut exists:
In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational , and , it is NP-hard to distinguish from on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.
The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.
Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.
The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).
OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.alphaGW is defined as the sInf of over ; this set is nonempty and bounded below, so the infimum is the true constant.Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.
A Unique Game is a system of constraints between pairs of variables, each constraint saying that the label of one endpoint is a fixed permutation of the label of the other. Deciding whether all constraints can be satisfied is easy (propagate labels along a spanning tree), so the interesting question is approximate: given an instance in which almost all constraints can be satisfied, can a polynomial-time algorithm find a labeling that satisfies even a small fraction?
Khot's Unique Games Conjecture (UGC, 2002) asserts that it cannot, unless P = NP. The conjecture matters because many optimal approximation thresholds have been proved conditionally on it: the Goemans–Williamson ratio for Max-Cut (KKMO 2007), the factor for Vertex Cover (Khot–Regev 2008), the basic-SDP threshold for every constraint satisfaction problem (Raghavendra 2008), and hardness for ordering, multicut/sparsest-cut and correlation-clustering problems. An unconditional proof would turn all of these into NP-hardness results.
This mission asks for a machine-checked proof of the Unique Games Theorem as stated in an OpenAI preprint dated September 23, 2026 (source), which claims a positive resolution of the conjecture. The preprint has not been peer reviewed, and its claim has not been independently verified; on the platform the Lean goal below is open.
Fix a finite alphabet . An instance has a finite vertex set and a nonempty list of oriented constraints with a permutation of ; repeated list entries count with multiplicity, and no weights are allowed. A labeling assigns a label to every vertex and satisfies when . The value of is the fraction of satisfied constraints and is the maximum over labelings.
An instance is simple bipartite if its vertices split into two sides, every constraint goes from the first side to the second, and no two list entries join the same ordered pair. It is a translation instance over if every constraint has the form .
3SAT inputs are bit strings decoding to a conjunction of clauses with exactly three literal slots (repeated variables and literals allowed); the input is a YES instance when it decodes to a satisfiable formula.
For every there exist and a deterministic polynomial-time map to simple bipartite translation instances over such that
The alphabet, the program and the running-time polynomial depend only on ; the two errors are chosen independently, before the alphabet. In Lean this is OAI.UniqueGamesTheorem.theorem11, which asserts that the structure BinaryGapReduction ε δ is inhabited.
The result itself. The conjecture is the hypothesis behind a large body of tight approximation thresholds; the preprint's Section 8 (pp. 39–43) records how Theorem 1.1 feeds the earlier reductions for Max-Cut, Vertex Cover, Raghavendra's CSP theorem, ordering CSPs, multicut/sparsest cut and correlation clustering. Those reductions and thresholds are due to their original authors. The statement also fixes the conjecture's quantifier order (errors first, then alphabet), which is exactly what the known algorithms above do not contradict.
Formalizing it. No machine-checked proof of the UGC, or of the 2-to-2 theorem it builds on, is known to exist. A complete development would have to formalize Håstad's parity gap, classical parallel repetition for projection games, the Khot–Minzer–Safra Grassmann/shortcode inverse theorem (used as an external input via Theorem 5.1, p. 22 of the preprint), and the preprint's new latent-alphabet gadget and matrix test. Each of these is reusable well beyond this mission.
The central obstacle, identified in the preprint's introduction (pp. 2–4), is completeness: in a unique constraint every label permits exactly one reply, so the natural codeword tests lose a constant fraction of constraints even on honest proofs. For example, on the rank-one matrix shortcode the evaluation is preserved by a random rank-one update only with probability about . The 2-to-2 theorem gives soundness but only near- completeness, and pushing completeness to while keeping soundness independent of the alphabet is a separate problem that the earlier programme left open.
Foundations.Target.Instance q over alphabet Fin q, with constraints given by explicit forward/inverse permutation tables and a nonemptiness proof; the value is countSatisfied / constraints.length in ℝ, so division by zero cannot occur.Turing.TM2ComputableInPolyTime program from raw input bits (identity encoding, so runtime is measured in the raw input length including sparse variable names) to the bit encoding gameBits; its tape alphabets must be finite.coordinates : Fin alphabet ≃ (Fin s → ZMod 2) fixes the structure, and translations requires every constraint to be a translation in these coordinates; simpleBipartite gives the orientation and the no-parallel-edge condition on list positions.BinaryLanguage.language: inputs that decode (canonically) to a satisfiable three-slot formula. Malformed inputs are NO instances and must be mapped to low-value games.Welcome contributions: a reusable Lean library for PCP-style gap reductions on TM2 machines, Fourier analysis over , parallel repetition for projection games, and the Grassmann expansion theorem.
Edit distance , the least number of single-symbol insertions, deletions and substitutions turning into , is the standard distance on strings. Embedding strings into with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for , so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.
This preprint gives two independent constructions of binary word sets whose least distortion is , two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.
For a finite alphabet with and an integer , let be the words of length at most , including the empty word. For an injective ,
The longest common subsequence and the deficit for words of length are used in the coding results. A binary substitution replaces each letter by a codeword.
In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most , and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.
finiteCircle_fullMainThe conjunction of the paper's main statements, with common absolute constants:
and the same bounds for .
The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of is ; this improves the previous lower bound to . The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.
Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.
List α with Fintype α; the domain is a subtype by length; the empty word is included.distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into ; exponentScale d = sqrt(log d · log log d) with natural logarithms.MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length .UniformUpper asks for a map into Fin M → ℝ with the norm written as a finite sum.The goal is not vacuous: a set with one element would have least distortion , so witnesses must be nontrivial, and both bounds are required uniformly.
Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.
Edit distance is the least number of single-symbol insertions, deletions and substitutions transforming a string into . It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into so that distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.
This preprint determines the exponential scale of the optimal distortion: for strings of length at most , it is , uniformly over finite alphabets.
For a finite alphabet and , let be the set of strings of length at most , including the empty string. Edit scripts may pass through strings of any length. Let be the space of absolutely summable real sequences. Define
the infimum over injective maps with no restriction on dimension or computability.
In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).
There are absolute and such that for every and every finite alphabet with ,
The lower bound is witnessed by a finite set of binary strings of one common length at most , and the same two bounds hold for .
The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between (Krauthgamer–Rabani) and . It rules out any embedding of edit distance with distortion , which limits -based approaches to approximate edit-distance search.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.
Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the exponent; reaching it requires a construction whose combinatorial separation and an displacement inequality match at that scale.
List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to .edit is an sInf over script lengths, which is attained since scripts always exist.distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into .BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length whose least distortion is at least exponentScale c d; a singleton has least distortion , so the witness must be nontrivial.The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.
Needed infrastructure: cut decompositions of finite metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.
A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some . Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.
The Hilbert case () remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.
A metric space is doubling with constant at most if for every and , the ball of radius about is covered by at most balls of radius with centers in . A map is a bi-Lipschitz embedding with distortion at most if some scale satisfies
Real is the Hilbert space of square-summable real sequences indexed by ; subsets carry the induced distance.
There is a universal such that every infinite-dimensional real Banach space contains a compact set with doubling constant at most that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.
The set is fixed once, independently of and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.
The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every , (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.
Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The constructions rely on uniform convexity estimates of that degenerate at , and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every and every simultaneously.
RealL2 := lp (fun _ : ℕ => ℝ) 2; is a Set RealL2 with the subspace metric.DoublingAtMost S bound: for each and there is a Finset of at most bound centers in such that every with satisfies for some center (open balls; centers in ).AdmitsBiLipschitzEmbedding S k: there are EuclideanSpace ℝ (Fin k), and with the two-sided bound above.CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant chosen before .A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.
Given vectors in the Euclidean unit ball of that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs , chosen once and for all, such that every signed prefix is , independently of . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.
Work in Euclidean space with norm , and let satisfy ; repetitions and zero vectors are allowed. A prefix sum is for (the empty sum is ). For a zero-sum family, the Steinitz quantity
is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant is its supremum over all such families.
There is an absolute constant such that for all and all with :
The constant is not fixed. The simplex example in the source shows , so the order is optimal. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: . Theorem 1.1 settles the prefix-discrepancy question of Bansal et al., removing the term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.
Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.
Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a factor, because the probability that a random walk stays in a ball of radius for steps decays with . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.
EuclideanSpace ℝ (Fin d), indexed by Fin N, with and .SignedPrefixBound C asks for signs (as reals) with every signed prefix at most . OrderingPrefixBound C asks, for zero-sum families, for a permutation with every reordered prefix at most . The goal is ; the same constant serves both, as stated in the source.Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is , attained by three planar sectors of angle (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.
This mission asks for a formal proof of the propeller bound in every dimension, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the standard Gaussian probability measure on , with density . For a measurable set , its centroid is the unnormalized vector
A measurable partition of consists of measurable sets such that almost every point (for ) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is . The propeller is the partition of , , into the three sets , where are the planar sectors of opening bounded by the rays at angles and , with any further cells empty.
For all positive integers and every measurable partition of ,
and for , the propeller is a measurable partition attaining equality.
The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant fixes the loss factor of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).
Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.
The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose nonzero centroids span an -dimensional space, so the three-dimensional theorem disposes of active cells. The remaining cases cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.
Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.propeller d k (cells empty) is a partition with value exactly . The sectors are written with closed inequalities, so they overlap only on null rays.The Johnson–Lindenstrauss lemma (1984) says that any points of a Hilbert space can be placed in -dimensional Euclidean space with distortion at most any prescribed . This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces with the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates are needed so that every -point subset of embeds into with distortion at most ?
The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed , , and the dimension is .
All spaces are real. Fix , an integer and . Let be the least integer such that for every measure space and every distinct points there are and a scale with
The map is arbitrary, not required to be linear. Put
For fixed , :
Since , the upper bound is . The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.
For the best previous finite-set bounds were polynomial in (linear for ), and for logarithmic dimension is impossible. The theorem places at for every fixed , in contrast with exact embeddings, where the dimension is of order . Thus the exponent jumps from at to for every . The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.
The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.
Linear maps cannot work: fixed-distortion linear maps on some configurations need dimension proportional to when . Subspace discretization theorems apply to the span of the points, which has dimension up to , so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in . One needs a single random scalar map whose increments have nearly equal normalized -th moments simultaneously for all pairs, with relative (not additive) error control.
coordinateDistance p y z is on Fin d → ℝ.GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the distance and a scale .dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.Tendsto statement along n : ℕ for each .A complete development needs spaces, -stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.
The Brunn–Minkowski inequality is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is , by a -mean of support functions. As the -mean becomes the geometric mean , giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.
A convex body is a compact convex set with nonempty interior; it is origin-symmetric if , in which case is an interior point. Its support function is
which is strictly positive for origin-symmetric bodies. For a positive function on the sphere, the Wulff body is
The logarithmic combination of with parameter is . In general is not itself a support function, which is why the Wulff body is needed. denotes Lebesgue measure.
For , origin-symmetric convex bodies and ,
The goal statement is published on the platform with status Open.
The result itself. By the arithmetic–geometric mean inequality, , so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric Brunn–Minkowski inequality for every (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: is log-concave for every even log-concave measure and origin-symmetric convex body (Corollary 8.1 of the source).
Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.
The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.
EuclideanSpace ℝ (Fin n) with ; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.sSup of over , nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).volume in ℝ≥0∞, with ℝ≥0∞-valued powers and . At the inequality reduces to (resp. ), so the edge cases are consistent.How densely can equal disks be packed in the plane? The hexagonal arrangement, with centers on the triangular lattice, covers a fraction of the plane, and Thue's theorem says no packing does better. In 2003 Cohn and Elkies introduced a linear programming bound for sphere packing: a single auxiliary function whose values are nonpositive outside a ball and whose Fourier transform is nonnegative certifies an upper bound on packing density. Viazovska (dimension 8) and Cohn, Kumar, Miller, Radchenko and Viazovska (dimension 24) found auxiliary functions for which the bound is sharp, solving sphere packing in those dimensions. Cohn and Elkies conjectured that a sharp function exists also in dimension 2 (Conjecture 7.3 of their paper). The planar packing problem itself is classical; the question here is whether the Fourier method certifies it exactly.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims an explicit sharp planar certificate.
Scale disks to radius , so a packing is a set of centers with for distinct centers. The Fourier transform is
A Schwartz function is smooth with all derivatives decaying faster than any inverse power of . A function is radial if depends only on ; for real radial integrable , is real and radial. The Cohn–Elkies theorem says that if is admissible, for and , then every packing of radius- disks has density at most .
There is a real radial Schwartz function with
Lean: OAI.sharp_fourier_certificate, open on the platform.
With the Cohn–Elkies bound equals , the hexagonal density, so the theorem answers the two-dimensional case of Cohn–Elkies Conjecture 7.3 affirmatively and gives a Fourier-analytic proof of Thue's theorem for arbitrary (not only periodic) packings. Its zero structure also recovers uniqueness of the triangular lattice among periodic optimal packings. The certificate does not satisfy the additional zero-set requirement of Cohn–Elkies Conjecture 8.1, which remains a separate question. The construction methods feed into the companion work on universal optimality of the triangular lattice in the same family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. By contrast, Viazovska's dimension-8 theorem has been the subject of formalization efforts, so a planar certificate would be a natural low-dimensional companion.
In dimensions 8 and 24 the magic functions come from modular forms, whose symmetries control a function and its Fourier transform at once. No such modular construction is known to produce the planar certificate, and Sardari's nonuniqueness theorem shows that prescribing values and derivatives on the lattice shells does not pin a function down. Numerical Laguerre–Gaussian searches (Cohn–Elkies) approach the bound but do not attain it. The hard part is an exact construction together with rigorous sign control of both (for ) and (everywhere), including between interpolation nodes and in the tails.
EuclideanSpace ℝ (Fin 2); the function is a SchwartzMap Plane ℝ.SharpPlanar.fourier f ξ is the Bochner integral of ; for a Schwartz function it is the usual transform.SharpCertificate f: Radial f, fourier f 0 = 1, f 0 = 2 / √3, for every ξ the transform has zero imaginary part and nonnegative real part, and f x ≤ 0 when 1 ≤ ‖x‖.A complete development needs Fourier transforms of radial functions in the plane (Hankel transforms, Gaussian pairings) and rigorous interval or Bernstein-polynomial sign certification. Formalizing the Cohn–Elkies bound itself (certificate implies density bound) would be a valuable reusable companion. Contributions formalizing Proposition 2.2, Proposition 3.4 or Proposition 4.3 are welcome.
Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.
The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.
Let and , the triangular lattice of covolume one. Let be the closed disk of radius about the origin. A set is locally finite if each is finite, and has centered disk density one if , where .
A smooth is completely monotone if for all , . The lower energy per particle is
summing over ordered pairs. The Fourier transform is and is the dual lattice.
For every there is a real radial Schwartz with
given for by the paper's explicit atomic interpolation construction.
For every smooth nonnegative completely monotone and every locally finite of centered disk density one,
Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.
Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as with ) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).
Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.
EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), and iteratedDeriv r g t for .energy g C is the liminf over of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.C and the equality latticeEnergy g = energy g A.realFourier is Mathlib's 𝓕 (kernel ) applied to the complexified function; the clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.
A finite metric embeds into exactly when it is a nonnegative combination of cut metrics . This makes distortion the right measure for the flow–cut gap: given edge capacities and pairwise demands, the ratio between the sparsest cut value and the maximum concurrent flow . Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) developed this connection, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured that every proper minor-closed family embeds into with uniformly bounded distortion (the GNRS conjecture). Graphs of bounded treewidth form one of its basic cases.
Let be a finite connected graph with edge lengths . The shortest-path metric is the least total length of a path from to .
A tree decomposition of is a finite tree with bags () such that the bags cover , each edge has both endpoints in some bag, and for each vertex the nodes whose bag contains induce a connected subtree. In this mission, as in the source, bounds the bag cardinality , so the treewidth bound is .
A map has distortion at most if .
For every integer there is a constant such that for every nonempty finite connected graph with a tree decomposition of bag size at most and every , there are and with
is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives for every multicommodity instance on graphs of treewidth less than . By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion . With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.
Formalizing it. The proof constructs cut measures directly on a tree decomposition and combines them with padded random partitions from the literature. A formal proof would certify that the constants depend only on , the point at which earlier approaches lost uniformity.
The successful pathwidth approach embeds the graph stochastically into dominating trees, but that route cannot work here: some series-parallel metrics require expected tree distortion (GNRS 2004, Theorem 5.6). Local-consistency approaches assume that small vertex sets admit compatible isometric cut representations, which a general bounded-treewidth metric need not provide. Multiscale constructions from padded partitions give good separation at each scale, but summing their contributions loses a factor growing with the number of scales. The construction must handle arbitrary branching of the decomposition tree and arbitrary edge-length ratios without such accumulation.
V is any nonempty Fintype with decidable equality; G : SimpleGraph V is connected.HasTreeDecomposition G k: a tree T on Fin n, bags Fin n → Finset V covering all vertices and all edges, with the bags containing each vertex inducing a connected subgraph of T, and all bags of cardinality at most k.ℓ : G.edgeSet → ℝ, strictly positive. shortestPathDistance is the sInf of lengths of paths (IsPath) from to ; this set is finite and nonempty for a connected finite graph, so the infimum is the true distance.PiLp 1 (Fin m → ℝ) with chosen per graph; this is the source's remark (p. 2) that the target can be taken to be finite-dimensional , and it is at least as strong as an target.C depends only on k and is quantified before the graph.A finite metric space embeds into exactly when its metric is a nonnegative combination of cut metrics . For this reason the least distortion with which a graph metric embeds into governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into with uniformly bounded distortion. The planar case has been the central open instance.
Let be a finite connected simple graph on vertex set with symmetric edge lengths on edges. The graph metric is the infimum of over walks from to . is planar if it has a drawing in : distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.
A map into the real space of some measure space has distortion at most if for all .
There is a constant such that for every , every connected planar graph on vertices and every symmetric positive edge-length function , there are a measure space and with
The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.
Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.
Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.
Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so ). Singletons are allowed.IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into ).The projection body of a convex body is the convex body whose support function in a unit direction is the -dimensional volume of the shadow of on . Petty showed that is affinely covariant, so the normalized volume
is invariant under invertible affine maps, and its extremal values are natural affine isoperimetric questions. Petty's conjecture concerns the minimum (ellipsoids). For the maximum, Brannen conjectured in 1996 that simplices maximize among all convex bodies (Mathematika 1996); the simplex value is .
This mission asks for a formal proof of an explicit counterexample in dimension , 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 convex body in is compact and convex with nonempty interior, and is -dimensional volume. For the brightness is , and
Let be the standard simplex and
The benchmark constant is , which equals of every -simplex (Proposition 5, p. 4).
It is not true that for every convex body .
is a convex body and
The result itself. Brannen's conjecture fails: in dimension the simplex is not the maximizer of normalized projection-body volume. The mechanism is the product identity for polytopes (Proposition 3, p. 3), which shows that is a lower bound for any universal upper constant in dimension ; iterating it gives an exponential excess for all large (Corollary 6, p. 6). The counterexample in dimensions was obtained independently by Feng, Hu, Liu and Xu; the contribution here is an explicit product witness with an exact rational value. The optimal upper constant and its maximizers remain separate questions.
Formalizing it. Every ingredient is elementary: the facet formula for projection bodies of polytopes (Cauchy's formula, Lemma 2, p. 2), the facet structure of a Cartesian product, affine covariance (Lemma 4, p. 3), and a fiber computation of . A formal proof would supply Mathlib with projection bodies of polytopes and Cauchy's projection formula, both reusable. The final comparison is an exact rational identity.
There is no shortcut through general inequalities: the statement is a strict comparison of two explicit volumes in dimension , so both and must be computed exactly. Computing of a product directly from shadow volumes is unwieldy; the efficient route goes through facet area-normal vectors, which requires proving that, up to a null set, each point of a shadow lies over exactly two facet interiors, and that the facets of are exactly and . The simplex value needs the volume of a cube plus a segment.
EuclideanSpace ℝ (Fin 20). In the goal, projectionVolume is the induced Lebesgue measure on the submodule of the orthogonal projection of ; brightness u = ‖u‖ * projectionVolume, so the support-function inequality is imposed for all (the homogeneous extension).productWitness is the set of whose first and last ten coordinates both lie in standardSimplex 10; the goal includes that it is compact, convex, with nonempty interior.simplexConstant 20 is the explicit number , not ; the goal states the exact ratio, its reduced fraction, the strict inequality, and .euclideanHausdorffMeasure (d-1) of the image under the orthogonal projection, and compares with ratio (simplex 20), so it implicitly needs Proposition 5.toReal; all bodies involved are bounded, so no infinite value is hidden.The projection body of a convex body packages the areas of all shadows of into a single convex body: its support function in direction is the -dimensional volume of the orthogonal projection of onto . The normalized volume is invariant under translations and invertible linear maps, so asking for its extremizers is an affine isoperimetric problem. Petty's projection-volume conjecture (Petty, 1971) predicts that this ratio is minimized exactly by ellipsoids. It is related to, but distinct from, Petty's projection inequality for the polar body , which is a classical theorem; inequalities in this family underlie affine Sobolev inequalities and isoperimetric inequalities in normed spaces.
This mission asks for a formal proof of the conjecture in every dimension , 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 convex body is a compact convex set with nonempty interior, and denotes -dimensional Lebesgue volume. For a unit vector , let be the orthogonal projection of onto the hyperplane and the Lebesgue measure on that hyperplane. The projection body is
the convex body with support function . Write for the volume of the Euclidean unit ball . An ellipsoid is a set with and an invertible linear map. Since , the ball has ratio .
For every integer and every convex body ,
with equality if and only if is an ellipsoid.
The result itself. Together with the separately proved three-dimensional case, it settles Petty's conjecture for all (in dimension the ratio is constant up to the standard identification). The preprint derives from it the Lutwak–Petty lower-degree inequalities, a mixed determinant-gradient inequality strengthening the Sobolev–Zhang affine inequality, and the sharp Holmes–Thompson isoperimetric inequality in normed spaces (Corollaries 7.1–7.3, pp. 27–29). Those corollaries for rely on the external three-dimensional theorem.
Formalizing it. The proof uses the first variation of volume, spherical harmonics with explicit cosine and Funk transform multipliers, a strict harmonic estimate for arbitrary norms, a variational representation of support functionals, and Brouwer's fixed-point theorem. Mathlib has Brouwer-type results only in limited forms and has no spherical-harmonic decomposition of ; these would be reusable. No machine-checked proof of any case of the conjecture is known.
Previous results are local: they require the body, after a linear change of variables, to be close to the ball, because the harmonic analysis of the projection operator only controls perturbations of the ball. A global argument must handle arbitrary bodies without symmetry or regularity. In the preprint (pp. 2–3) the degree-two spherical harmonic component is not a zero mode of the relevant sign-test operator and has to be removed by choosing affine coordinates; this needs a continuous family of variational minimizers extended to singular matrices and a fixed-point argument (Proposition 5.5, p. 23). Harmonics of degree at least four are controlled by a strict norm estimate valid for every norm (Theorem 4.1, p. 12). The equality case must come out of the same estimates.
Space n is EuclideanSpace ℝ (Fin n); IsConvexBody K is compact, convex, nonempty interior; .shadowVolume K u is the measure, in the induced Euclidean volume on the submodule , of the image of under orthogonalProjectionOnto. projectionBody K is the intersection of half-spaces over unit vectors, which has support function shadowVolume K because that function is itself a support function.projectionRatio K = volume.real (projectionBody K) / volume.real K ^ (n - 1); for a convex body both volumes are finite and the denominator is positive.pettyConstant n = kappa (n-1) ^ n * kappa n ^ (2 - n) with an integer exponent, the volume of the closed unit ball.IsEllipsoid K: for a linear equivalence .iff equality characterization; neither part is vacuous for .Place a convex body in the position coordinates and its polar in the momentum coordinates of the standard symplectic space . The resulting Lagrangian product links two problems. Its volume is the Mahler volume product , and its symplectic capacities measure how large a round ball can be squeezed into it by a symplectic map. Since symplectic maps preserve volume, a ball of capacity inside forces . Artstein-Avidan, Karasev and Ostrover showed that the Hofer–Zehnder capacity of equals for every origin-symmetric and connected Viterbo's volume–capacity conjecture to Mahler's conjecture (Duke 2014). Whether actual balls of capacity close to fit, i.e. whether the Gromov width also equals , was open.
This mission asks for a formal proof that it does, as claimed in an OpenAI preprint dated September 22, 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.
An origin-symmetric convex body is compact, convex, has nonempty interior, and satisfies . Its polar is . On put , and let
A symplectic embedding of an open set into is a map on that is a topological embedding, maps into , and whose derivative preserves at every point. The Gromov width is the supremum of capacities for which embeds symplectically into .
For every and origin-symmetric convex body , .
For every and every origin-symmetric convex body ,
and for every there is a symplectic embedding . No embedding at capacity exactly is asserted.
The result itself. It answers the symmetric-polar-product width question with no smoothness, strict convexity or unconditionality assumptions, and through volume preservation it implies the symmetric Mahler inequality in every dimension (Corollary 5.3). For it also transports finite ball packings satisfying strict volume and pairwise-capacity conditions into (Corollary 5.5, p. 17). It is specific to symmetric polar products: the general Viterbo conjecture is false.
Formalizing it. Mathlib has smooth manifolds and differential forms but no symplectic capacities, nonsqueezing, or Moser's deformation method. A formal proof would need these, together with a conformal map of the disk with explicit boundary estimates. These components are reusable across symplectic geometry. No machine-checked computation of a Gromov width of a non-trivial domain is known.
The upper bound follows from Gromov nonsqueezing and a supporting-cylinder argument (or from the Hofer–Zehnder computation). The lower bound is the hard direction: knowing does not produce any ball, and explicit embeddings were previously known only for special families ( balls, the cube). The preprint's route (Sections 2–4) needs balls of capacity close to from holomorphic maps vanishing to order , and a momentum scale that is uniform up to the tips of a conformal lens, where slice heights approach as grows; a non-uniform estimate does not suffice.
EuclideanSpace ℝ (Fin n); phase space is their product. polar uses the real inner product; polarProduct K is interior K ×ˢ interior (polar K).capacityBall n c is the open ball , so a ball of radius has capacity .HasSymplecticEmbedding U V: some e with ContDiffOn ℝ ∞ e U, IsEmbedding on the subtype U, MapsTo e U V, and for all .gromovWidth is an sSup in ℝ≥0∞ of the admissible capacities, so an unbounded set would give ⊤; the goal asserts the value 4 and separately every capacity below .Welcome contributions: a Lean notion of symplectic embedding between open subsets of , Gromov nonsqueezing (as an axiom-free target in its own right), and volume preservation for symplectic maps.
The volume product of a convex body measures how large a body and its polar can simultaneously be. For a body without a distinguished centre, the polar is taken about the point that makes it smallest, the Santaló point, so the product is invariant under all invertible affine maps. The Blaschke–Santaló inequality identifies ellipsoids as the maximizers. Mahler's conjecture for general convex bodies asks for the minimizers and predicts simplices, with minimum value . The question arose from Mahler's work on polarity and the geometry of numbers, and it is the sharp form of the Bourgain–Milman reverse Santaló inequality.
This mission asks for a formal proof of the general Mahler conjecture with its equality case, as stated in an OpenAI preprint dated September 22, 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 convex body is a compact convex set with nonempty interior; is Lebesgue measure and the Euclidean inner product. For an interior point , the polar of about is
and the volume product is
The infimum is attained at the unique Santaló point . A simplex is the convex hull of affinely independent points.
For every and every convex body ,
with equality if and only if is a simplex.
The result itself. It is the exact form of a problem open since the 1930s and previously settled only in dimensions and and for polytopes with few vertices. Because the infimum over centres is taken, it gives the same lower bound for at every interior point . Via the known geometric-to-functional implication, the preprint derives the sharp functional Mahler inequality for log-concave functions and an entropy–transport inequality (Corollary 1.2, p. 4; Corollary 8.1, p. 41). The symmetric conjecture, with the larger constant , is a different statement treated in a companion preprint.
Formalizing it. The proof combines convex cones and their Laplace transforms, Gaussian Sobolev calculus, Moreau's decomposition, matrix divided differences, and certified one-variable inequalities. A formal proof would provide checked versions of these tools and of the Santaló point's existence and uniqueness. No machine-checked proof of the conjecture in any dimension is known.
Symmetrization does not apply, the volume product is not convex along natural deformations except in restricted families (shadow systems), and local minimality at simplices says nothing about distant bodies. In the preprint's route the main obstacle (Introduction, pp. 2–3) is that the Jacobian matrices of the Gaussian-averaged cone projections neither commute nor increase in : bounding them separately loses both the sharp constant and the equality case. Controlling them jointly requires comparing the whole family with spectral thresholds of a linear Gaussian matrix (Sections 5–7), and equality must then force the cone to split into half-lines.
EuclideanSpace ℝ (Fin n) with IsCompact, Convex ℝ and nonempty interior, and .polarAt K z is the polar about ; volumeProduct K is the sInf over interior K of (volume K).toReal * (volume (polarAt K z)).toReal. For an interior the polar is bounded, so toReal reads the true volume; the index set is nonempty because the interior is.volumeProduct K = (n+1)^(n+1)/(n!)^2 iff K = convexHull ℝ (range v) for some affinely independent v : Fin (n+1) → _.Welcome contributions: polar bodies and their volumes in Mathlib, the Santaló point, Laplace transforms of convex cones, and Gaussian integration by parts.
The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on for but not on . Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on for , because pointwise (Kinnunen 1997). At this argument breaks, since is unbounded on . Hajłasz and Onninen asked whether the gradient estimate nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual machinery is unavailable.
This mission asks for a formal proof of the planar centered-disk case, 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.
Identify with the Euclidean plane and write for the open disk of radius centered at . For a locally integrable real function , the centered disk maximal function is
The space consists of integrable whose distributional gradient is represented by an integrable vector field , i.e. for all . Norms of gradients are Euclidean: . For the signed estimate, put and .
There is an absolute constant such that for every real and with a power of two (including ),
with independent of , and the number of dyadic scales.
There is an absolute constant such that for every real , is finite almost everywhere, locally integrable, belongs to , and has a globally integrable weak gradient with
The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to inputs and yields a co-area type perimeter bound for level sets of . The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of in remain separate questions.
Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.
For one bounds and uses the strong maximal inequality, which fails for . One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).
EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real of lower Lebesgue integrals of over Metric.ball x r divided by ; the goal asserts it is finite a.e. before passing to maximalReal = toReal.HasWeakGradient f g is the integration-by-parts identity against every compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.sSup over the closed radius band ; the band envelope is continuous in , so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.The Hilbert transform is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field , integrate along the segment through in direction . Whether such directional Hilbert transforms are bounded on is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If depends on only one coordinate, the problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of is necessary, and some truncation of the integration length is necessary because a field can turn.
Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of . In the formulation of Lacey and Li, this is a uniform weak- conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.
The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong bound at short scale for every Lipschitz field.
Let be Lipschitz with . For the short directional Hilbert transform is
The direction is frozen at the output point . For a Schwartz function the principal value exists at every point, since .
There are absolute constants and such that every unit field with satisfies, for all ,
and the truncations and the principal value extend to bounded operators on with norm at most . The constants and are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.
The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for -Lipschitz fields at every outer length . By the dilation it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant is a convention of the formalization, not of the paper.
The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.
The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).
Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.
EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.twoSidedTruncation v ε a f x is the sum of interval integrals over and of ; smoothPrincipalValue integrates the symmetric quotient over , with the removable value at filled by the derivative.ShortHilbertConclusion a C bundles the five clauses (truncation bound for , principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for and .A complete development needs singular-integral and Littlewood–Paley machinery on , wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.
The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:
Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of . This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case () as Problem 13 in the 2017 collection Some problems in harmonic analysis.
For complex functions on and , the hard truncation is
and the maximal truncation is
For the finite truncations converge absolutely outside a common null set, and is measurable (Lemma 7.1 of the source).
There is an absolute constant such that, for all complex ,
The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and is almost-everywhere measurable. The goal statement is published on the platform with status Open.
The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each . It yields existence of the joint principal value almost everywhere and in (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form , which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.
Formalizing it. The estimate is a clean statement in Mathlib's and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.
Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales . The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.
ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).truncation F G E z is the Bochner integral of over , with endpoints packaged as Endpoints ().GoodPoint requires integrability on the annuli for all , hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of .For a set the distance set is . Falconer (1985) asked how large a set must be, measured by Hausdorff dimension, to force to have positive length. Examples built from lattices show that dimension is not enough in general, and Falconer conjectured that any compact set of dimension strictly greater than suffices. The question is the continuous analogue of Erdős's distinct-distances problem and has been a driving problem for geometric measure theory and Fourier restriction theory: progress on it has repeatedly come from, and fed back into, spherical averages, restriction estimates, decoupling and radial projections.
The source of this mission is an OpenAI preprint dated September 23, 2026.
The goal OAI.Falconer.falconer_distance_conjecture is open on the platform.
Theorem 1.1 resolves Falconer's distance conjecture in every dimension, with no regularity assumption beyond the strict dimension bound: no equality of Hausdorff and packing dimension, no Ahlfors regularity, no product structure. The threshold is sharp by Falconer's lattice examples, and no endpoint assertion is made. The result is unpinned: it does not assert that a single point has at the threshold. Positive measure is stronger than .
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The classical route bounds the norm of a distance measure via spherical averages of Fourier transforms (Mattila), and every improvement so far has come from finer restriction or decoupling estimates, which stall above . In higher dimensions there is a structural obstacle: radial projections of an -dimensional source cannot gain dimension above , so for one cannot assume radial projections have densities, and the angular input the Fourier argument needs must be built as cap bounds on directional fibres with arbitrarily small losses. Converting such fractal angular laws into a distance estimate requires a belt (rather than cap) estimate whose annular power is exactly balanced at , and a recursive multiscale accounting whose costs must be paid by a potential across two separated depths.
EuclideanSpace ℝ (Fin d), so dist is the Euclidean distance.dimH E : ℝ≥0∞ is Mathlib's Hausdorff dimension; the hypothesis is (d : ℝ≥0∞) / 2 < dimH E, strict.0 < volume {r : ℝ | ∃ x ∈ E, ∃ y ∈ E, dist x y = r} with Lebesgue volume on ℝ; compactness of makes this set compact.PlanarFalconer.distanceSet on EuclideanSpace ℝ (Fin 2) with 1 < dimH E.A complete development needs Frostman's lemma, energy and Fourier characterizations of dimension, Mattila's spherical-average criterion, stationary phase for spherical oscillatory integrals, and the Orponen–Shmerkin planar incidence theorem (used as an external input). Contributions formalizing Lemma 5.5 (the classical distance threshold ), Theorem 4.1 (linear projection gain), Theorem 4.2 (planar discretized Furstenberg estimate), Proposition 5.10 (starting pair measures), Proposition 8.1 (graph estimate) and Theorem 10.4 (single-profile angular bound) are welcome.