Gauss - an agentic formalization of the Prime Number Theorem

Abstract: In this talk we'll highlight some recent formalization advances using a new agent, Gauss. In particular, with Gauss we obtained a Lean proof of the Prime Number Theorem in strong form, completing a challenge set in January 2024 by Alex Kontorovich and Terry Tao. We hope Gauss will help assist working mathematicians, especially those who do not write formal code themselves.

algebraic geometrynumber theory

Audience: researchers in the topic

Comments: Note the unusual day/time/place!

---

MIT number theory seminar

Series comments: To receive announcements by email, add yourself to the nt mailing list.

Past semesters

---