Browse by category
Browse by source
- Erdős Problems 864 files with 2714 statements
- OEIS 235 files with 1635 statements
- Wikipedia 158 files with 784 statements
- Papers 41 files with 286 statements
- Green's Open Problems 55 files with 261 statements
- arXiv 39 files with 221 statements
- Written on the Wall II 56 files with 158 statements
- OpenQuantumProblems 3 files with 127 statements
- MathOverflow 13 files with 65 statements
- Other 10 files with 55 statements
- Books 12 files with 52 statements
- Millennium Prize Problems 5 files with 30 statements
- Hilbert Problems 2 files with 13 statements
- Kourovka Notebook 7 files with 10 statements
- OptimizationConstants 1 files with 5 statements
- LittProblems 1 files with 4 statements
Browse by subject
- Number theory 4131 statements
- Combinatorics 1846 statements
- Convex and discrete geometry 227 statements
- Linear and multilinear algebra; matrix theory 188 statements
- Quantum theory 175 statements
- Algebraic geometry 172 statements
- Geometry 137 statements
- Information and communication, circuits 113 statements
- Field theory and polynomials 106 statements
- Functions of a complex variable 99 statements
- Group theory and generalizations 85 statements
- Computer science 69 statements
- Associative rings and algebras 69 statements
- Mathematical logic and foundations 67 statements
- Measure and integration 65 statements
- Operator theory 57 statements
- Real functions 54 statements
- Harmonic analysis on Euclidean spaces 51 statements
- Sequences, series, summability 45 statements
- Probability theory and stochastic processes 44 statements
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.