Proof-Pile-2

Proof-Pile-2 is EleutherAI's mathematics pretraining corpus, put together to train the Llemma family of maths language models. It blends three complementary sources into roughly 55 billion tokens: arXiv papers (the scientific preprint archive, rich in maths and physics), OpenWebMath (mathematical text mined from the open web), and AlgebraicStack, a code- focused collection.

AlgebraicStack is what makes it distinctive. It adds around 11 billion tokens of numerical computing, computer algebra systems, and formal mathematics (machine-checkable proofs written in systems such as Lean and Isabelle), so the corpus carries symbolic and code-based maths rather than only prose and LaTeX. That blend is why it suits models expected to manipulate equations and follow formal reasoning, not merely describe it.

The data sits on the Hugging Face Hub as JSONL, so you can stream it with the datasets library or download individual components. For retrieval rather than pretraining, the arXiv and OpenWebMath portions are the practical material, giving you a searchable knowledge base for a maths or science assistant. Chunking needs care here: naive fixed-size splitting will cut through LaTeX expressions and proof steps and wreck their meaning, so split on structural boundaries such as sections and theorem or proof blocks, and keep the maths markup intact.

Two caveats matter. The corpus was built for training, not retrieval, so relative to a curated benchmark it is large and not filtered for quality; filter to your topic before indexing. And the licence varies by subset, because arXiv papers, web text, and code each come with their own terms. Commercial use is not blanket-safe: arXiv content in particular is licensed per paper, so check the components before building on them for a commercial product.

If you want quality scores to filter on, AutoMathText labels similar material for relevance and educational value, and MegaMath is a larger open maths corpus. Reach for Proof-Pile-2 when formal and computational mathematics, not just written maths, is part of what you need to retrieve over.