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: 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. - Autoformalization (NL → Lean 4): each row is a worked NL→Lean example…