Float kernels
LiveBinary32 add, mul, sum and batched matrix multiply, each proved equal to its specification bit for bit. A faster entry takes over as champion.
- faster on the current benchmark
- 8.1×
- champions so far
- 36
Open math problems. Paid when Lean accepts the proof.
Unsolved conjectures, each written as an exact Lean statement. Use any model or method: the Lean kernel decides, a reviewer confirms, and the bounty is paid.
- Paid to solvers
- $105,687
- Rewards paid
- 36
- 260
- Open bounties
- 47
- Lean accepted
Results
Recently solved.
Each of these passed the Lean kernel and a human review before it was paid. The proof and its verification record are one click away.
$2,042
Research targets · 14 Oct 2026
Six-speed maximum-speed/denominator boundFor every primitive set of six distinct positive integer speeds with maximum loneliness p/q<1/6 in lowest terms, every speed is less than 3q.
by Elias
$2,177
Research targets · 14 Oct 2026
Wilf inequality for proper numerical semigroups with conductor at most four times multiplicityEvery proper numerical semigroup with conductor c at most four times its multiplicity satisfies c<=e*L.
by Elias
$4,118
Erdős problems · 14 Oct 2026
Erdős problem 1057The logarithm of the number of Carmichael integers at most x, divided by log x, tends to one.
by JenW1N and gus
$1,649
Research targets · 14 Oct 2026
Every scalar real polynomial minimal graph in dimension eight is affineEvery real polynomial in eight variables satisfying the polynomial minimal-surface operator identity has total degree at most one.
by JenW1N
Open problems
Pick one.
Each entry states the problem in ordinary mathematics next to the exact Lean statement you prove. What you read is what gets checked.
- Artin's Conjecture on Primitive Roots, first half. Let be an integer that is not a square number and not . Then the set of primes such that is a primitive root modulo has a positive asymptotic density inside the set of primes. In particular, is infinite.
Number theory
Artin Primitive Roots Conjecture - part i
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Borsuk's conjecture in dimension , the smallest open case.
Convex and discrete geometry
Borsuk Conjecture - four
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Brocard's Conjecture For every
Number theory
Brocard Conjecture
n ≥ 2, between the squares of then-th and(n+1)-th primes, there are at least four prime numbers.- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Bunyakovsky conjecture If a polynomial over integers satisfies both Schinzel and Bunyakovsky conditions, there exist infinitely many natural numbers such that is prime.
Number theory
Bunyakovsky
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- *Carmichael's totient function conjecture*: For every positive natural number , there exists a natural number with , such that .
Number theory
Carmichael Totient - charmichael Totient
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- There are infinitely many real quadratic fields
Number theory
Class Number Problem
ℚ(√d)with class number one, whered > 1is a squarefree integer.- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Dickson's conjecture If a finite set of linear integer forms satisfies Schinzel condition, there exist infinitely many natural numbers such that are primes for all .
Number theory
Dickson
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Is there some such that every integer is the sum of a prime and at most powers of ?
Combinatorics
Erdős problem 10
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
- Is the diameter of at least for some constant ?
Convex and discrete geometry
Erdős problem 100
- Attempts
- 0
- Modes
- 2
- Bounty
- $4,819
How it works
From problem to payout.
Pick a problem
Prove the statement or refute it. Both count, and one reward is paid per problem.
Work on it your way
Any model, agent or amount of compute. Keep the chat that produced the proof.
Check, then submit
Checking your file is free. Submitting costs one credit, and the chat logs go in with it.
Get paid
Lean checks the proof, a reviewer approves it, and the bounty goes to your wallet in alpha.
Optimisation
Faster code, proved correct.
The same rule applied to software. A submission is faster code plus a Lean proof that it behaves exactly like the original. The proof is checked first, then the speed is measured.
DEFLATE
EndedTwo weeks of LZ77 parsers for miniz_oxide, each proved in Lean to decode back to its input.
- proved parsers accepted
- 648
- faster than zopfli at the same size
- 29×