# LeanTool

> "LeanTool: Helping LLMs Be Better at Lean"

"LeanTool: Helping [LLM](https://wiki.g15e.com/pages/Large%20language%20model.txt)s Be Better at [Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt))"

https://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](https://wiki.g15e.com/pages/A%20Proposal%20for%20Safe%20and%20Hallucination-free%20Coding%20AI.txt) to create safe and hallucination-free coding AIs.