Mathematical proof, not new.
Machine proof?
By Caroline Delbert Published: Mar 27, 2024 7:30 AM EST
... 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.)
Mathematician Kevin Buzzard will use his experience with Lean to chip away at coding a landmark proof.
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. ...
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 sheer 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.
Caroline Delbert is a writer, avid reader, and contributing editor at Pop Mech. She's also an enthusiast of just about everything. Her favorite topics include nuclear energy, cosmology, math of everyday things, and the philosophy of it all.
A Part of Hearst Digital Media
We may earn commission from links on this page, but we only recommend products we back.
©2024 Hearst Magazine Media, Inc. All Rights Reserved.
https://www.popularmechanics.com/sc...e-defied-them/?utm_source=pocket-newtab-en-us
Machine proof?
Machines Are on the Verge of Tackling Fermat’s Last Theorem—a Proof That Once Defied Them
Advanced algorithms are now deciphering what once was the domain of pure human intellect.By Caroline Delbert Published: Mar 27, 2024 7:30 AM EST
- 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.
... 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.)
Mathematician Kevin Buzzard will use his experience with Lean to chip away at coding a landmark proof.
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. ...
Related Story
The Math Behind Discovering ExoplanetsThere’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 sheer 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.
Caroline Delbert is a writer, avid reader, and contributing editor at Pop Mech. She's also an enthusiast of just about everything. Her favorite topics include nuclear energy, cosmology, math of everyday things, and the philosophy of it all.
A Part of Hearst Digital Media
We may earn commission from links on this page, but we only recommend products we back.
©2024 Hearst Magazine Media, Inc. All Rights Reserved.
https://www.popularmechanics.com/sc...e-defied-them/?utm_source=pocket-newtab-en-us
