Hugging Face's logo
Activity Feed

AI & ML interests

AI for mathematics, including formal mathematics and theorem proving in Lean, and AI for verified software engineering.

Recent Activity
Lemmy00  updated a model 3 days ago
EPFL-LARA/lean-feedback-qwen3-4b
Lemmy00  updated a model 3 days ago
EPFL-LARA/lean-one-token-qwen3-8b
Lemmy00  updated a model 3 days ago
EPFL-LARA/lean-encoder-modernbert-large
View all activity

EPFL-LARA 's collections 2

Formal Theorem Proving with Lean World Models
Models and datasets for Formal Theorem Proving with Lean World Models: continued pretraining, proof repair, GRPO, and informal reasoning.
Learning Lean Feedback
Companion resources for "Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs": three models and two datasets.
Formal Theorem Proving with Lean World Models
Models and datasets for Formal Theorem Proving with Lean World Models: continued pretraining, proof repair, GRPO, and informal reasoning.
Learning Lean Feedback
Companion resources for "Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs": three models and two datasets.