Overview
Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore recent advances in mathematical formalization through a conference talk that presents Gauss, a new AI agent designed to assist working mathematicians with formal proof development. Learn about the successful formalization of the Prime Number Theorem in strong form using Lean, which completed a challenge posed by Alex Kontorovich and Terry Tao in January 2024. Discover how this innovative approach aims to make formal mathematics more accessible to mathematicians who don't typically write formal code themselves, potentially bridging the gap between traditional mathematical practice and computer-verified proofs. Gain insights into the current state of autoformalization technology and its potential impact on mathematical research and verification processes.
Syllabus
Jared Duker Lichtman | Gauss – towards autoformalization for the working mathematician
Taught by
Harvard CMSA