Mathematical Proofs

MiniF2F is a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The miniF2F benchmark currently targets Metamath, Lean, and Isabelle and consists of 488 problem statements drawn from the AIME, AMC, and the International Mathematical Olympiad (IMO), as well as material from high-school and undergraduate mathematics courses.

A new large-scale geometry problem-solving dataset - 3,002 multi-choice geometry problems - dense annotations in formal language for the diagrams and text - 27,213 annotated diagram logic forms (literals) - 6,293 annotated text logic forms (literals)

ProofNet is a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. Source: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics Image Source: https://arxiv.org/pdf/2302.12433v1.pdf

MED is a new evaluation dataset that covers a wide range of monotonicity reasoning that was created by crowdsourcing and collected from linguistics publications. The dataset was constructed by collecting naturally-occurring examples by crowdsourcing and well-designed ones from linguistics publications. It consists of 5,382 examples. Source: https://github.com/verypluming/MED Image Source: https://www.aclweb.org/anthology/W19-4804v2.pdf

The NaturalProofs Dataset is a large-scale dataset for studying mathematical reasoning in natural language. NaturalProofs consists of roughly 20,000 theorem statements and proofs, 12,500 definitions, and 1,000 additional pages (e.g. axioms, corollaries) derived from ProofWiki, an online compendium of mathematical proofs written by a community of contributors. Source: NaturalProofs

HolStep is a dataset based on higher-order logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies. Source: HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

This relational database consists of 24 unique names in two families (they have equivalent structures). Source: https://archive.ics.uci.edu/ml/datasets/kinship

The official HOList benchmark for automated theorem proving consists of all theorem statements in the core, complex, and flyspeck corpora. The goal of the benchmark is to prove as many theorems as possible in the HOList environment in the order they appear in the database. That is, only theorems that occur before the current theorem are supposed to be used as premises (lemmata) in its proof. Source: HoList Image Source: https://sites.google.com/view/holist/home

Enumerate–Conjecture–Prove: Formally Solving Answer-Construction Problem in Math Competitions We release the ConstructiveBench dataset as part of our Enumerate–Conjecture–Prove (ECP) paper. It enables benchmarking automated reasoning systems on answer-construction math problems using Lean 4. Source Repository: https://github.com/JackSun200312/ECP Description This dataset (constructivebench.json) contains curated Olympiad-style math problems along with metadata and aligned Lean 4 formalizations. Each entry includes: Problem statement Category (e.g., Algebra, Combinatorics) Source (e.g., IMO 2011) Formal answer in Lean Full formal theorem Answer-construction alignment parts (header, answer, theorem, and theorem without answer) Example Entry { "name": "IMO2011SLC4", "category": "Combinatorics", "source": "IMO/2011", "problem": "...", "answer": "The greatest such number k is 3", "formalization": "...", "is_formalized": true, ... }

GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Source: GamePad: A Learning Environment for Theorem Proving