Simple math proofs12/16/2023 For example, Thomas Hales seems to have proved that the densest packing of spheres in 3d space is the obvious one, like this: These longer proofs all involve computer calculations. Maybe now Gonthier is dreaming of computerizing the whole classification of finite simple groups.īut there are even longer proofs of important results in math. It involves 15,000 definitions and 4,300 lemmas. It took them 6 years! The completed computer proof has 170,000 lines. But the real reason of having this project was to understand how to build all these theories, how to make them fit together, and to validate all of this by carrying out a proof that was clearly deemed to be out of reach at the time we started the project.” “The reaction of the team the first time we had a meeting and I exposed a grand plan,” he recalls ruefully, “was that I had delusions of grandeur. When Gonthier first suggested a formal Feit-Thompson Theorem proof, his fellow members of the Mathematical Components team at Inria could hardly believe their ears. It’s quick to say, but hard to show-so hard that making the proof fully rigorous on a computer seemed out of reach at first: So, this property of a group got the name ‘solvability’.Įvery finite group with an odd number of elements is solvable. Galois showed that every polynomial equation has a group of symmetries, and you can solve the equation using addition, subtraction, multiplication, division and taking roots if its group has a certain special property. For example, those operations aren’t powerful enough to solve this equation: He showed a bunch of specific polynomial equations couldn’t be solved just using addition, subtraction, multiplication, division and taking roots. Galois invented group theory and used it to go further than Abel and Ruffini had. What does the Feit–Thompson theorem say? Every finite group with an odd number of elements is solvable! Explaining that statement might take quite a while, depending on what you know about math. Feit and Thompson’s original proof of this result, skipping lots of steps that are obvious to experts, took 255 pages! Recently mathematicians led by George Gonthier have used Coq to give a completely detailed proof of a small piece of the classification of finite simple groups: the Feit–Thompson Theorem. The French are so sexy that even their proof assistant sounds dirty: it’s called Coq. So far six books have been written as part of this project.Įven when it’s all in one book, how can we be sure such a long proof is right? Some people want to use computers to make the argument completely rigorous, filling in all the details with the help of a program called a ‘proof assistant’. The new proof will be a mere 5,000 pages long. This was done by lots of people in lots of papers, and the total length is somewhere between 10,000 and 20,000 pages… nobody is exactly sure! People are trying to simplify it and rewrite it. Jumping ahead quite a lot, the longest proof written up in journals is the classification of finite simple groups. Did most people ignore it completely? Or did everyone ignore most of it? Anyway, his argument seems to have a gap… and later Niels Abel gave a proof that was just 6 pages long, so most people give the lion’s share of credit to Abel. But his proof was 500 pages long! As a result, it was “mostly ignored”. In 1799, Paolo Ruffini proved that there was no general solution using radicals for polynomial equations of degree 5 or more. (Click repeatedly to enlarge.) But again, it only involves additions, subtraction, multiplication, division and taking roots.
0 Comments
Leave a Reply.AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |