Lean in Munich meetup

​What happens to mathematics, when AI starts proving theorems?

​Kevin Buzzard started a multi-year effort to formalize Andrew Wile's proof of Fermat's last theorem. Until a team of Anthropic researchers were able to use AI-agents to achieve that goal in merely 11 days.

​Kevin is personally cited in Anthropic's announcement of the formalization success.

​We thank AWS for their generosity in hosting us.

​Please note that in order to access the venue it is required to sign up with your first and last name, company, and position.

​Please bring a government photo ID to enter the venue.