phanerozoic/

Lean4-Mathlib

Structured dataset of mathematical formalizations from the Mathlib4 library for Lean 4.

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.