NaturalProofs

NaturalProofs assembles mathematical knowledge in the form that mathematicians actually write it: theorem statements paired with their proofs, in natural language mixed with LaTeX rather than a machine-checkable formal language. It contains around 32,000 theorem-and-proof pairs, 14,000 definitions, and 2,000 further pages such as axioms and corollaries.

The material is drawn from three places: ProofWiki, a community encyclopaedia of mathematical proofs; the Stacks Project, a large collaborative reference in algebraic geometry; and a set of mathematics textbooks. Crucially, the pages are linked by their references, so the data doubles as a small knowledge graph of how one result depends on another. It ships as JSON from the GitHub repository, with the processing scripts included, and a companion release (NaturalProofs-Gen) reframes the same material for proof generation.

For RAG, the natural task is reference retrieval: given a theorem or a claim, retrieve the definitions and prior theorems its proof relies on. That makes it a strong fit for a mathematical assistant that needs to ground an explanation in cited results, or for evaluating whether your retriever understands mathematical text, where surface word overlap is often misleading. You can embed each statement and definition as its own record and use the reference links as ground-truth relevance labels.

The caveats are about form and licence. The proofs are human-written prose, not formally verified, so this is not the resource for training a theorem prover in Lean or Coq; it is about mathematical language and structure. On rights, the processing code is MIT licensed, but the underlying content keeps the licences of its original sources, which vary (ProofWiki is share-alike, for example), so check each source's terms before reusing the text commercially. Alongside AMPS and the MATH dataset, which lean towards problems and solutions, NaturalProofs is the reference-and-proof corpus, better suited to retrieval than to drilling worked exercises.