Each problem states how progress is verified and what counts as a contribution. Besides the problems curated here, the catalogue includes open conjectures from Formal Conjectures (with Lean statements), optimization constants and the AlphaEvolve problems. Know one that belongs here? Propose a problem.
4 shown
Settle open finite combinatorial questions with SAT solvers that emit checkable unsatisfiability proofs (DRAT/LRAT). Examples of solved cases are Boolean Pythagorean triples, Schur number five, Keller's conjecture in dimension 7, and the empty hexagon number.
Find sorting networks with fewer comparators than the best known for n ≥ 13 inputs, or prove optimality.
Find a bilinear algorithm multiplying 3×3 matrices with fewer than 23 multiplications, or raise the lower bound.
Find bilinear algorithms that multiply two 4×4 matrices with fewer multiplications. The records are 48 over Q and C (2025) and 47 over GF(2) (2022).
