1 Potential AI Assistance in Science and Mathematics

In a recent XTX-sponsored conference speech, renowned mathematician and a Fields medalist Terrence Tao stated that AI can accelerate the proof of mathematical theorems, particularly when combined with proof assistants like Lean. Proof assistants are computer languages designed to verify mathematical statements and create certificates of correctness. However, formalizing proofs using these languages is currently time-consuming, often taking mathematicians several months for even medium-sized problems.

• Tao believes AI can automate parts of the formalization process, leading to faster proof writing than traditional methods. He envisions a future where mathematicians dictate proofs to AI, which then formally verifies each step, creating a more efficient and collaborative approach to mathematical research.

• Tao used his own experience formalizing a combinatorics theorem as an example of AI's potential in this area. Using a tool called GitHub Copilot, he found that the AI could suggest correct Lean code for parts of the proof, highlighting the potential for automating these tasks.

• Formalization offers several benefits for mathematics: (1) Guarantees of correctness. (2) Enhanced collaboration by breaking down proofs into smaller, verifiable components. (3) Integration of AI into mathematical research with higher confidence in the results.

• Tao argues that formalization will likely become standard practice in mathematical publishing, enabling referees to focus on the significance of results rather than verifying every line of a proof. He also suggests that funding agencies may need to develop new metrics to assess the contributions of mathematicians involved in large-scale formalization projects.