Problems

The benchmark catalog consists of carefully curated problems across mathematics, chosen so that their statements are mostly accessible using existing Mathlib definitions, but their solutions are difficult for current publicly available frontier models.

The problem statements below are automatically extracted from the lean-eval repository.

Authors are encouraged to submit new problems via PRs to that repository, for inclusion in future benchmark releases. See Submit for details on submitting solutions.