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… See the full description on the dataset page:
https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization.
