Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In the -server problem, servers sit at points of a metric space; requests arrive one at a time, and each request must be served by moving some server onto it, at a cost equal to the distance travelled. An online policy sees only the requests revealed so far, and its quality is measured by its competitive ratio: how much more it moves, in expectation, than the offline optimum that knows the whole sequence. The problem was introduced as a common framework for paging, caching and other online service problems, and the question of the best ratio achievable by randomized policies has driven the development of metric embeddings, online primal-dual methods and entropic regularization.
This mission asks for a formal proof that randomized -server has competitive ratio on every metric space, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a metric space and the initial positions of labelled servers; repeated positions are allowed. To serve a request , a policy chooses one label and moves server to , leaving the others fixed (a server already at may be chosen at zero cost). For a finite request sequence , is the total distance moved and is the minimum of this cost over all label sequences, chosen with knowledge of . A randomized online policy chooses, at each step, a probability distribution over labels as a function of the past requests, its own past choices and the current request. Requests are fixed in advance, independently of the policy's randomness (the oblivious adversary).
There is an absolute constant such that for every , every metric space with at least points, and every , there are a randomized online policy and a finite with
for every finite request sequence . The same policy serves all sequences and horizons; may depend on , and but not on ; and when the entries of are distinct.
The result itself. Combined with the Bubeck–Coester–Rabani lower bound, it identifies as the worst-case order of the randomized competitive ratio over all metrics. The bound has no dependence on the number of points, the aspect ratio, finiteness or boundedness of , removing the factor left by static tree embeddings. No computational efficiency is claimed; a companion preprint turns the existence statement into a uniform algorithm on finite rational metrics.
Formalizing it. The statement is elementary to state, but its proof combines a rank-based allocation on separated trees, slowly varying simplex trackers, a compact potential for partition edits, online partitions with an embedded comparator, balanced rounding, and a compactness argument (Tychonoff) producing one policy for all finite inputs. None of these online-algorithm tools exist in a formal library, and a machine-checked competitive analysis of a randomized -server algorithm on general metrics is not known.
Embedding the metric into a random hierarchically separated tree and running an tree algorithm loses the embedding distortion, which is in the worst case and is not bounded in terms of . Removing it requires changing the tree as requests arrive, and the cost of re-partitioning must be paid for. A previous dynamic approach (Lee's fusible HSTs) had its general claim withdrawn after a gap in that accounting (p. 3). In the preprint, the partition schedule is driven by the posterior measure of a hidden comparator, and the edit costs and the travel of parked mass are bounded separately (Sections 7–8). Passing from finite metrics and finite horizons to one policy on an arbitrary, possibly infinite and unbounded, space with a fixed constant requires a further compactness step (Section 10).
X : Type u carries an arbitrary MetricSpace instance; "at least points" is an injection Fin (k+1) → X. No finiteness, separability or boundedness is assumed.Policy k X maps the history (list of past requests with the labels used) and the current request to a LabelDistribution k, i.e. a probability vector on Fin k. Every step moves exactly one server (Function.update), as in the source.expectedCost is the finite sum over all label sequences of the path probability times the service cost; optimalCost is the sInf over all label sequences of the service cost (nonempty finite set, so the infimum is a minimum). Restricting the offline optimum to one-server-per-request service does not change it (triangle inequality).Function.Injective s → B = 0 encodes the distinct-start clause.Real.log).Multiplying two matrices by the schoolbook method costs about operations. The matrix-multiplication exponent of a field is the infimum of exponents such that matrices over can be multiplied with additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.
Fix a field . An arithmetic program is a straight-line sequence of gates, each a constant from , an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies matrices if designated registers equal the entries of for every pair of input matrices over . A real number is admissible if for every there is such that for every some correct program has cost at most , and
In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].
The Lean statement also contains the numerical comparison , which carries no mathematical content (the source writes the comparison as ). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on from (Dupont et al.) to , and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.
Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on needs.
Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.
F : Type u, with free constants from and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".AdmissibleExponent F τ asks, for each , for one constant that works for every . omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.A graph is three-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding three-colorability is NP-complete. The approximate coloring problem asks how much a promise helps: given a graph promised to be three-colorable, can one efficiently find a coloring with a few more colors, or at least a large independent set? Every three-colorable graph on vertices has an independent set of size (its largest color class). The best polynomial-time algorithms use colors, while hardness results long reached only small palettes and needed extra conjectures for stronger gaps. Problems of this kind are central test cases for the PCP theorem, Label Cover and the theory of promise constraint satisfaction.
A 3-CNF formula is a conjunction of clauses, each a disjunction of at most three literals (variables or their negations); it is satisfiable if some truth assignment makes every clause true. For a finite simple undirected graph with vertices, is the size of a largest independent set, a set of pairwise nonadjacent vertices. A polynomial-time reduction is a deterministic algorithm that, on an explicit binary encoding of its input, runs in time polynomial in the encoding length and outputs an explicit encoding (here the full adjacency matrix) of the output graph.
For every fixed real there is a deterministic polynomial-time algorithm mapping each explicitly encoded 3-CNF formula to a nonempty finite simple graph with
The running time and output size are polynomial in the binary length of , with constants depending only on . The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 shows that, even with the full promise of three-colorability, it is NP-hard to find an independent set of any fixed positive density. It implies hardness of distinguishing -colorable graphs from non--colorable graphs for all fixed (Corollary 1.2), the long-standing conjecture recorded by Barto–Bulín–Krokhin–Opršal. Unlike the routes through -to- games and arc graphs, it keeps the independent-set soundness together with three-colorable completeness, and unlike Dinur–Khot–Perkins–Safra it does not delete vertices. Earlier results with this combination were conditional (Dinur–Mossel–Regev; Braverman–Khot–Lifshitz–Minzer).
Formalizing it. The statement is fully explicit: Mathlib's TM2ComputableInPolyTime fixes the machine model, and the formula and graph encodings are spelled out bit by bit. A formal proof would require a machine-checked PCP theorem with perfect completeness (Label Cover), a dimension-independent junta approximation theorem, and the paper's alignment and list-decoding lemmas. Any of these is a substantial and reusable formalization project; complexity-theoretic reductions are barely represented in Mathlib today.
Gap reductions from Label Cover to coloring traditionally use long-code or dictatorship tests whose soundness analysis loses control either of three-colorability of every vertex (completeness) or of independent sets of arbitrarily small density (soundness). Known unconditional routes reach constant-palette coloring hardness only by composing reductions that lose the independent-set guarantee, and routes keeping it required unproven games conjectures with structural assumptions. The proof must decode a labeling from any independent set of density in a graph that is genuinely three-colorable on every vertex when is satisfiable, without bounds on projection-fiber sizes.
Graph records: vertices Fin n, a symmetric loopless Boolean adjacency. Independence number is the maximum card of an independent Finset; three-colorability is a proper map to Fin 3.RealGraphReduction δ packages a function reduce : List Bool → Graph with a Turing.TM2ComputableInPolyTime witness (identity input encoding, graphBits output encoding, finite stack alphabets), an explicit polynomial output-size bound, completeness and strict soundness on encoded formulas. The reduction must be total and polynomial-time on all bit strings, which is harmless since malformed inputs can be sent to a fixed graph.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 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.
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 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 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 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.
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.
The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.
The Riemann sphere is , with local coordinate near finite points and near . A domain is a nonempty connected open subset. A map is conformal at if it is continuous at and, in these coordinates, complex differentiable at with nonzero derivative. A conformal equivalence is a bijection that is conformal at every point of and whose inverse is conformal at every point of .
A closed round disk in is the image of the closed unit disk under a Möbius transformation , ; these are closed Euclidean disks, closed half-planes together with , and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.
Lean: OAI.Problem047.koebe_circle_domain, open on the platform.
The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.
The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.
The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.
Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of in the charts chart p, chart (f p) (identity coordinate at finite points, at ).IsConformalEquivalence f U V: conformal on , MapsTo f U V, and a conformal g on with MapsTo g V U that is a two-sided inverse.IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).U; there is no countability or regularity assumption on the complement.A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.
A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.
The Riemann sphere has local coordinates and . A map is conformal at if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence is a bijection, conformal on , with conformal inverse. A Möbius transformation is with . A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.
A compact is conformally removable if every orientation-preserving homeomorphism of that is conformal on is Möbius. A circle domain is conformally rigid if every conformal equivalence from onto another circle domain is the restriction of a Möbius transformation.
Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of is assumed.
Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions (-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.
Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of may correspond to a disk component of and vice versa, so the coordinates of need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.
Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts and with HasDerivAt and a nonzero derivative.IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.
A bounded symmetric domain is a bounded connected open set in with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.
Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.
An affine variety is a reduced complex algebraic set , the common zero locus of a set of polynomials. A subset of is semialgebraic if it is a finite Boolean combination of sets and , with a real polynomial in the real and imaginary parts of the coordinates. Let be open in , connected, semialgebraic and bounded. A map on is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of ; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group acts properly discontinuously if the action is proper for the discrete topology on (finite stabilizers are allowed), and the action is cocompact if is compact. is smooth if each point has a neighbourhood in biholomorphic to an open subset of some .
Let be a nonempty connected semialgebraic bounded open subset of a complex affine variety , and let a group act on by biholomorphisms, properly discontinuously and with compact. Then
The goal statement is published on the platform with status Open.
The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.
Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.
The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model to which Vey's theorem applies.
IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; is open in the subspace topology of , IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in , closed under complement and union.ProperSMul and a compact orbit space. Each acts holomorphically in the sense of local ambient analytic extension; since also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.IsSmooth U asks for local biholomorphisms of neighbourhoods in onto open subsets of some . IsBoundedSymmetricDomain D asks that be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For points on a surface with ample , a dimension count gives the universal upper bound . Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at very general points for every sufficiently large . On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.
Let be a smooth integral complex projective surface and an ample line bundle, with self-intersection . For a tuple of distinct points, the multipoint Seshadri constant is
the infimum over integral curves through at least one . If is the blow-up at with exceptional curves , then is the largest such that is nef (nonnegative on every integral curve), and always . Let be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of .
For every such there is such that for each there is a countable union of proper Zariski-closed subsets of , with , such that for every
The threshold may depend on and is not explicit. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below , including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ( in ) is a separate companion result.
Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.
The upper bound is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on . The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in .
Surface: an integral scheme, smooth of relative dimension over , with a closed immersion into some compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then and , by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return ; finite-dimensionality for projective schemes is part of what a solver must prove.IsClosed, ≠ univ, with a point outside all of them).sInf over integral curves with positive total multiplicity.PointBlowup, characterized by its universal property, and the exceptional ideal sheaves . The inequality is for every integral curve on the blow-up.Euler's totient counts the integers in coprime to . Many integers share a totient, and most integers are not totients at all, so counting the distinct values of is much harder than counting integers with a given factorization. Let
The size of was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines up to a bounded multiplicative factor but leaves open whether has an asymptotic equivalent, and Erdős and Hall's question whether .
This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Logarithms are natural and is the -fold iterate. For let , let be the unique root of , and set
For large put , , the phase , and ; the factor is Ford's counting scale.
For each the preprint defines an explicit arithmetic coefficient , , from a finite set of "tail witnesses" (tuples of primes , , and a cofactor , subject to explicit size and recurrence constraints, ) by inclusion–exclusion over witnesses with a common totient , weighted by (formula (2.8), p. 5). Here is the least preimage, and when the limit exists. The coefficient is defined without reference to .
for .
uniformly on , with , and
For let and . Then converges uniformly and ; if some totient has then and , and otherwise and . The positive alternative holds for .
The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase , built from finite arithmetic data, and answers the Erdős–Hall question: is regularly varying of index . Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals , reducing it to the existence of a "seed" totient with . Whether such seeds exist for every (equivalently, whether is unbounded) is not settled by the preprint.
Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root , the witnesses, ) are explicit and can be checked independently of any proof.
Counting integers with a typical factorization is a volume computation, but counts values, and different can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ( with fixed, then ), and no continuity of is available, so all errors must be uniform in the phase.
IsTotient v means for some ; V x counts totients in ; ell v is Nat.find of the least preimage (junk value for non-totients, never used on them).rho is the sInf of roots in of ; the root is unique, so this is the source's .AH H f s is formula (2.8) with finsum over totients and over nonempty finite sets of witnesses with ; the witness set is finite for each , so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).coefficient_nonnegative is stated for every , while the source states it for sufficiently large ; for small the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.For a positive integer , Jacobsthal's function is the least such that every run of consecutive integers contains an integer coprime to . Equivalently, is the longest interval that can be covered by choosing one residue class modulo each prime divisor of (the classes shifted by the interval's start). Its maximum over integers with at most prime divisors,
governs how long a stretch can be sieved out by primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether .
The source of this mission is an OpenAI preprint dated September 25, 2026.
Both are stated in Lean as the existence, for each , of a length satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.
Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter , where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly ) remains large; Vaughan suggested .
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant is not made explicit.
The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.
IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for the denominator is positive.IsJacobsthalBound identically.A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.
Goldbach-type problems ask which sets are sumsets of primes. The inverse Goldbach problem, due to Ostmann (1956), reverses the question: can the set of primes itself, up to finitely many changes, be written as a sumset with both and having at least two elements? Ostmann conjectured that it cannot: the primes are asymptotically additively indecomposable. The problem is a clean test of how much additive structure the primes can carry, and it connects sieve theory (the primes avoid one residue class modulo each prime) with inverse questions for the large sieve.
The source of this mission is an OpenAI preprint dated September 24, 2026.
Let and let be the set of positive primes. For the sumset is . Two sets are asymptotically equal if their symmetric difference is finite. A decomposition is nontrivial if and ; the trivial decompositions are excluded.
Theorem 2.3 is the core of the proof; Lemma 2.2 reduces Theorem 1.1 to it by a short sieve argument.
The goal OAI.Ostmann.inverseGoldbach is open on the platform.
Theorem 1.1 resolves Ostmann's conjecture. The conclusion controls both requirements of an eventual decomposition: if and contains every sufficiently large prime, then contains infinitely many composite numbers. The proof does not go through the general inverse large-sieve conjecture of Green and Harper; it uses the simultaneous residue restrictions together with coverage of every large prime directly.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The statement is elementary, so the formal target is short; the difficulty is entirely in the proof.
Counting alone cannot work: sieve bounds put and near , which is compatible with the lower bound forced by covering the primes. The known necessary conditions (large intersections with quadratic images) fall short of the near-containment that Green and Harper's conditional route requires. The proof must turn the local information (modulo each prime , the images of and are disjoint) into a global contradiction: it rules out correlations with translated multiplicative characters of every order, compares a positive sumset statistic with its average over the primes, and handles residue indicators with no prescribed algebraic form via a finite-field comparison of binary trees. The paper runs to about 80 pages.
primes = {n : ℕ | Nat.Prime n}; sumset A B is Mathlib's pointwise A + B on Set ℕ.A.Nontrivial means has two distinct elements.InverseGoldbach asserts Set.Infinite (sumset A B ∆ primes); TwoInfiniteSummandsImpossible uses EventuallyPrimeSumset A B := ∃ N, ∀ n ≥ N, n ∈ A + B ↔ n.Prime, which is equivalent to a finite symmetric difference.OAI.Ostmann.main is the same statement as the goal without the definition file and is included as a reference item.A complete development needs the additive large sieve (Montgomery–Vaughan), Gallagher's larger sieve, Mertens-type estimates, character sums over finite fields including the quadratic large sieve, prime number theorems in progressions with the exceptional character, and Fourier analysis on . Contributions formalizing Lemma 2.1 (fixed shifts), Lemma 2.2 (finite summands), Lemma 2.4 (square-root bounds), Proposition 3.1, Corollary 4.2 (mixed-character decorrelation), Proposition 5.1 and Lemma 6.1 (tree comparison) are welcome.
Let be the largest prime factor of an integer . The classical theory of smooth numbers (Dickman 1930, Ramaswami 1949, de Bruijn 1951) shows that has a limiting distribution: the proportion of with tends to , where is the Dickman function. Multiplicative structure of and of is expected to be independent, since consecutive integers share no prime factor, but proving independence of such "additive shifts" of multiplicative data is the core difficulty of the Chowla/Elliott circle of problems. Erdős and Pomerance (1978) asked whether and are asymptotically independent with Dickman marginals, and, as a consequence, whether holds for exactly half of all (a comparison question usually attributed to Erdős and Turán).
For , is the largest prime dividing . The Dickman function is the continuous function with
equivalently for . For a property of integers and real , the natural density at scale is
For every fixed ,
with running over all reals and ordinary, unweighted counting. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 says that, in natural density, and are independent with Dickman marginals. It settles the Erdős–Pomerance independence question positively, removes the logarithmic weighting of Teräväinen's theorem and the exceptional scales of Tao–Teräväinen, and implies the Erdős–Turán comparison: because the limiting marginal is continuous, the product law gives no mass to the diagonal, so each strict ordering has density (Corollary 1.2). Previous unconditional work only gave lower natural densities, never the existence of the density.
Formalizing it. The goal is a clean density statement about elementary objects, but its proof combines Matomäki–Radziwiłł short-interval estimates, sieve bounds, a divisor amplifier, graph comparison and cut-norm sampling. No part of this argument is machine-checked. Even the one-variable Dickman law (the marginal case) is not in Mathlib, and would be a reusable milestone in its own right.
Independence of and is a binary correlation problem for multiplicative data, of the same nature as the two-point Chowla conjecture. Tao's entropy-decrement and logarithmic-averaging method handles such correlations only with weight , or at almost all scales; the step that fails for ordinary density is ruling out a positive correlation along a sparse sequence of scales. The indicator is also not multiplicative, so short-interval theorems for multiplicative functions do not apply to it directly.
Nat.maxPrimeFac n (largest element of the prime factor list, a faithful backport of the Mathlib definition) represents ; its junk values at are irrelevant since counting starts at .realDensity P X is #{n ∈ [2, ⌊X⌋] : P n} / X as a real number, and limits are Tendsto … atTop over real , matching "the limit over all real ".(n:ℝ)^a, and the hypotheses , are explicit.stepApprox and evaluating the -th iterate at ; this agrees with the Dickman function on , which is the only range used (). A wrong would make the goal false, so this definition is part of what solvers should check.A mathematical program with complementarity constraints (MPCC, also called MPEC, mathematical program with equilibrium constraints) is a nonlinear optimization problem in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such constraints model equilibria inside an optimization problem: bilevel programs whose lower level is replaced by its optimality conditions, Stackelberg games, traffic and electricity market equilibria, contact problems in mechanics. See Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996), doi:10.1017/CBO9780511983658.
The complementarity constraints make the standard theory fail. At every feasible point the Mangasarian–Fromovitz constraint qualification is violated, so the Karush–Kuhn–Tucker conditions are not necessary for optimality, and standard NLP solvers lose their convergence guarantees. A common remedy is relaxation: replace the MPEC by a family of ordinary nonlinear programs depending on a parameter , solve them for , and study the limits of their stationary points.
The first relaxation scheme, and the reference point for all later ones, is due to Scholtes (Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001), doi:10.1137/S1052623499361233). Scholtes showed that limits of stationary points of the relaxed programs are C-stationary when MPEC-LICQ holds at the limit. Hoheisel, Kanzow and Schwartz (Preprint 299, University of Würzburg, 2010; later Math. Program. 137 (2013), doi:10.1007/s10107-011-0488-5) compare five relaxation schemes and weaken the constraint qualification in each convergence theorem. For Scholtes' scheme, their Theorem 3.1 replaces MPEC-LICQ by the weaker MPEC-MFCQ. This mission formalizes that theorem.
The MPEC (1) is
with continuously differentiable and feasible set . For a point the paper uses the index sets , , and .
A standard nonlinear program has constraints , . Its point satisfies the Mangasarian–Fromovitz constraint qualification (MFCQ) if the gradients are linearly independent and some direction has for all active and for all . A stationary point is the -part of a KKT point: is feasible and there are , with and .
The tightened program TNLP keeps , and imposes on , on , and on . MPEC-MFCQ holds at if MFCQ holds at for TNLP.
A feasible is weakly stationary if there are multipliers , , with
, , on and on . It is C-stationary if such multipliers can be chosen with, in addition, for all .
Scholtes' relaxed program replaces by and keeps all other constraints of (1). The notation means a sequence of positive parameters decreasing to .
Let , let be a stationary point of , and let with MPEC-MFCQ at . Then
No feasibility of is assumed; it is part of the conclusion.
Theorem 3.1 says that Scholtes' scheme, run to the limit, produces C-stationary points under a constraint qualification strictly weaker than the one in Scholtes' original result. MPEC-MFCQ is the natural assumption here: under it the KKT multipliers of the relaxed programs need not converge, and the theorem shows that a convergent subsequence of suitably modified multipliers still exists. The result is the first of a family of convergence theorems in the paper (the schemes of Lin–Fukushima, Kadrani–Dussault–Benchakroun and Steffensen–Ulbrich follow the same pattern) and the baseline against which those schemes are compared.
The theorem is proved in the paper; it is not open. To the extent a search of the Prove2Me catalog shows, no MPEC stationarity concept, MPEC constraint qualification or relaxation result has been formalized there, and Mathlib has no theory of constraint qualifications for nonlinear programs. The mission produces a machine-checked proof of Theorem 3.1 and, along the way, reusable statements of Definition 2.1, MFCQ, KKT points and the MFCQ/positive-linear-independence equivalence for general nonlinear programs.
The obvious argument takes a limit of the KKT multipliers of . That fails twice. First, under MPEC-MFCQ the multiplier sequence need not be bounded, so there may be nothing to take a limit of; boundedness has to be recovered from MPEC-MFCQ through positive-linear independence, a theorem of the alternative. Second, the multiplier of the product constraint multiplies , which is not a multiplier of or alone; how it is redistributed depends on whether lies in , or , and the sign condition on comes from the support disjointness between and the multipliers of , , which uses . Compactness, index-set bookkeeping along a subsequence and continuity of all gradients have to be combined.
EuclideanSpace ℝ (Fin n), gradients are Mathlib's gradient, and is the inner product. Constraint indices are Fin m, Fin p, Fin l (0-based); may be .P.IsC1 (ContDiff ℝ 1 for each function) of the goal and of milestones 4 and 5. Milestones 1–3 are pointwise linear algebra and assume no smoothness.