Anyone here using Lean 4 with LLMs/math AIs? Not sure if to post this in the math thread, technology, or advice.I’m trying to figure out the best workflow for getting an AI to solve math problems and produce/check Lean 4 proofs, instead of just giving a normal natural-language solution that might be wrong.Questions:- What models/tools are actually good with Lean 4 right now?- Do people use ChatGPT/Claude/Gemini + a local Lean install, or is there a better setup?- Is Mathlib required for most contest/undergrad-style problems?- What’s the best way to prompt the AI so it writes valid Lean code instead of fake theorem names?- Are there any good examples/repos where an AI iterates with Lean errors until the proof compiles?Basically I want a setup where I can give it a problem, have it formalize the statement, try a proof, run Lean, read the errors, and keep fixing it until it works.Any advice, examples, or workflows appreciated.
damn nigga math hittin dat lean now? fr that shit wild
>>17002647Claude's Fable 5.
>>17002647>run Lean, read the errors, and keep fixing it until it works.Lean is the wrong system for that workflow. Use Idris instead, the type system is actually designed for interactive proof development:https://idris-community.github.io/idris2-tutorial/Tutorial/Functions2/Holes.html
the tool to use is codex cli or claude codethe loop you can vibe code using the same tooljust ask it to make a script that will check the lean file for errors and if any found then prompt your codex with "plz fix errorinos king make no mistakes this time over"without the scripted loop it will give up after some time
