formal-math-autoformalization

Formal Math Autoformalization Dataset

A growing, CC0 public-domain corpus of ⟨natural-language statement ↔ Lean 4 statement + proof⟩ pairs, contributed through the Agentic Commons network.

Why this is scarce data. Mathlib already contains millions of proven Lean theorems — but as bare Lean, with no paired natural language:

theorem add_comm (a b : ℕ) : a + b = b + a := ...   -- no "addition on naturals is commutative" attached

The scarce, valuable artifact is the pairing of the human-language statement with a Lean formalization — especially statements not already in Mathlib. Mathlib gives you the Lean half (the answer); this dataset supplies the missing human-language half and ties the two together, with a machine proof that the Lean half is actually a theorem.

• Lean toolchain: leanprover/lean4:v4.30.0
• Mathlib revision: c5ea00351c28e24afc9f0f84379aa41082b1188f
• License: CC0-1.0 (public domain)

What's in it / intended use