Formal proofs
Hi,
Is the model able to generate formal proofs in the Lean 4 language, or use tools (like a Python REPL tool) ?
Thanks
Hi!
The model was trained to produce proofs in natural language, not Lean (or any other formal language).
While the base model (Qwen3-4B-Think) supports tool-use, we did not do any finetuning with tool calls. The model might have therefore lost its ability to make effective use of tools.
Hi, it might be interesting though to connect it to our UlamAI Prover via Ollama which uses LLM - LeanDojo loop to formalize mathematics from .tex - https://github.com/ulamai/ulamai -- I'm happy to collab more on the integration because it genuinely seems like something that can run locally.
QED-Nano itself is not really perfectly suited for this; as mentioned above, it lacks Lean and tool-calling capabilities. It is therefore unlikely it knows (1) enough syntax to produce correct Lean, (2) is able to bridge the significant gap between natural language and formal proofs when attempting autoformalization, and (3) interact with the provided tools in a meaningful way.
We are currently not (yet) looking at creating a model that can do those things, instead focusing on improving our model for natural language theorem proving.