Pushing the Frontiers of Mathematical Research

My earliest work did this kind of research

Pushing the Frontiers of Mathematical Research,   By Allyn Jackson

Commissioned by CACM Staff, September 8, 2022

For decades, mathematicians have turned to computers for help with tasks like big numerical calculations and visualizing complex geometric objects. Like a blackboard, the computer has been a handy tool that picks up where human capacity to juggle numbers, symbols, and pictures drops off.

Today, however, computers are playing an entirely new role: they are learning modern mathematics.

A loose-knit international group is using computer proof assistants, originally developed to check formal software correctness, to create online libraries of mathematical theorems and proofs. The theorems housed in these libraries can then be called upon as building blocks for proofs of new mathematical results. The hope is that the libraries one day will encompass the entirety of mathematical knowledge.

"It's a completely new way to do mathematics that is very satisfying," said mathematician Kevin Buzzard of the U.K.'s Imperial College London.

Buzzard discussed this work in one of the most-watched lectures at the 2022 International Congress of Mathematicians in July this year. (The Congress, originally scheduled to be held in Saint Petersburg, Russia, was transformed into an entirely online event after that country's invasion of Ukraine.) Around the same time, a paper appeared on the arXiv containing what might be called a "proof assistant manifesto," laying out progress achieved and describing challenges ahead. Buzzard is one of the paper's 10 authors, along with ACM A.M. Turing Award recipient Leslie Lamport.

During the course of his career in number theory and algebraic geometry, Buzzard has worked on pure mathematics with no obvious applications. He describes his latest work with computer proof assistants as also "100% blue-sky research," explaining, "It's interesting, important, and beautiful. But I can't see the future. I don't know what killer app might come out of this work."

Verifying Proofs Down to the Axioms

Computer proof assistants, also called interactive theorem provers, began to have a significant impact in mathematics starting with the work of Thomas Hales of the University of Pittsburgh.  In the late 1990s, Hales announced a solution to a venerable sphere-packing problem called the Kepler conjecture. While his approach was generally accepted as correct, Hales' use of a computer program to sort through a huge number of possible packings left many skeptical.

Hales then embarked on a multi-year project to validate his solution by recasting it as a "formal proof," a thoroughgoing version of the proof in which every logical inference is checked, down to the fundamental axioms of mathematics. Formal proofs, far too verbose and tedious for humans to read, are tailor-made for computer proof assistants. In 2014, Hales and 20 collaborators completed a computer verification of the Kepler proof. 

In parallel with this work, during the early 2000s, a few mathematicians began to use proof assistants to formalize proofs of several classic mathematical results. The work was slow and painstaking, and the technology rather off-putting. As a result, formal proofs remained something of a niche area, far from the frontier of mathematics.

Buzzard got into the act after listening to a 2017 lecture in which Hales described his experiences using proof assistants. "That lecture changed my life," said Buzzard, as he realized that proof assistants could handle the theorems that mathematicians are working on at the frontier of research today. "Computer scientists were figuring out how to write the software, to make it useful," Buzzard said. "They've done that now. Now it's our turn."

The True Value of Proof Assistants

As the name suggests, a computer proof assistant is very good at verifying proofs, but its true value in mathematics lies elsewhere, in its ability to store mathematical results and the fundamental logic supporting them. Every theorem, lemma, and proposition that was used or proved in the course of verifying, for example, Hales's solution of the Kepler conjecture, now sits in the memory of a proof assistant, ready to be called upon as raw material to build proofs of new theorems.  ... '