FrenzyMath/mathlib_informal_v4.16.0 download history

FrenzyMath/mathlib_informal_v4.16.0 is a translation dataset on the Hugging Face Hub. In the last 30 days it was downloaded 48 times (15 in the last 7 days), and 1,821 times in total. It ranks #191,560 among datasets by monthly downloads.

Notes Names All names in Lean (names of symbols and modules) are stored as their raw form (list[int | str]) instead of the usual pretty-printed form to avoid problems arising from quoting/unquoting. For example, instead of "Lean.«binderTerm∉_»" we have ["Lean", "binderTerm∉_"].

Open FrenzyMath/mathlib_informal_v4.16.0 on Hugging Face

Sister project: Paper Pulse, the upvote history of every Hugging Face Daily Paper.