# What are the most interesting mathematical theorems

## This number theorist fears that a lot of our math basics are wrong

It's time to usher in a new era in mathematics, says Kevin Buzzard. The British number theorist and math professor at Imperial College London wants computers to play a bigger role in pure mathematics, especially in evidence. Mathematical proofs have become so complex that no one can understand them in detail, let alone verify them. Buzzard fears that much of the accepted evidence is, in truth, false.

What is a math proof? A proof demonstrates that a mathematical assumption is correct. With each proof, our knowledge of mathematics grows - and this then seeps into other areas.

To prove it, you need a few definitions first. For example, you define a set of numbers like all whole numbers, i.e. any number from minus infinity to plus infinity. Next, one formulates a theorem. For example: there is no greatest whole number. The proof itself is then the logical reasoning that shows whether the theorem is right or wrong - right in this case. The logical derivation in the proof is based on other, already proven mathematical truths - for example that 1 is less than 2.

Also at VICE: The math of a mass uprising

Because humankind has been doing mathematics for thousands of years, modern evidence builds on a multitude of previous findings. However, Buzzard says that in many cases the old evidence on which the new evidence is based has not been clearly understood. There are important scientific papers that openly refer to unpublished works. That worries Buzzard.

"I fear that all of the published math is wrong because mathematicians don't control the details - and I've seen them wrong," Buzzard told VICE.

"The likelihood that some of our great castles are not built on sand, in my opinion, is almost zero," Buzzard wrote in a presentation.

Actually, new mathematical theorems should be proven from the ground up. Every step has to be controlled. On the other hand, experienced and respected experts play an important role in mathematics. If one of these sages cites an article and refers to it in their work, that article probably does not need to be checked again - at least that is the widespread attitude.

Buzzard accuses modern mathematics of being too dependent on this select circle of wise men. New evidence cites perhaps 20 other papers, and only a single one of them can be 1,000 pages of dense and complex reasoning. If a respected mathematician cites the 1,000-page paper in her own proof, many other mathematicians assume that the work cited and the new proof are correct. As a rule, nobody then bothered to check everything again.

According to Buzzard, nobody really understood the proof of one of the most difficult mathematical problems ever, Fermat's Great Theorem from the 17th century, published in 1994.

"I believe that no one, dead or alive, knows all the details of this proof. But the mathematical community has accepted the proof of Fermatsch's Great Theorem anyway," Buzzard wrote in a presentation. "Because the wise men decided the evidence was OK."

A few years ago, Buzzard first heard about evidence testing software in talks given by math greats Thomas Hales and Vladimir Voevodsky. With this, evidence can be systematically confirmed by a computer.

When Buzzard began to work with such a program, Lean, he was instantly captivated. Not only did the software allow him to examine evidence beyond doubt, it also encouraged mathematical thinking in a clear and unambiguous way.

"Computers only accept very precise inputs, which also corresponds to my preferred approach to mathematics," says Buzzard. "I fell in love because I felt like I had found a soul mate. This program thought about math as I did."

To verify a proof with Lean, one must formalize the proof or convert it from human language and symbols to the Lean programming language. This also applies to all subordinate proofs and definitions on which the new work is based. While this process is very labor-intensive, Lean seems to be able to handle all of the math tasks Buzzard feeds it with - this is what sets Lean apart from other comparable software.

This is one of the reasons why Lean has aroused the interest of more and more mathematicians, especially in teaching. Jeremy Avigad is a lecturer majoring in evidence theory at Carnegie Mellon University in Pittsburgh. He and Buzzard began using Lean in introductory proof theory seminars. The software checks every line of evidence and gives feedback, which is particularly helpful for students.

Although Avigad is excited about the growing interest in Lean, he urges caution. The software still needs improvements. The use of such evidence assistants is above all time-consuming. "The area has been around for a couple of decades and it's getting better and better, but we haven't quite got there yet," he says.

If these hurdles are overcome, the software could also be used in other ways, according to Buzzard. New results are published every year at a breathtaking speed. It is therefore extremely important to be able to search this evidence. If all new abstracts were entered in Lean, any mathematician could query the database for a precise mathematical object and learn all that is known about it.

Computer researchers could use such a database as a training ground for artificial intelligence. Programs can deal with the precise language of Lean better than with work that is written in idiosyncratic English.

Another goal of computer science would be to create a generalized, automated theorem prover - a software system that derives its own proofs. The increasing use of Lean could be an important step towards automating math.