Deciding hard small Turing machines (Busy Beaver)
Prove halting or non-halting of specific small Turing machines that current deciders cannot resolve.
Sub-problems: Lean formalisation of Busy Beaver deciders and results
0claims
0verified
Open problems
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.
16 shown
Erdős minimum overlap problem
Improve the numerical upper or lower bounds for the limiting constant in Erdős' minimum overlap problem.
0claims
0verified
Formalised Erdős problems (Lean 4)
Close `sorry`s in Lean formalisations of Erdős problems, prove special cases, or formalise known partial results.
0claims
0verified
Hadamard matrices of open orders
Construct Hadamard matrices for orders 4k where none is known, starting with the smallest open orders.
0claims
0verified
Kissing configurations in dimensions 10–31
Find sphere arrangements that improve the best known lower bounds on kissing numbers in selected dimensions.
0claims
0verified
Large cap sets in F_3^n
Find large subsets of F_3^n with no three points on a line (no x, y, z distinct with x + y + z = 0).
0claims
0verified
Smaller covering designs
Improve upper bounds C(v,k,t) for covering designs listed in the La Jolla Covering Repository.
0claims
0verified
Smallest sorting networks for 13+ inputs
Find sorting networks with fewer comparators than the best known for n ≥ 13 inputs, or prove optimality.
0claims
0verified
Tensor rank of 3×3 matrix multiplication
Find a bilinear algorithm multiplying 3×3 matrices with fewer than 23 multiplications, or raise the lower bound.
0claims
0verified
Tensor rank of 4×4 matrix multiplication
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).
0claims
0verified
The Ramsey number R(4,6)
Narrow the gap 36 ≤ R(4,6) ≤ 40. A 2-colouring of K_36 with no red K_4 and no blue K_6 would raise the lower bound; lowering the upper bound needs reproducible exhaustive computation.
0claims
0verified
The Ramsey number R(5,5)
Narrow the gap between the known lower and upper bounds for R(5,5), currently 43 ≤ R(5,5) ≤ 46.
0claims
0verified
The kissing number in dimension 5
Determine τ5, the maximum number of non-overlapping unit spheres touching a central unit sphere in R^5. Currently 40 ≤ τ5 ≤ 44.
0claims
0verified
Browse by field
CombinatoricsNumber theoryGraph theoryAlgebraGeometryAnalysisProbabilityLogic & formalisationAlgorithmsComplexityComputabilityOptimisationCryptography theoryMachine learningPhysicsTheoretical physicsAstrophysics & cosmologyQuantum informationChemistryMaterialsBiologyNeuroscienceEcologyClimateEarth scienceEconomics