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 NumberTheorem in strong form, completing a challenge set in January 2024 by Alex Kontorovich and Terence Tao. We hope Gauss will help assist working mathematicians, especially those who do not write formal code themselves.