A machine has verified the maths that won a Fields Medal: why it matters, Pg13

Key Highlights:

• Mathematicians have achieved a milestone in verifying the solution to the sphere-packing problem, for which Maryna Viazovska won the Fields Medal in 2022.
• The team has a proof that a machine has fully verified the solution to the problem of packing spheres in eight dimensions.
• An auto-formalisation agent called Gauss, developed by Math, Inc, was used in the verification process.
• Lean, a programming language with a logical foundation, was used to check the definitions, theorems, and proofs.

Detailed Insights:

• Viazovska's proof, like many human proofs, originally skipped steps considered obvious, but the new achievement involved a machine checking all steps.
• The effort to have machines check proofs is to avoid logical flaws or unstated assumptions that can slip through unnoticed.
• Formalisation translates human proofs into a machine's language, allowing other mathematicians to audit it or reuse parts of it.
• The Sphere Packing Lean project had a large Lean codebase with lemmas and definitions, and Gauss, an AI tool, formalised the remaining statements for Lean to check.
• Lean's kernel verifies proofs using built-in logical rules, while mathlib supplies standard definitions and theorems.
• The ultimate purpose is to make mathematical correctness less dependent on trust and more on explicit and verifiable mathematics.
• Major theorems that have been completely formalised include the four-colour theorem, the prime number theorem, the Feit-Thompson odd order, and the Kepler conjecture.
• Tools like Lean Copilot, Sledgehammer, and Alpha Proof are helping with formalisation.
• AI is being used to generate novel conjectures in topology and geometry, often spotting connections across disparate fields that evaded experts.

Key Concepts Involved:

• Fields Medal: An award presented to two, three, or four mathematicians not over forty years of age at the International Congress of Mathematicians.
• Formalisation: Translating a non-exhaustive human proof into a machine's language.
• Lemmas: A proven proposition which is used as a stepping stone to a further result.
• Theorems: A statement that has been proven on the basis of previously established statements.