LeanTool

“LeanTool: Helping LLMs Be Better at Lean”

github.com/alok/LeanTool

LeanTool is a simple utility that connects LLMs with a “Code Interpreter” for Lean. This is implemented as tool calls from the LLM to the Lean executable, hence the name. … This is part of a a broader effort to create safe and hallucination-free coding AIs.