Asher et al. built Numina Fuse as an environment where a human user works alongside an AI orchestrator on a Lean 4 project.
Lean 4 formalization tool shifts from human supervision to autonomous agent orchestration
The authors show how Numina Fuse moved from a human-paced agent pipeline to an orchestrator that dispatches specialists and parallel provers during a Kakeya conjecture formalization.
Research Lab
Justin Asher · Yichuan Cao · Ruichen Qiu · Pietro Pellegrino · Jia Li
Project Numina · University of Naples Federico II · Academy of Mathematics and Systems Science · University of Chinese Academy of Sciences
Research Digest··3 min read
The authors present Numina Fuse, an agent-native application that formalizes mathematics in Lean 4 under human supervision.
The Daily Edition
The front page in your inbox each weekday morning: the lead, the picks, and why each one earned its place.