Machines Are on the Verge of Tackling Fermat’s Last Theorem—a Proof That Once Defied Them
- Oops!Something went wrong.Please try again later.
"Hearst Magazines and Yahoo may earn commission or revenue on some items through these links."
A mathematician will turn a groundbreaking 100-page proof into computer code.
The proof tool, Lean, lets users turn proofs written in prose into rules and logic for testing.
Kevin Buzzard already uses Lean and makes tools for students to better learn proofs.
Some people count down to new video games or Beyonce albums. Mathematicians can now also count down to April, when mathematician and programmer Kevin Buzzard will release and begin updating his newly-announced plans for a computer coded proof of Fermat’s Last Theorem. He has received a grant for this research, which is expected to take years and will likely be one of the most complex proofs to be computerized in this way.
17th century French mathematician Pierre de Fermat came up with this theorem many years ago, but was unable to prove it in his own lifetime. The theorem states that no three positive integers a, b, and c satisfy the equation aⁿ + bⁿ = cⁿ for any integer value of n greater than 2. (Thank you to a keen-eyed reader who noticed we initially used subscript by error.)
In case you don’t remember high school geometry class (which is understandable), mathematical proofs use logic statements, measurements, and other traceable steps to verify that a statement about math is logically true. And as Fermat’s Last Theorem indicates, sometimes mathematicians are trying to prove a negative: how can you make sure there are no integers all the way to infinity that satisfy the equation?
Thankfully, turning the idea of infinity into logic is old hat for mathematicians—that is, mathematicians today. In much simpler proofs, we use induction to show that the next counting number will always fall into the logic we already established. If it’s true for 8, it’s true for 9, 10, 11, and so forth, up to infinity. But Fermat’s Last Theorem was stuck in math’s craw for hundreds of years. It was finally proven in 1993 by English mathematician Andrew Wiles in a written proof that is 100 pages long. Wiles became a household name, at least in mathematical households.
A 100-page proof is way outside the realm of the average math student, or even mathematician. But there’s no reason the proof need only be laid out the old-fashioned way anymore. Lean is a coding tool built on the C++ language specifically to help codify and verify induction proofs. While much of “artificial intelligence” is just careful arrangement of human-like wording, this kind of computer-aided proof is a truer blend of how humans think with how computers can help reinforce their work.
British mathematician Kevin Buzzard teaches math at Imperial College in London, and he's spent years building tools in Lean that support the entire undergrad math education offered at Imperial College. Students can see the material they discuss in class broken down into functional steps that use logic and math operators. It’s like a math-proofs Rosetta Stone.
Clarissa Littler, a mathematician and coder who teaches Discrete Math at Portland Community College, has used Kevin Buzzard’s self described “classical introduction game for Lean” in their discrete math classes for the last two quarters. “I used the Natural Number Game to get students used to the idea of mathematical induction and I use the Set Theory Game to, well, get folks used to reasoning about sets [and] bridging the gap between the hyper-formal ‘here is first-order logic, now write proofs as a sequence of rule applications’ and the more informal ‘write a prose argument explaining why something is true’ tasks I have them do,” they told Popular Mechanics.
“A big emphasis in the classes is on getting students—who usually don’t have a very strong math background—more comfortable with thinking like a mathematician and with ideas of proof, evidence, and how to show something is true,” they continued.
These changes of abstraction—taking formal logic, turning it into a list of rules, then writing it as prose, and all vice versa—is key to breaking projects into code pieces that work together. It’s an essential place where coding and pure mathematics overlap, which makes it a great area for a computer-powered learning aide like Lean.
Buzzard told New Scientist that his goal is to help codify more of the complex math ideas that Fermat’s Last Theorem helped inspire. Centuries worth of people developed entire, very valuable new areas of math as they tried to prove this theorem that, Buzzard affirms, is “completely pointless.” Now, turning Wiles’ 100-page proof into formal language and rules could open up computer-supported proofs to new generations of mathematicians. And as with Littler’s real-life students, this bridging tool could also help coders.
“I think ambitious projects area always worthwhile in this space because we'll all benefit from the lessons learned [and] the libraries written,” Littler said. “Interactive theorem proving is still a relatively young field, and the Lean community has been doing a lot of good work that, I think, is getting us closer to these tools being an unremarkable part of undergraduate mathematics education.”
There’s an additional layer of value in this project, too. As computer tools grow more powerful, and as the boundaries between specific areas of math—and even between entire disciplines—grow blurrier, there are proofs that are almost unverifiable. Japanese mathematician Shinichi Mochizuki of Kyoto University wrote an infamous 500-page proof that took years to be published, partly because no one knew what to do with it.
Mathematics will probably get even blurrier—not in veracity or logical soundness, but in the transparent breadth of different ideas that can be piled into one proof together. Equipping mathematicians with robust logic tools like Lean could help them codify their ideas as they go, making their work at least less inscrutable to colleagues who may not yet understand the overall proof. The more everyone puts down precedents and shares their work, the more future mathematicians can iterate on that work their own work going forward.
In fact, Lean itself creates a workflow like this. Buzzard said on Twitter, that the “very nature of writing mathematics in Lean is that you can leave very precisely-stated results (which might be mathematically “standard”) unproved and then someone else (perhaps who has no interest or understanding of the full FLT proof) can pick them off later.”
In other words, Fermat’s Last Theorem is about to get the crowdsourcing treatment—especially if the coding takes longer than Buzzard’s remaining working years. It takes a village to raise a mathematical proof. And maybe, someday, we’ll get Genius.com for proofs.
You Might Also Like
