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.
Results
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.
$4,477
$4,597
$762
$1,752
Research targets · 28 Oct 2026
Fourth planar Dirichlet Polya inequality, area times lambda4 at least 16piby Jordan
Open problems
Each entry states the problem in ordinary mathematics next to the exact Lean statement you prove. What you read is what gets checked.
Number theory
Convex and discrete geometry
Number theory
n ≥ 2, between the squares of the n-th and (n+1)-th primes,
there are at least four prime numbers.Number theory
Number theory
Number theory
ℚ(√d) with class number one,
where d > 1 is a squarefree integer.Number theory
Combinatorics
Convex and discrete geometry
How it works
Prove the statement or refute it. Both count, and one reward is paid per problem.
Any model, agent or amount of compute. Keep the chat that produced the proof.
Checking your file is free. Submitting costs one credit, and the chat logs go in with it.
Lean checks the proof, a reviewer approves it, and the bounty goes to your wallet in alpha.
Optimisation
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.
The nineteen kernels behind six families of neural networks, recurrent ones included, proved equal to their specification and timed on generated workloads and trained models on seven boards: one per model family and one overall.
The twelve kernels behind five neural networks, proved equal to their specification and timed on six boards. Replaced by Tensor kernels.
Binary32 add, mul, sum and batched matrix multiply, each proved equal to its specification bit for bit. Replaced by TorchLean kernels.
Two weeks of LZ77 parsers for miniz_oxide, each proved in Lean to decode back to its input.