LeanTool feature: Sorry Hammer

Stream: Machine Learning for Theorem Proving

[GasStationManager]

I have always been a fan of the Draft-Sketch-Prove approach, and LeanTool's system messages and features generally encourage the LLMs to decompose the proof task by starting with a proof sketch, and getting the goals from the sorrys (thanks for Pantograph's load_sorry). What had been missing was a good hammer tactic that can help solve some of the smaller goals.
That's changed lately with the recent release of LeanHammer, and other tools including Canonical, egg, grind etc coming along.

To help facilitate the use of hammers by LLMs, I have added the following (very experimental) "Sorry Hammer" feature to LeanTool: if the LLM passes a Lean source code with sorrys to the tool, and choose to activate the sorry_hammer option of the tool call, then the tool will try to replace the first sorry with a hammer tactic. By default it is hammer from LeanHammer, but this is configurable, and can even be a list of tactics to try one by one (the list is converted to first | tac_1 | tac_2 | ..).

LeanTool allows the LLM to iteratively refine its proof attempt: if the hammer fails, it can go back to the drawing board and try replacing the sorry with a more fine-grained proof sketch. (Right now you might need to prompt the LLMs; but if you find a prompt that works well, let me know and I can add it to the system prompt!)

You can try it out by installing LeanTool, or trying out its API server (by pointing your coding assistant to http://www.codeproofarena.com:8800/v1 as the base URL.)

Let me know how it goes! Feature requests welcome.

• what combination of tactics tend to work best as hammer for your use case?
• rewriting with the proof from the Try this suggestion: for now you can prompt the LLM to do it. One could try to automate this...

[Bas Spitters]

This is exciting! It seems similar functionality is available in Jetbrains RocqStar (for Rocq) https://arxiv.org/pdf/2505.22846
However, LeanTool makes it more convenient to give specific hints about what tactics to use.