Skip to content
RAG Repo

Proof-Pile-2

Proof-Pile-2 pulls together three complementary sources into a single maths pretraining corpus: arXiv papers, the web text of OpenWebMath, and AlgebraicStack, a code-heavy collection focused on mathematical computation. Together they total roughly 55 billion tokens.

AlgebraicStack is the distinctive part. It contributes about 11 billion tokens covering numerical computing, computer algebra systems, and formal mathematics (machine-checkable proofs), which makes the corpus useful for models that need to reason about symbolic maths and code, not just prose.

The dataset is hosted on Hugging Face by EleutherAI and was assembled for training the Llemma family of maths language models. Licensing varies by subset, so check the terms of each component before building on it commercially.

mathematicsarxivformal-mathematicspretrainingscientific

Related sources