Formal proofs
#2
by
catalin-hanga
- opened
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.