Text Classification
Transformers
Safetensors
English
modernbert
lean
lean4
theorem-proving
formal-verification
encoder
text-embeddings-inference
Instructions to use EPFL-LARA/lean-encoder-modernbert-large with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Transformers
How to use EPFL-LARA/lean-encoder-modernbert-large with Transformers:
# Use a pipeline as a high-level helper from transformers import pipeline pipe = pipeline("text-classification", model="EPFL-LARA/lean-encoder-modernbert-large")# pip install -U transformers accelerate # Load model directly from transformers import AutoTokenizer, AutoModelForSequenceClassification tokenizer = AutoTokenizer.from_pretrained("EPFL-LARA/lean-encoder-modernbert-large") model = AutoModelForSequenceClassification.from_pretrained("EPFL-LARA/lean-encoder-modernbert-large", device_map="auto") - Notebooks
- Google Colab
- Kaggle
Download Example.lean from EPFL-LARA/lean-encoder-modernbert-large: direct link, hf CLI and curl.
- Browser
- Download file 80 Bytes
-
https://huggingface.co/EPFL-LARA/lean-encoder-modernbert-large/resolve/main/Example.lean
- Command line
-
hf download hf://EPFL-LARA/lean-encoder-modernbert-large/Example.lean
-
curl -L -o Example.lean https://huggingface.co/EPFL-LARA/lean-encoder-modernbert-large/resolve/main/Example.lean
80 Bytes
| import Mathlib | |
| theorem nat_add_zero_identity (n : ℕ) : n + 0 = n := by | |
| rfl | |