LeanAssist is an open source proof assistant for the Lean theorem prover. It uses large language models to suggest tactics and help users complete formal proofs inside Lean.
We built a proof search algorithm in Python that can test any large language model on the LeanDojo datasets. It uses OpenRouter and Fireworks so it is easy to swap between different models.
We wrote a tool that turns LeanDojo theorem data into simple question and answer style conversations. These conversations can be used directly for training models on theorem proving.
We updated LeanCopilot so it can call any model through one shared interface. A user can register a new model with a small change in the configuration and then use it to get tactic suggestions in their editor.
We tested DeepSeek V3.2 on 100 theorems from each LeanDojo Lean 4 test set. On the random split it solved about one quarter of the problems and on the harder novel premises split it solved a similar number of problems as the ReProver model.
We also fine tuned a smaller model called Qwen3 8B on a custom dataset that we generated from LeanDojo. This run showed that our tools for building datasets and training models work correctly and are ready for larger experiments when more resources are available.