Formal Commons
Advances in AI put the frontier of mathematical research within reach of formalization.
This small workshop will discuss the Formal Commons project, which aims to curate a comprehensive formal foundation for contemporary research mathematics built on Lean's Mathlib. The project will draw on existing projects like Tau Ceti and Formal Frontier and will enlist the help of mathematics research institutes to involve the entire mathematics research community.
This meeting was sponsored by the Hoskinson Center for Formal Mathematics at Carnegie Mellon University.