A Lean Lunch

​A Lean Lunch is an informal gathering for people working in AI-driven mathematics, including formalization in mathematics and other disciplines.

​We’re bringing together a small group of researchers and builders to talk about the role of formal systems in science. How are proof assistants changing the way we do research? What can a formal proof tell us, and what still depends on the definitions, assumptions, and models we choose? We’re especially interested in applications beyond pure mathematics, from physics to law.

​Come share what you’re working on, swap ideas, and meet others thinking about these questions. Bring a problem, a project, or just your curiosity. Lunch and beverages will be provided. We’ll also have projectors available for anyone who’d like to give a short talk about a passion project. Stay as long as you’d like.

​Saturday, November 21, 2026 · 12 pm–3 pm
Chinatown, Manhattan

​We’re keeping the gathering small. Please request a place on the list and tell us a little about your affiliation and your involvement with formalization. Registration requires host approval.

​Sponsored by Magic State Labs, a research lab hunting for discoveries in quantum physics.

​