Browse by category
Browse by source
- Erdős Problems 1307
- Wikipedia 471
- Green's Open Problems 160
- Papers 130
- OpenQuantumProblems 125
- Written on the Wall II 110
- OEIS 105
- arXiv 57
- MathOverflow 53
- Millennium Prize Problems 19
- Other 18
- Hilbert Problems 13
- Books 6
- OptimizationConstants 5
- Util 4
- Kourovka Notebook 2
Browse by subject
- Number theory 1527
- Combinatorics 909
- Quantum theory 183
- Linear and multilinear algebra; matrix theory 140
- Information and communication, circuits 96
- Convex and discrete geometry 93
- Algebraic geometry 88
- Geometry 56
- Field theory and polynomials 54
- Group theory and generalizations 42
- Special functions 41
- Operator theory 35
- Mathematical logic and foundations 29
- General topology 28
- Functions of a complex variable 27
- Real functions 24
- Computer science 22
- Measure and integration 18
- Order, lattices, ordered algebraic structures 16
- Dynamical systems and ergodic theory 15
What is this?
While there is a growing corpus of formalised theorems including proofs, there is a lack of open conjectures where only the statement has been formalised. This repository collects such statements from diverse sources — ErdÅ‘s’s problem lists, Wikipedia, MathOverflow, the OEIS, research papers, and more.
The project aims to become a benchmark for automated theorem provers, help clarify conjectures through formalisation, and highlight gaps in Mathlib.