You can deploy this model and start earning money today!

adeo1/
mathlib_informal_v4.28.0

Views

No views yet

	mathlib_informal_v4.28.0




	
	Dataset Summary

This dataset contains Lean v4.28.0 mathlib declarations informalized with the repo's external LeanSearch-based pipeline and published in the retrieval schema used by this codebase.

What Is Included

mathlib_informal_v4.28.0.jsonl: one JSON object per declaration dataset_metadata.json: supplemental provenance, schema, and checksum metadata

Cleaning And Normalization

Machine-local paths were removed from the… See the full description on the dataset page: https://huggingface.co/datasets/adeo1/mathlib_informal_v4.28.0.