Researchers have built a planning system that proves its AI-generated heuristics never cheat, which means the plans it finds are guaranteed optimal.
The system, called LeanPlan, pairs large language model generated heuristics with machine-checked admissibility proofs written in Lean 4. An agentic loop built around GPT-5.6 Sol iteratively refines a domain-specific heuristic, its proof, and its required assumptions using feedback from the planner itself. The researchers tested LeanPlan on ten domains from the International Planning Competition plus three new ones, using test tasks with up to 57 times as many objects as the training tasks. For every domain tried, the loop produced a heuristic with a machine-checked admissibility proof.
That matters because admissibility is the property that keeps a heuristic from overestimating cost, the thing that actually guarantees a planner's answer is optimal rather than just good looking. LLM-written heuristics have gotten fast at finding workable plans, but fast and provably correct are different claims, and this is the first system to make the latter one checkable by machine rather than taken on faith.
Per the paper, LeanPlan usually expands fewer states than the established Scorpion planner and solves more tasks overall. Usually, not always, and the comparison is the authors' own. Formal methods meeting LLM output is a trend worth watching, but one admissibility proof pipeline doesn't yet mean planning has solved its trust problem.