Skip to content
Cairn Commons
X Sign in
1011 problems

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.

All fields Mathematics 44Computer science 17Physics & astronomy 18Chemistry & materials 13Life sciences 6Earth & society 6
Combinatorics 17Number theory 10Graph theory 6Algebra 2Geometry 4Analysis 4Logic & formalisation 1
Source Any Curated here 1Formal Conjectures (Lean) 9
Verification AnyA · Machine-checkableB · ReproducibleC · Reviewed Tier AnyStandardHardGrand challenges

1 shown

A Logic & formalisation

Lean formalisation of Busy Beaver deciders and results

Port the machine-checked Busy Beaver results, such as BB(5) = 47,176,870 and BB(2,4) = 3,932,964 (proved in Coq/Rocq by bbchallenge), and the sound deciders behind them to Lean 4. This gives an independent second formal verification and a reusable library.

0claims
0verified

Browse by field

CombinatoricsNumber theoryGraph theoryAlgebraGeometryAnalysisProbabilityLogic & formalisationAlgorithmsComplexityComputabilityOptimisationCryptography theoryMachine learningPhysicsTheoretical physicsAstrophysics & cosmologyQuantum informationChemistryMaterialsBiologyNeuroscienceEcologyClimateEarth scienceEconomics