Can you trust computers?

This simple expression in the language of mathematical software Maple tests a formula that counts the number of integer triangles with a given perimeter.

Shalosh B. Ehad, co-author of several works published in respected mathematical journals, is known for his laconic proofs of theorems and identities that previously required many pages of mathematical reasoning. Last year, when he was asked to confirm the formula for the number of integer triangles with a given perimeter, Ehad performed 37 calculations in less than a second and gave the answer: correct.

Shalosh B. Ehad is a computer. More precisely, this is any of the computers used by mathematician Doron Seilberger - from Dell in his office in New Jersey, to an Austrian supercomputer, whose time he sometimes rents. The Hebrew name for “three B is one” refers to AT & T 3B1, the first version of Ehad.
')
“Soul is software,” says Seilberger, who writes her code with the popular mathematical programming tool Maple.


Doron Seilberger

A mustache 62-year-old professor at Rutgers University, Seilberger is at one end of the spectrum of opinions about the use of computers in mathematics. He points out Ehad as a co-author of his work since the late 1980s, “to state that computers must also be given the deserved glory.” For decades he has resisted man-centered fanaticism inherent to mathematicians: the preference for evidence made by man on paper. Seilberger argues that such sentiments have brought progress to a standstill. “And for good reason. People feel they’ll lose their jobs. ”

Anyone relying on calculators or spreadsheets may be surprised that not all mathematicians accept computers. For many of them, programming a computer to prove the identity of the triangles, or to solve a problem that has not yet been solved manually, is akin to changing the rules of a 3000-year game in the course of its operation. The search for new knowledge about the mathematical universe almost always required the use of intuition, creativity, and a bit of genius - and not a knock on the keys. It was the need to avoid computing (due to the lack of a computer) that often progressed, and led mathematicians to elegant character techniques like mathematical analysis. For some people, the process of discovering the unexpected, building paths leading to truth, and discovering new mathematical objects in the process, is not in itself a means to an end, but an end.

In other words, finding evidence in which computers play an increasing role is not always the ultimate goal of mathematicians. “Many mathematicians believe that theories are being created to understand the mathematical universe,” says Minhyong Kim, a professor of mathematics at Oxford University and Pohang University of Science and Technology in South Korea. Mathematicians are trying to create a conceptual platform that defines new objects and puts forward new hypotheses, as well as proving old ones. Even when a new theory provides important evidence, many mathematicians "feel that they are more interested in theory than in proof," says Kim.

Computers are universally used to discover new hypotheses through the search for patterns in data or equations, but they cannot develop a concept for them within the framework of a larger theory, as people do. Computers also miss the process of creating a theory when proving theorems, says Konstantin Telemann, a professor at the University of California at Berkeley, who does not use computers in his work. He believes the problem is this. “Pure mathematics is not just trying to find out the answer — it needs understanding,” says Telemann. “If all you have is a computer that has checked a million cases, it means that you could not figure out the task.”

Zeilbegger disagrees. If people can understand the task, then, in his opinion, the task is trivial. In the endless search for mathematical progress, humanity, in his opinion, is losing its grip. Intuitive insights and abstract thinking gave us a head start, but as a result, the logic of zeroes and ones, controlled by programmers, will overtake our conceptual understanding, as it happened in chess.

“Most of what people do in 20-30 years will easily make computers,” says Seilberger. “For some sections of mathematics, this has already happened. Many published works performed by people are already outdated and can be done by computers. Some of today's tasks are completely uninteresting, but they are done because they are accessible to people. ”

Seilberger and other pioneers of computational mathematics feel that from the last five years their views have turned from radical to fairly common. Traditional mathematicians are retiring, and the technological generation is taking over. At this time, computers became millions of times more powerful than the first computers that appeared on the mathematical scene in the 1970s, and also appeared without counting new clever algorithms and convenient software. And more importantly, according to experts, modern mathematics is becoming more and more complicated. On the fronts of some areas of research, evidence made by people by hand is already listed in the Red Book.

“The time when someone could do real mathematical research worthy of publication without using a computer is running out,” says David Bailey, a mathematician and computer scientist from the National Laboratory for them. Lawrence Burkeley, and author of several books on computational mathematics. "And if you do this, you are increasingly restricting yourself in certain highly specialized areas."


Konstantin Telemann

Telemann studies algebraic geometry and topologies — in these fields, most researchers today cannot do without computers, as in other subsets of areas of mathematics related to algebraic operations. He concentrates on problems that can still be solved without a computer. “Do I do this math because I can't use a computer, or because this is the best thing I can do? Good question". Several times during his 20-year career, Telemann would like him to be able to program and be able to calculate the solution of the problem. And each time he decided to spend three months, which, in his opinion, are required to study programming, for a manual solution. Sometimes, according to him, he “does not deal with such questions or gives them to a student who knows how to program.”

If today doing math without a computer is like “running a marathon without shoes,” as Sara Billey from the University of Washington identified it, the mathematical community was divided into two crowds of people running.

Computer use is common, but not widely accepted. Bailey believes that researchers often downplay the importance of the computational aspects of their work in published studies, possibly to avoid unnecessary friction. And although computers have produced outstanding results from as early as 1976, students and post-graduate students of the faculties of mathematics still do not need to learn programming in basic education. Mathematical departments, according to researchers, behave conservatively in changing curricula, and budget constraints can prevent the introduction of new courses. Instead, students often gain programming knowledge themselves, and as a result, their code turns out to be confusing and difficult to verify.

What is even worse, according to researchers, is the lack of clear rules for the use of computers in mathematics. “More and more mathematicians are learning to program; but the standards for testing the program and determining whether it is working properly — well, they are not, ”says Jeremy Avigad, a philosopher and mathematician at Carnegie Mellon University.

In December, Avigad, Bailey, Biley, and dozens of other researchers met at the Institute of Computational and Experimental Mathematics to discuss the standards of reliability and reproducibility of results. Of the many problems, one common question arose: in the search for the final truth, how much can we trust computers?

Computerized Mathematics

Mathematicians use computers in different ways. One way: proof of starvation. The proof is described in such a way that the assertion is true if it withstands a large but finite number of checks. Then a program is written that checks all these cases.

More often, computers help to detect interesting sequences in the data, according to which mathematicians then formulate hypotheses or just guesses. “I achieved a lot by just looking for patterns in the data and proving them,” says Biley.

Using computing to test the hypothesis in all possible cases, and the subsequent belief in this, “gives you psychological motivation to do all the work necessary to get proof of the hypothesis,” says Jordan Ellenberg, a professor at the University of Wisconsin who uses computers to searching for hypotheses, and then creating proofs manually.

Increasingly, computers not only help to find hypotheses, but also to prove them. Platforms for proving theorems, such as Microsoft's Z3, can test certain types of statements, or quickly find a counterexample that refutes them. Algorithms such as the Wilf-Zeilberger method (invented by Doron Zeilberger and Herbert Wilf in 1990) can perform symbolic computations, work with variables instead of numbers, and produce accurate results without rounding errors.

With the computing power available today, such algorithms solve problems, the answers of which look like algebraic expressions with tens of thousands of members. "And then the computer simplifies this expression to 5-10 members," says Bailey. “A man not only could not do this, he could not do it without mistakes.”

But computer programs are wrong, because they are written by people. Errors of the code and difficulty in finding them sometimes made mathematicians back down.

Telemann recalls that in the 1990s, specialists in theoretical physics predicted the existence of a “beautiful answer” to the question about higher order surfaces related to string theory. When mathematicians wrote a computer program to test the hypothesis, they discovered that it was incorrect. “But programmers were wrong, and physicists were right,” says Telemann. “This is the greatest danger of using computer evidence: what if there is an error in them?”

This question takes John Hank [Jon Hanke]. A number theory specialist and experienced programmer, Hank believes that mathematicians have become accustomed to overly trusting tools that they have recently disapproved of. He believes that the software can not be trusted, and you need to constantly check. But most of the software used by mathematicians cannot be verified. The most popular tools for mathematical programming, Mathematica, Maple and Magma, costing $ 1000 for a professional license, the code is closed. And users have already encountered errors in each of them.

“When Magma gives me the answer 3.765, how do I know that it is correct? - asks Hank. - I dont know. I have to trust her. ” If mathematicians want to maintain a long tradition in which each stage of the proof can be tested, then, according to Hank, they cannot use closed source software.

There is a free open source alternative, Sage, but in most cases it loses in power. She could catch up with competitors if more mathematicians worked on her development, as on Wikipedia, says Hank - but there is practically no academic motivation for this. “I wrote a bunch of software for quadratic forms in C ++ and Sage, and used them to prove the theorem,” says Hank. "And all this work on open source has not received recognition." After the closure of the opportunity to take a permanent position in the staff of the University of Georgia in 2011, Hank left science for finance.

Although many mathematicians are aware of the need for the urgent emergence of new standards, they will not be able to solve one problem. Checking someone else's code takes time, and people may not want to do it. “It's like looking for a bug in the code running on your iPad,” says Telemann. - Who will look for her? How many iPad users do code research? ”

Some mathematicians see only one way out: the use of computers for step-by-step proof of theorems, using cool and precise real logic.

Proof proof

In 1998, Thomas Hales surprised the world by using a computer to solve the 400-year Kepler hypothesis. She argues that the most dense method of packing balls is the storage method used for oranges - a package called face-centered cubic packaging. She is known to all street vendors, but no mathematician could prove it. Heles solved the problem by designating spheres as graph vertices and connecting them with edges. He reduced an infinite number of possibilities to a list of several thousand of the most dense graphs and conducted a "proof of starvation." “We then used linear programming to show that none of the possibilities was a counterexample,” says Heles, a mathematician at the University of Pittsburgh. In other words, none of the graphs turned out to be more dense than the graph corresponding to the packaging of oranges in the box. The proof consists of 300 pages of text and 50,000 lines of code.



Heles sent proof to Annals of Mathematics, the most prestigious journal, with the result that four years later, reviewers reported that they could not confirm the correctness of its code. In 2005, the journal published a shortened version of the evidence based on confidence in the correctness of the written part of the evidence.

According to Peter Sarnak, a mathematician from the Institute of Advanced Studies, who worked as an editor for Annals of Mathematics until January, the problems revealed by Heiles's proof have repeatedly appeared in the last 10 years. Knowing that computer proofs will appear more and more often in the future, the editors' board decided to listen to such evidence. “However, in cases where the code is very difficult to verify alone, we will not make statements about its correctness,” wrote Sarnak. “We hope that in case of sufficiently important results, other people will write a similar, but independent code, and verify the statements made.”

According to Heiles's colleagues, his response to the reviewer's dilemma may change the future of mathematics. “Tom is an amazing person. He is not afraid of anything, says Avigad. “After learning that people had doubts about his proof, he said, 'OK, the next task is to create a formally verified version of the proof'. He had no experience in this field, and he began to communicate with computer scientists and learn how to do it. And now this project has a few months left to complete. ”



To show the proof of proof, Heles considers it necessary to recreate it using the basic elements of mathematics — logic and axioms. Obvious things like x = x serve as a set of rules for mathematicians, just as grammar controls language. Heles intended to use a technique called “proof of formal evidence,” in which a computer program uses logic and axioms to evaluate each step of the proof. The process can be slow and laborious, but as a reward you get confidence. The computer “does not forgive you anything,” says Avigad, who formally tested the theorem on primes in 2004. “He keeps track of everything you do. He reminds you that there is still some case that needs to be taken into account. ”

By putting his proof of Kepler’s hypothesis to this test, Heles hopes to eliminate all doubts. “Now everything looks promising,” he says. But this is not his only mission. It also serves as the vanguard of formal evidence technology. With the proliferation of computer proofs that cannot be verified manually, Heiles believes that the computers themselves should evaluate the evidence. “I think formal proofs are absolutely necessary for the future development of mathematics,” he says.

Alternative logic

Three years ago, Vladimir Voevodsky, one of the organizers of the new mathematics program at the Institute of Advanced Studies in Princeton, discovered that the formal logic system called “theory of types” developed by computer scientists can be used to recreate the entire mathematical universe from scratch. The theory of types corresponds to mathematical axioms, but is expressed in computer language. Voevodsky believes that this other way of the formalization of mathematics, which he called the univalent foundations of mathematics, will put on stream the process of proving formal theorems.

Voevodsky and the team adapt the Coq program, developed for the formal confirmation of algorithms, for use in abstract mathematics. The user suggests tactics or logically consistent actions that the computer must use to verify the validity of one step of the proof. If the tactic confirms the step, the user suggests the next one to evaluate the next step. “So the evidence becomes a sequence of tactical names,” says Voevodsky. With improvements in technology and with the complication of tactics, similar programs will someday be able to argue on a par with people, or even surpass them.

Some researchers believe this is the only solution to the problem of complicating mathematics.

“Confirmation of work has become equal in complexity to writing a work,” says Voevodsky. - For writing, you get a reward - for example, a promotion - but no one gets rewards for checking someone else's work. So we dream that the work will go to the journal along with the file written in this formal language, and the reviewers will simply check the statement of the theorem and its value for the readers. ”

Formal proof of the theorems is rarely used so far, but some researchers believe that this will change with the improved adaptation of the Voivodship Coq program. Heles imagines a future in which computers are so eager to lead a high-level discourse that can prove large chunks of theorems with minimal human participation, or without it at all.

“Maybe he's right, maybe not,” says Ellenberg about Heles' predictions. “He is definitely the most thoughtful and knowledgeable person among all the people who are promoting this idea.” Ellenberg, like many of his colleagues, see more important roles for people in the future of their field: “We are very good at understanding those things that computers cannot understand. If we imagine a future in which all known theorems can be solved on a computer, we simply imagine other things that cannot be solved on a computer, and this will be mathematics. ”

Telemann does not know what to expect from the future, but he knows what kind of mathematics he likes more than others. Solving problems in a human way, with its elegance, abstractions and surprises, gives him more pleasure. “There is something against defeat that we resort to computer evidence. We can't do this, so let the computer work. ”

Even the most ardent fan of computers among mathematicians admits the existence of a tragedy in surrendering to the superior logic of Shalosh B. Ehad, and accepting the role of a supporting element in the search for mathematical truth. It's just people. “I am satisfied that I understand everything in the proof from beginning to end,” said Seilberger. - On the other hand, this is life. And life is a complicated thing. ”