phanerozoic/Lean4-Mathlib

Lean4-Mathlib Structured dataset of mathematical formalizations from the Mathlib4 library for Lean 4. Source Repository: https://github.com/leanprover-community/mathlib4 Commit: b9f14353520df73472ae3825fb53f86559a01319 Files: 8170 License: apache-2.0 Schema Column Type Description statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof proof string Verbatim… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Mathlib.

<iframe src="https://silytics.si/embed/item/e8f5811b-89d6-4d0c-b4c8-93a291636814" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.