Terence Tao at IMO 2024: AI and Mathematics

Introduction to Professor Terence Tao

Background of Terence Tao

• Professor Terence Tao began participating in the International Mathematical Olympiad (IMO) at age 11, earning a bronze medal.

• He won a silver medal the following year and became the youngest gold medalist at age 13.

• Currently, he is a professor at UCLA and recognized as one of the most influential mathematicians today.

The Importance of IMO Experience

Reflections on IMO

• Tao expresses joy about returning to the IMO, recalling it as one of his most enjoyable experiences.

• He emphasizes that competition is not just about scores but also about social interactions and events organized during the IMO.

AI's Role in Mathematics

Introduction to AI in Math

• The talk focuses on AI and machine assistance in mathematics, highlighting its transformative potential.

• Mention of DeepMind's AlphaGeometry tool that can solve certain geometry problems from past IMOs.

Differences Between Research and Competition Mathematics

• Research mathematics differs significantly from competition math; research often takes months with no guaranteed solutions.

• Despite differences, there are overlapping skills between competition math and research.

Historical Context of Machines in Mathematics

Evolution of Computational Tools

• Machines have been used for mathematical computations for thousands of years, starting with simple tools like the abacus.

• The use of computers dates back around 300–400 years; however, modern electronic computers emerged only in the 1930s and 1940s.

Human Computers

• During WWII, women known as "computers" performed calculations manually while men were away fighting.

• Early computational tasks included generating logarithm tables which were essential before calculators became common.

Tables and Databases in Mathematical Research

Significance of Tables

• Even today, mathematicians rely on databases akin to historical tables for research purposes.

• Important results like the prime number theorem were conjectured based on patterns found through extensive table computations by mathematicians like Gauss.

Modern Resources: OEIS

• The Online Encyclopedia of Integer Sequences (OEIS), a vital resource for identifying integer sequences related to various mathematical problems.

Scientific Computation and Its Evolution

The Origins of Scientific Computation

• Scientific computation, often associated with number crunching, has been utilized since the 1920s for large calculations.

• Hendrik Lorentz was a pioneer in scientific computation, tasked by the Dutch to model fluid equations for a giant dyke project using human computers.

• He invented floating point arithmetic to represent numbers of varying magnitudes efficiently.

Applications of Scientific Computation

• Modern scientific computation can solve complex problems like linear equations, partial differential equations, and combinatorial calculations.

• Algebra packages such as Sage or Maple can convert geometry problems into systems of equations but face challenges with complexity as problem size increases.

Advances in Problem Solving Techniques

• SAT solvers are powerful tools designed to tackle logic puzzles involving true/false statements and constraints.

• SMT solvers extend SAT solving capabilities by incorporating theories and laws (e.g., commutativity of addition), but they also struggle with scalability.

Notable Achievements in Computational Mathematics

• A significant achievement involved solving the Pythagorean triple problem using computer SAT solvers, proving that one color must contain a Pythagorean triple when coloring natural numbers.

• The proof required extensive computation over several years and resulted in a proof certificate that was initially 200 terabytes long but later compressed to 86 gigabytes.

Innovative Uses of Computers in Mathematics

• Recent advancements include using machine learning neural networks to uncover new mathematical connections that humans might overlook.

• Large language models (like ChatGPT) generate potential solutions to mathematical problems, showcasing their utility despite variable success rates.

Modern Proof Assistants in Mathematics

The Evolution of Proof Assistants

• Recent advancements have made proof assistants easier to use, facilitating complex mathematical projects that were previously unfeasible.

• The Four Color Theorem, proven in 1976, is highlighted as one of the first significant computer-assisted proofs, combining human and computational efforts.

Historical Context of the Four Color Theorem

• The original proof involved extensive computation and manual verification by humans, marking it as a hybrid approach rather than a fully computer-based proof.

• A list of 1,000-2,000 special subgraphs was created to check properties like dischargeability and reducibility for each graph configuration.

Challenges Faced in Early Proof Verification

• Manual checks were tedious; early computers required inputting graphs by hand, leading to potential errors and necessitating updates.

• A more streamlined proof emerged in the '90s with fewer graphs (around 700), allowing for quicker verification through modern programming languages.

Advancements in Computer-Assisted Proofs

• In 2005, a complete verification down to mathematical axioms was achieved using Coq (now Rooster), showcasing significant progress from earlier methods.

The Kepler Conjecture: Sphere Packing

Overview of the Kepler Conjecture

• Proposed by Johannes Kepler in the 17th century, this conjecture addresses optimal sphere packing in three-dimensional space.

• Two primary packing strategies are discussed: triangular packing (like oranges at a grocery store) and cubic packing.

Complexity of Proving Sphere Packing Efficiency

• Proving optimal density for sphere packing is surprisingly difficult; only recently has progress been made in higher dimensions (8 and 24).

Strategies for Tackling Sphere Packing Problems

• Toth's strategy from the '50s involves subdividing space into Voronoi regions to analyze volume relationships among spheres.

Attempts at Proving the Conjecture

Understanding the Complexity of Mathematical Proofs

The Challenge of Linear Inequalities

• The aim is to create linear inequalities between different scores to establish upper bounds for density, ultimately seeking the optimal density. However, this method's flexibility can lead to complications due to numerous possible setups.

• Sam Ferguson noted that whenever he faced challenges in minimizing his functional, he would change the scoring function and retry. This led to a cycle of re-evaluation and increased complexity in their scoring functions.

Complications Over Time

• Over nearly a decade, the scoring function evolved into something more complex, resulting in significant time savings but also causing friction with colleagues due to constant changes presented at conferences.

• In 1998, they announced finding a score that adhered to multiple linear inequalities across 150 variables. Initially not intended as a computer-assisted proof, it became necessary due to increasing complexity.

Publication Challenges

• The proof was extensive by 1998 standards—250 pages and three gigabytes of data—which made it difficult to referee. It took four years with twelve referees concluding they were 99% certain about its correctness but could not certify all computer calculations.

• An unusual decision was made: the paper was published with an editor's caveat regarding its verification status. At that time, there was considerable debate over whether computer-assisted proofs qualified as legitimate proofs.

Formalization Efforts

• This case marked a pivotal moment for formalizing mathematical proofs down to first principles using formal proof languages. Hales initiated the Flyspeck project aimed at achieving this level of rigor.

• Although Hales estimated it would take 20 years for formalization, collaboration with 21 others allowed completion in just 12 years; the results were published in 2014.

Advancements in Formalization Techniques

• Recent years have seen improvements in workflows for formalizing proofs, though still tedious. Peter Scholze has contributed significantly through condensed mathematics—a blend of algebra and category theory applied to functional analysis.

• Condensed mathematics aims to address questions within functional analysis using algebraic methods by establishing new categories like condensed abelian groups and vector spaces.

Foundational Importance of Key Theorems

• A crucial vanishing theorem needed proof for condensed mathematics' foundation; Scholze spent a year obsessing over it without anyone daring to scrutinize its details fully.

• He expressed concerns about being only "99.9% sure" regarding this theorem's correctness since its validation is essential for applying condensed formalism effectively within functional analysis contexts.

Modern Proof Assistants

• To ensure accuracy, Scholze sought formalization using Lean—a modern proof assistant language supported by a crowdsourced math library containing many pre-proven intermediate results from undergraduate-level courses onward.

Mathematical Formalization and Collaborative Proofs

The Incompleteness of Mathematical Libraries

• The mathematical library is still incomplete, lacking areas such as homological algebra, sheaf theory, and topos theory. However, a significant theorem was formalized in 18 months with mostly correct proofs and minor technical issues.

Enhancements to Lean's Math Library

• The project greatly expanded Lean's math library, improving its capability to handle abstract algebra. Additionally, supporting software was developed for future formalization projects.

Blueprint Methodology for Proof Formalization

• A new workflow called "blueprint" was introduced to simplify the formalization of large proofs by breaking them into smaller steps that can be tackled individually.

• This approach allows team members to work on different parts of the proof simultaneously, enhancing collaboration and efficiency.

Human-Readable Proof Generation

• Efforts are underway to convert formal proofs back into human-readable formats. Tools have been developed that allow users to interactively explore these proofs.

• An example shows how a topological problem's proof can be generated from a formal proof in Lean, maintaining an interactive format for better understanding.

Future of Textbooks and Collaborative Projects

• The speaker envisions future textbooks being written in an interactive style where formalized content is presented alongside user-friendly explanations.

• A recent combinatorial problem was solved collaboratively using the blueprint method within three weeks by a group of about 20 people, showcasing the effectiveness of this approach.

Dependency Graph for Task Management

• A dependency graph illustrates how various statements depend on one another within the proof structure. Each bubble represents a statement with color coding indicating its status (formalized or not).

Expanding Collaboration Beyond Traditional Boundaries

• This collaborative model allowed contributions from individuals outside traditional mathematics backgrounds, including computer programmers who excelled at solving specific tasks.

Trust Through Automated Verification

• Unlike typical collaborations limited by trust issues among mathematicians, this project utilized Lean’s compiler which automatically checks correctness before allowing submissions.

Decoupling Mathematical Proofs

The Future of Mathematics

• The process of proving mathematical concepts is evolving, allowing for specialization in different skills. Some individuals can focus on the big picture while others work on smaller components without needing extensive mathematical knowledge.

• Despite advancements, formalizing proofs remains challenging and time-consuming, often taking ten times longer than traditional methods due to the need for programming expertise.

Efficiency in Formal Proofs

• Changing established proofs can be streamlined through formalization; a recent example involved updating a theorem from 12 to 11, which was accomplished quickly with targeted fixes rather than rewriting the entire proof.

• Significant projects are underway in proof formalization, such as Kevin Buzzard's initiative to formalize Fermat's Last Theorem using Lean, projected to take five years for key parts.

Machine Learning Applications in Mathematics

Introduction to Machine Learning

• Machine learning employs neural networks to predict answers across various domains. One notable application is its use in knot theory.

Understanding Knot Theory

• Knot theory studies loops or curves in space that can be deformed into one another without crossing themselves. Key questions involve determining when two knots are equivalent.

• Knot invariants are essential tools used to classify knots; these include numerical values or polynomials that remain unchanged under continuous deformation.

Types of Knot Invariants

• Various types of knot invariants exist:

• Signature counts crossings and their arrangement.

• Famous polynomials like the Jones and Alexander polynomials connect multiple mathematical fields.

• Hyperbolic invariants arise from geometric properties associated with knots.

Linking Different Approaches Through Machine Learning

Discovering Connections Between Invariants

• Researchers have recently utilized machine learning to explore connections between combinatorial and geometric invariants of knots by creating databases containing millions of examples.

Neural Network Insights

• After training a neural network on this data, it could accurately predict signatures based on hyperbolic geometry invariants about 90% of the time, revealing hidden relationships between these concepts.

Saliency Analysis Findings

Understanding the Role of Machine Learning in Mathematics

The Use of Neural Networks in Mathematical Conjectures

• Researchers utilized a human network to identify patterns through graph analysis, leading to conjectures about mathematical phenomena.

• Initial conjectures were proven incorrect using neural networks, which facilitated the correction and eventual proof of a new conjecture explaining specific statistics.

Machine Learning's Contribution to Problem Solving

• Machine learning aids in mathematics by providing hints and connections, but human insight is still essential for making final connections.

• Large language models (LLMs), like GPT-4, have gained attention for their capabilities; they can solve simplified math Olympiad questions but often struggle with complex problems.

Performance of AI on Mathematical Problems

• Despite successfully solving one IMO question, LLMs had only a 1% success rate across various similar problems due to cherry-picked examples.

• AI excels at tasks humans find difficult but struggles with simpler tasks; this highlights an orthogonal approach to problem-solving.

Limitations and Challenges of AI Models

• An example showed that when asked basic arithmetic, an LLM provided an incorrect answer initially but corrected itself after further processing.

• Current models rely on guessing rather than first principles; ongoing efforts aim to improve accuracy through various methods.

Enhancing AI Capabilities for Mathematical Proofs

• Strategies include connecting LLMs with reliable software or teaching them problem-solving techniques used in math competitions.

• While progress is being made, LLM performance remains insufficient for most math Olympiad or research problems.

Practical Applications of AI as a Collaborative Tool

• Users have found value in conversing with LLMs for brainstorming techniques; while not perfect, they can suggest useful approaches previously overlooked.

Advancements in Proof Assistance Tools

• Tools like GitHub Copilot assist in writing formal proofs by predicting subsequent lines based on user input.

AI in Mathematics: Current State and Future Prospects

The Role of AI in Proving Mathematical Theorems

• AI is currently being used to suggest proofs, which are then verified by compilers. This method has shown success with short proofs (4-5 lines), but larger proofs (tens of thousands of lines) remain challenging.

• There is optimism about using computers to solve math problems directly in the future, though current AI applications are limited to narrow problem domains and lack full reliability.

• For the foreseeable future, AI will serve as a useful assistant rather than a complete solution for mathematical problems, enhancing traditional computational methods.

Generating Conjectures and Exploring Problem Spaces

• A promising direction for AI is its potential to generate good conjectures from large datasets, although this capability has not yet been fully realized due to the absence of massive datasets.

• The vision includes solving classes of similar problems simultaneously rather than one at a time. This could revolutionize how mathematicians explore problem spaces and techniques.

• With advanced tools, mathematicians could efficiently analyze numerous related problems, significantly speeding up the discovery process compared to traditional methods that take decades.

Future Implications for Mathematics

• While traditional theorem proving will continue alongside AI advancements, understanding foundational concepts will be essential for guiding AI effectively in mathematical exploration.

Discussion on Formalizing Mathematics

• A question arises regarding Voevodsky's work on homotopy type theory after his concerns about abstract proofs' verifiability.

• Voevodsky proposed changing mathematics' foundations through homotopy type theory, which allows many proven statements to remain valid even if axioms change.

• There are various proof assistant languages available; however, automatic translation between these languages remains an area where AI could provide significant assistance.

Personal Reflections on Education Pathways

• The speaker reflects on their early university experience at age 13 and emphasizes that educational paths should be personalized rather than dictated by age or external expectations.

Choosing Research Topics in Mathematics

The Process of Selecting Research Problems

• The speaker reflects on their early career, noting that they had advisers who suggested problems to tackle. However, the current approach is more spontaneous and influenced by social interactions within the mathematical community.

• Attending math conferences plays a crucial role in discovering new research questions. The speaker mentions an upcoming conference in Edinburgh where they anticipate engaging discussions related to the PFR conjecture.

• While there are long-term projects of interest, many research questions arise unexpectedly through conversations with other mathematicians. This highlights the dynamic nature of mathematical inquiry.