An agentic proof system called LAMP just verified 96.7% of theorems in a niche branch of mathematics that existing tools largely ignore.
Researchers built LAMP to tackle Combinatorics on Words, a field studying sequence properties like periodicity, borders, and morphisms that is underrepresented in Mathlib, the main repository of formalized Lean 4 math. Rather than fine-tune a model on new data, LAMP coordinates three agents — Planner, Builder, and Verifier — that access a domain-specific ontology at inference time via the Model Context Protocol. The team also published a new Lean 4 formalization of the field, covering 93 definitions and lemmas across eight modules. Together, the two contributions give the framework something to work with that simply did not exist before.
The 96.7% success rate on a 90-theorem benchmark matters because it comes without any weight updates to the underlying model — meaning the approach is portable to other underrepresented domains without expensive retraining. Ablation tests are the honest part: strip out the tool-grounded architecture or collapse the Planner-Builder split and performance drops roughly 12 percentage points each, isolating exactly where the gains come from.
Formal verification has long been bottlenecked by the gap between what provers can check and what mathematicians actually study; LAMP's ontology-injection trick is a plausible wedge into that gap, though how far it scales beyond carefully curated niche domains remains the open question.