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.
Push the boundary of where zeros can exist.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
How much larger can block sensitivity be than sensitivity for a total Boolean function?
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
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?
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?
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…
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
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.
An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least such that every natural number greater than is a sum of at most primes; that such a exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give , and is close to equivalent to that…
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as…
Stochastic differential equations combine deterministic dynamics with random forcing, making them a common mathematical language for continuous-time uncertainty. Simo Särkkä and Arno Solin's Applied Stochastic Differential Equations (Cambridge University Press, 2019) develops this subject from ordinary differential equations and Brownian motion through…
The Collatz conjecture, also called the problem, asks whether one elementary iteration rule has the same long-term behavior for every positive integer. It belongs to number theory and discrete dynamical systems: the rule is deterministic and trivial to compute for any fixed input, but no argument is known that controls every orbit. The problem has…
A number field has a unit group which, by Dirichlet's unit theorem, is free of -rank modulo roots of unity. Fix a prime and embed the units diagonally into the units of the completions of at the primes above . The topological closure of the image is a finite free a …
An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout…
A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the…
A positive integer is perfect when it equals the sum of its proper divisors: , , then , , and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that…
Nonconvex optimization over a polytope, with , is the basic model behind constrained training problems and many operations-research formulations. Gradient methods reach first-order stationary points, but these include strict saddle points, which degrade solutions in practice. The usual remedy…
Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the rev…
The Riemann zeta function governs the distribution of prime numbers, and the size of on the critical line controls error terms throughout analytic number theory. In 1908 Ernst Lindelöf asked how fast can grow as and conjectured that it grows more slowly than every positive power of .…
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed so that the signed sum is bounded in every coordinate by a universal constant — independent of how many…
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct…
Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number , choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that…
A finite Gaussian location mixture in is the law of , where the hidden index takes the value with probability and is independent noise. Such mixtures are a basic model of heterogeneous data in statistics and machine learning. Distribution learning asks for a description of a law close to the mixture in…
The quantum relative entropy is frequently used as a distance, or distinguishability measure between two quantum states. In this paper we study the relation between this measure and a number of other measures used for that purpose, including the trace norm distance. More precisely, we derive lower and upper bounds on the relative entropy in terms of various…
A polynomial is split if and for some and . Split polynomials are the simplest non-constant maps defined over that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational.…
Communication complexity measures how many bits (or qubits) two parties, Alice and Bob, must exchange to solve a joint task when each sees only part of the input. It is one of the few settings where quantum advantages can be proved unconditionally, and such separations now underpin experimental demonstrations of quantum advantage in space (Kretschmer et al.…
A Fisher market sells divisible items to agents who each hold a budget; a competitive equilibrium (CE) is a price vector at which every agent buys a best bundle she can afford and every item is sold. When the items are goods with linear utilities, equilibria are the optimal solutions of the convex Eisenberg–Gale program and can be computed in polynomial…
An election is run by someone — a chair, a committee, an organiser — who can shape it without touching a single ballot: by deciding which candidates appear, which voters are registered, or how the electorate is split into bodies that pre-select nominees. Bartholdi, Tovey and Trick (1992) proposed to measure how well a voting rule protects itself against…
The n-Queens problem, placing mutually non-attacking queens on an chessboard, is a standard benchmark in constraint programming and artificial intelligence. As a decision problem it is trivial: a solution exists for every other than and and can be written down in closed form, and the input has only bits. This has…
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the…
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the…
A strongly regular graph with parameters is a finite simple graph on vertices in which every vertex has exactly neighbours, every pair of adjacent vertices has exactly common neighbours, and every pair of non-adjacent vertices has exactly common neighbours. For most parameter tuples the elementary counting and integrality…