Terence Tao, "Machine Assisted Proof"

Briana C, president of the AMS, warmly welcomes the audience to the colloquium lectures, a prestigious series dating back to 1895. She highlights the historical significance of the lectures and their notable speakers, including Stein Ilia. The introduction focuses on the remarkable achievements of Terry Tao, a mathematician with numerous awards, including the Fields Medal and a MacArthur Fellowship, and his extensive contributions to mathematics through publications and collaborations. Briana shares a personal anecdote about Terry's engagement with technology and data during the 2008 election night, emphasizing his multifaceted personality.

The speaker delves into the historical use of 'computers' in mathematics, initially referring to human calculators, and later mechanical and electronic devices. The development of logarithmic tables by Napier is cited as an early example of computer-assisted mathematics. The speaker discusses the evolution to modern computational tools used for creating large data tables, like the Online Encyclopedia of Integer Sequences (OEIS), and the use of these tools in experimental mathematics and number theory. The narrative then shifts to the application of computers in numerics and scientific computing, mentioning the use of interval arithmetic for more rigorous computations and the advent of SAT solvers and SMT solvers for complex problem-solving.

The speaker presents a specific application of SAT solvers in mathematics, focusing on the Boolean Pythagorean triples problem from Korea. The problem involves coloring natural numbers in such a way that one color class always contains a Pythagorean triple. Initially, a massive computation was conducted to prove this up to a certain number, but it was later formalized using a SAT solver, resulting in the world's longest proof at the time. The proof certificate, although large, provided a verifiable proof, highlighting the potential of computer-assisted proofs in mathematics.

The speaker discusses the recent developments in using machine learning algorithms and large language models like GPT in mathematics. While these models have not been directly tailored for mathematical tasks, they have shown potential in suggesting proof techniques and related literature. The speaker also mentions the use of formal proof assistants, which are designed to verify mathematical proofs and can also be used to verify the output of large language models, thus combining the strengths of both technologies.

The speaker recounts the history of the Four Color Theorem, from its initial proof in 1976 to its formalization in proof assistant languages in the early 2000s. The process of formalization is highlighted as a way to ensure the correctness of complex proofs, with the speaker sharing the story of the proof's formalization in the Lean proof assistant, which involved creating a blueprint of the proof and then translating it into a formal language.

The speaker introduces Peter Scholze's work on condensed mathematics and the challenges faced in formalizing a key theorem within this theory. The need for formalization arose from the desire to ensure the correctness of the theorem, which is fundamental to the application of condensed mathematics to functional analysis. The process involved a collaborative effort, similar to the Kepler experiment, and highlighted the importance of having foundational theories already formalized in proof assistants.

The speaker reflects on the benefits of formalizing mathematical proofs, including the ability to collaborate on a large scale, the discovery of errors, and the simplification of proofs. The process of formalization is shown to be a community effort, with many contributors working on individual parts of a proof. The speaker also discusses the potential of formalization to make mathematics more accessible and to facilitate the exploration of theorem spaces.

The speaker concludes by discussing the potential impact of AI and technology on the future of mathematics. They foresee a time when proof formalization may become faster than traditional proof writing, leading to a tipping point where mathematicians might routinely use these tools. The speaker also speculates on the possibility of AI-generated conjectures and the exploration of mathematical spaces, as well as the role of large language models in assisting mathematicians in understanding complex topics.

The session concludes with a Q&A where the speaker addresses concerns about the proliferation of formally verifiable proofs that may be incomprehensible to humans. He suggests that computer-generated proofs can still be analyzed and translated into human-understandable forms. The speaker also discusses the role of human intuition in proof generation and the potential for AI to automate this aspect of mathematics in the future, although he acknowledges that current AI models are not yet capable of distinguishing good ideas from bad ones.