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
File size: 80 Bytes
1b6fcc6 | 1 2 3 4 5 | import Mathlib
theorem nat_add_zero_identity (n : ℕ) : n + 0 = n := by
rfl
|