Lean

Formal Verification for LLM Reasoning: Solvers and Theorem Provers

How solvers and proof assistants check LLM reasoning: solver feedback on partial programs, formal logic checks inside a chain of thought, and LLM theorem provers for Lean, Isabelle and Coq that retrieve, search, repair and learn from the checker.