This Sunday we're hosting Justin Asher, the project leader behind Numina Fuse, an agent-native autoformalization platform for Lean released in beta earlier this year. The official announcement describes Fuse as
a web app that connects to your Lean projects on GitHub integrating an updated version of our Numina-Lean-Agent, allowing users to leverage the agent in the browser to analyze and update their Lean projects.
Unlike an in-editor coding agent, Fuse runs on a sandboxed cloud clone of your repo — working in parallel and for long, unattended stretches — so you can hand off an informal PDF and return to a finished proof. It also generates a TeX blueprint of the project, giving humans a readable map to check the agent's work. Under the hood, Fuse builds on Asher's semantic search engine LeanExplore, and inherits its design goal:
Crucially, the system design facilitates not only more intuitive human engagement with Lean but also the effective integration of its formal capabilities as a powerful tool for artificial intelligence.
Fuse is funded by Project Numina, a nonprofit advancing mathematics through human–AI collaboration. The team has already used it on real formalization targets across pure mathematics and cryptography. Numina Fuse was developed alongside Ruichen Qiu and Yichuan Cao, with additional contributions from Hugues de Saxcé and Junqi Liu. To see it in action, come to his talk this Sunday at Nomadworks Times Square — and please RSVP in advance.