@rohanpaul_ai
The paper built a theorem prover that keeps trying LLM ideas until Isabelle finally accepts a full proof. Isabelle checks formal proofs with strict rules, so its automation often gets stuck when goals need many careful steps. Instead of writing proofs by hand, the prover searches for a script, using an LLM as a guide. Their main trick is a loop where an LLM, suggests the next proof command and Isabelle checks it. To guide those suggestions, the system retrieves a small set of relevant earlier lemmas, meaning previously proved facts, and learns which commands to try first. For longer proofs, a planner asks the LLM for an Isar outline, meaning a readable proof skeleton, then fills gaps by calling the stepwise search again. They run it on consumer laptops and test Isabelle goals where Sledgehammer fails, and the stepwise loop proves some, while the fill and repair part usually stalls. The takeaway is that Isabelle's yes or no feedback can keep the LLM honest, and LLM written code still struggles with the toughest planner pieces. ---- Paper Link ā arxiv. org/abs/2601.04653 Paper Title: "Vibe Coding an LLM-powered Theorem Prover"
