l3lab/lean-premises download history

l3lab/lean-premises is a dataset on the Hugging Face Hub. In the last 30 days it was downloaded 121 times (36 in the last 7 days), and 2,630 times in total. It ranks #99,329 among datasets by monthly downloads.

This dataset stores the premises extracted from Mathlib, Batteries, and Lean core. It also stores the pre-computed embeddings for these premises embedded by some trained models. This dataset is intended to be used for the premise selection server. Please see the appropriate branch according to the L

Open l3lab/lean-premises on Hugging Face

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