Problem collections
The public problem lists we import or curate from. Every problem keeps a link to its source; results are checked here and should also be reported upstream.
Formal Conjectures
Formal Conjectures is an open repository, started by Google DeepMind, of conjectures stated in Lean 4 with Mathlib.
367 problemsErdős problems
Paul Erdős posed hundreds of problems, many with cash prizes.
44 problemsBen Green's 100 open problems
Ben Green (Oxford) keeps a list of 100 open problems, mostly in additive combinatorics and related number theory, with notes on what is known.
139 problemsOEIS conjectures
Conjectures stated in OEIS entries — that a sequence is infinite, that a formula holds for all n, that some search never ends — formalised in Lean by Formal Conjectures.
106 problemsOptimization constants
Constants defined by an optimisation problem — the best bound in an inequality, the extremal value of a construction — whose exact value is unknown.
44 problemsAlphaEvolve problems
The problems from Georgiev, Gómez-Serrano, Tao and Wagner, Mathematical exploration and discovery at scale (2025), where AlphaEvolve searched for constructions in analysis, combinatorics and geometry.
36 problemsOberwolfach problems
Problems posed at problem sessions of workshops at the Mathematisches Forschungsinstitut Oberwolfach and recorded in Oberwolfach Reports 2024–2026.