The latest development of foreign science and technology; Foreign Technology, No.7, 2000, pp.30-32
-
Mathematical proof and its beauty
Mathematical proofs used to be simple and beautiful, but now they are more like a voluminous War and Peace or even a boring phone book. People can't help asking: Has beautiful mathematical proof become a lost art? Euclid is admired by the world for his simple, beautiful and intelligent mathematical argument. People are amazed at the elegance of mathematics and the beauty of the mathematical world, and are also willing to understand the correctness of its proof. Paul Erdos, an eccentric but clever mathematician, concluded that God has a book about all the best mathematical proofs. In his view, the mathematician's job is to peek at books over God's shoulders and pass on God's wisdom to mankind. But now it seems that this simple and elegant method is only one of several mathematical proofs. Throughout the past few years, the famous mathematical proofs are not short and pithy proofs that the Greeks are familiar with, but extremely huge, with hundreds or even thousands of pages. What happened to the beauty created by God? Are these huge proofs really necessary? Is it because mathematicians are too stupid to find the short and ingenious proof method written in the book of God? One of the answers is that a short mathematical exposition may not have a short proof. Kurt Godel, an Austrian-born mathematician, proved in principle that some short mathematical statements need a long proof, but he didn't know which mathematical statements were like this, and so were others. In the past few years, some important mathematical proofs are long and complicated, such as Fermat's Last Theorem, which was proved by andrew wiles, a mathematician from Princeton University, in 1996. In order to solve this problem, wiles used a lot of mathematical methods to disassemble the problem. It turns out that it is not boring at all, but rich and beautiful. Although it is not as short as the proof in the Book of God, it is also like War and Peace. The formation process of Fermat's last theorem is worth mentioning. 1637, Pierre de Fermat, a French lawyer with extraordinary mathematical talent, expounded an important theorem in his personal book Diophantine Arithmetic, which is related to Pythagoras theorem a2+b2=c2 (where A, B and C are integers). A, B and C satisfying this equation have many different values. Fermat tried to make cubic or quartic equations hold, but he couldn't find an example. In other words, he can't find the equation that makes an+bn=cn, where a, b, c are integers (a, b, c≠0) and n is an integer greater than 2. Does this mean that this equation cannot exist? Fermat wrote in the margin of his book that he thought of a wonderful way to prove that Pythagoras theorem only applies to quadratic, but he also noticed that "the place is too small to write this proof". Although such a proof method cannot be written on the edge of the book, it is certainly concise and beautiful, and it can occupy a place in the "book of gods". However, for three and a half centuries, one mathematician after another tried to find it, but all failed. However, in the late 1980s, andrew wiles, a British mathematician from Princeton University, began to solve this problem. He worked alone in his attic and only told a few colleagues who swore to keep his secret. Wiles used the same method as his predecessors, assuming that A, B, C and N satisfy the existence of equations, and then he hoped that algebra would lead to contradictions. His starting point originated from the idea of Gerhard Frey of Essen University in Germany. Frey thinks that the three roots A, B and C of Fermat's "impossible existence" equation can form a cubic equation representing an elliptic curve. This is a clever way, because mathematicians have studied elliptic curves for more than a century and have mastered many methods to deal with elliptic curves. At that time, mathematicians had realized that the elliptic curve generated by the root of Fermat equation had peculiar characteristics, which contradicted another conjecture Taniyama-Shimara-Weil, which determined the properties of elliptic curves. The root of Fermat equation will deny the Taniyama-Shimahara-Weil conjecture, that is, if the conjecture is proved to be correct, the root of Fermat equation cannot exist. So it took wiles seven years to solve this problem with number theory. Although he worked alone, he didn't create this field alone, and he kept close contact with the latest progress in the field of elliptic curves. Without a series of new methods created by many number theory experts, he may not succeed. Even so, his own contribution is enormous, and he has pushed this field to a brand-new era. Wiles's certificate has been published at present, with more than 100 pages. Of course, it's too long to write on the edge of the book. The method of proving Fermat's Last Theorem invented by wiles is extremely rich and beautiful. His thought initiated a brand-new era of number theory. Of course, his proof is very long, and the specific content can only be understood by experts in this field. There is also a third mathematical proof method, which only appeared in recent 30 years. This is a computer-aided proof. It's like a fast food restaurant offering a monotonous sandwich. It can do the work, but the result is not beautiful at all. The job of computer-aided proof is to turn the usual clever method of solving difficult problems into huge and procedural calculations, and then hand them over to the computer. If the computer says "yes", the proof is complete. An example of using this proof method appeared last year. In 16 1 1, johannes kepler came to a conclusion when he studied the method of piling balls together: in a given space, the most effective way to put the largest number of balls in is the method of piling oranges by fruit merchants. Stack one layer into a honeycomb shape first, and then stack the same layer on it, but it is located in the depression of the first layer. This stacking method also appears in many crystals, which physicists call face-centered cubic lattice. Kepler's conclusion is "obvious", but people who think so naturally lack keen judgment. For example, at that time, it was not even proved that the most effective stacking method included water paving. Although fruit merchants put their goods layer by layer, they don't have to. Even the two-dimensional version of this problem, that is, the most effective way to lay a circle with the same size on a plane is honeycomb laying, was not proved by Hungarian mathematician laszlo Fejes Toth until 1947. About 10 years ago, Wu Yixing of the University of California announced that he had proved a three-dimensional version of this problem. This proof is 200 pages long, but the reasoning in it lacks coherence, and gradually other mathematicians refuse to accept this proof. Last year, Thomas Hales of the University of Michigan published a computer-aided proof, which was hundreds of pages long and accompanied by a large number of calculation results. This proof was first published on his website, and now it is being reviewed by peers with a view to publishing it in mathematical journals. Hales's method is to record all possible ways of pellet stacking, and then prove that if the stacking method does not conform to the face-centered cubic lattice structure, it can be compressed by slight adjustment. The conclusion is that the only incompressible stacking method, that is, the most effective method to fill the space, is the kind of speculation. Todd also deals with two-dimensional problems in this way. He listed about 50 possible arrangements, while hales had to deal with thousands. Computers need 3G memory to prove these different methods. One of the earliest mathematical proofs using this computer method is the four-color principle. About 150 years ago, Francis Guthric, a British mathematician, asked whether all maps containing countries of any shape could be colored in four colors, so that neighboring countries could have different colors. This principle sounds simple, but it is extremely difficult to prove. 1976, American mathematicians Kenneth Appel and Wolfgang Harken discovered the proof method. Through repeated experiments and manual calculations, they first proposed nearly 2,000 combinations of countries, and then proved by computer that these combinations are "inevitable", that is, the arrangement of countries in any possible map is at least one of these combinations. The next step is to prove that any of these combinations is "reducible", that is, a part of each combination can be reduced and removed to become a simple map. Strictly speaking, restoration must ensure that if the restored simple map can use four colors, so can the original map. Now imagine the simplest map that needs more than five colors, the so-called "minimum violation map". Like all maps, this map must contain at least one of 2000 reducible combinations. By reducing the included combinations, we can get a simpler map, which certainly only needs four colors, that is, the minimum violation map only needs four colors, and the only possibility to avoid this contradiction is that the minimum violation map does not exist. In fact, more methods are used in the process of proof, not just thumbnails. Finding the corresponding reduction method for each combination requires a lot of computer operations. It takes 2000 hours with the fastest computer at that time, but only 1 hour with the current computer. Finally, Appel and Haken get the answer. Computer-aided proof brings a series of problems such as style, innovation, method and concept. Some philosophers believe that in the traditional sense, what is obtained by computer-aided proof is not proof at all. Others pointed out that this massive and programmed work is the specialty of computers, but it is the weakness of human beings. If computers and people come to different conclusions after large-scale calculations at the same time, the bet should be on the computer. Any calculation carried out by a computer is ordinary and monotonous, and only when people go deep into it will it be valuable. If wiles's proof of Fermat's Last Theorem is as rich in connotation and full of thoughts as War and Peace, then computer proof is more like a phone book, and no one wants to read such things. In fact, proofs like Appel-Haken and Hales are too short from the perspective of literature reading and are only used for auditing. However, these proofs do not lack elegance and depth. After all, we should be smart enough for computers to solve difficult problems. After proving the correctness of the conjecture, we may try to find a more elegant proof method. It sounds strange, but it often proves that it is easy to know the correctness of things. It is possible to hear this conversation among mathematicians, and some people will jokingly suggest that we can spread a solved lie in an important problem to make it easier for others to find a way to prove it. Does this mean that mathematicians can gradually discover the God proofs of Kepler's and Fermat's theorems? If so, of course, it is good, but it may not be satisfactory. Perhaps there is no proof of these theorems in the book of God. There is no reason to think that stating a simple theorem must have a simple proof. As we all know, many things that are extremely difficult to do are simple to say, such as "going to the moon" and "treating cancer", and mathematics is no exception. Experts are often deeply impressed by the mistakes of complicated and lengthy proofs or other simplified proof methods put forward by some people. Although they are often right, their judgment is occasionally affected by knowing too much. Just like there is a high mountain, the winding mountain road is the natural way to reach the top. But if the mountain is full of glaciers and ravines, the road may be extremely long and dangerous. Perhaps this seems to be the only way to choose, and there are cliffs that cannot be climbed. However, it is possible to invent a helicopter, so that you can reach the top quickly and easily. Therefore, some people will come across similar methods to prove the experts wrong. Please remember that Godel's theory and some mathematical proofs he found must be very long. Perhaps the four-color theorem and Fermat's last theorem are examples. As far as the four-color theorem is concerned, it can be proved by calculation that it is impossible to have a shorter proof if we use the current method, that is, to find a series of inevitable combinations and then eliminate them one by one by "reduction". It's like climbing a mountain and encountering an ice gap. Of course, the emergence of a "helicopter" is not ruled out. Go back to Fermat's scribbled notes on his works. If the best proof that humans can find can only be so huge, then why did Fermat annotate it like that? Of course, he won't make a mistake in the 200-page proof and scribble "Don't write on the edge of the book." This is another theory. Godfrey Hardy, a mathematician at Cambridge University, is an atheist, but he is not a traditional religious believer. Hardy believes that God's mathematical proof is for him, so when he takes a boat trip that he hates, he will send a telegram: "Riemann conjecture has just been proved, but it is impossible to write down the proof process on the boat." Riemann conjecture of complex analysis of prime numbers has always been the most important unsolved problem in mathematics. Hardy believes that God will not let the ship sink, because if the ship sinks, he will gain the reputation that he may find a way to prove it after death. Maybe Fermat has the same idea, or maybe he just wants to be famous. If so, his purpose has been achieved.
Believe in mathematics, or believe in computers
Author: Rui | May 2004-14
If you have a bunch of oranges in front of you, how to put them in the most space-saving way?
Don't think that this is just one of the daily troubles that plague fruit shop owners. Although anyone can judge by experience or intuition, it is obviously more reasonable and space-saving to put the oranges on the upper layer alternately in the adjacent grooves of the oranges on the lower layer than to stack them directly. But who can mathematically prove that there is really no more reasonable method?
In fact, in more than 400 years, the question of "Kepler conjecture" first put forward by Sir Walter Raleigh stumped many mathematicians. Although the latest issue of Mathematical Yearbook published a proof paper written by Thomas Hiles, a professor of mathematics at the University of Pittsburgh, in 1998, this authoritative mathematical community admitted that a difficult problem has the usual final solution form, but this time it seems to have caused more controversy. The center of the argument is, can you believe the calculation result of a computer?
Speaking of the history of Kepler's conjecture, it can be traced back to one day in 1590. When preparing supplies for his fleet before going to sea, Sir Walter Raleigh suddenly thought: Can we calculate the exact number of shells according to the height of a pile of neatly arranged shells? Thomas Harriot, his assistant and mathematician, gave the answer almost effortlessly. However, when thinking more deeply about this problem, Harriet found that the mystery was not so simple. Is the arrangement commonly used by sailors the most space-saving way? How to place spheres so that they occupy the least space? Harriet conceived various stacking models and developed his own atomic theory on this basis.
A few years later, in a letter to the famous astronomer johannes kepler, Harriet mentioned this problem. After a series of experiments, Kepler put forward his own conjecture on the correct answer to the question in the booklet "New Year's Gift-Snowflakes with Six Results" published by 16 1: When spheres of the same size exist in the form of "face-centered crystals"-the center of the sphere is located in the center of each side of a cube, and the first layer is placed in a hexagon.
After Kepler conjecture was put forward, many mathematicians tried to prove it. But it was not until more than 200 years later that another great mathematician, C.F.Gauss, proved Kepler's conjecture in 183 1, that is, Kepler's conjecture is correct for regular shapes. But after that, the proof of Kepler's conjecture stopped. At the international congress of mathematicians in 1900, mathematician david hilbert listed it as one of the famous "23 unsolved mathematical problems".
1953, the Hungarian mathematician Laszlo Fejes Toth pointed out that the proof of Kepler's conjecture can be simplified to a limited number of calculations, whether the shape is regular or irregular. This means that, theoretically, it is feasible to exhaust all possible proofs. And a fast enough computer can turn this idea into reality.
From 1992, Hiles at the University of Michigan began to cooperate with his students to prove Kepler's conjecture with computer assistance. After six years of operation, Hiles announced the completion of the certificate in August of 1998. All his proofs include 250 pages of notes, 3GB of computer programs, data and calculation results.
Although Hiles's proof is so unusual, the Mathematical Yearbook agreed to publish this paper. To this end, the Mathematical Yearbook also specially hired Gabor Fejestoth of the Hungarian Academy of Sciences, the son of laszlo Fejestos, as the head of the evaluation committee.
Kepler's conjecture is not the first famous mathematical problem proved by computer. 1976, two mathematicians of the University of Illinois used computers to prove the famous four-color theorem, that is, any map only needs four colors to ensure that the colors of two adjacent areas will not be the same. After this proof was published, mathematicians kept finding some mistakes from it. Although every time a mistake is found, researchers can correct them quickly, but this has left a very bad impression on many mathematicians.
In order to avoid repeating the mistake of proving the four-color theorem, the staff of Mathematical Yearbook decided to thoroughly and cautiously test the proof of Kepler's conjecture. However, after nearly six years of verification of massive data, last year, the jury reluctantly announced that it would abandon the plan to fully verify Kepler's conjecture. Everything they have verified is absolutely correct, but it is almost impossible to check all the data clearly.
In desperation, Mathematical Yearbook came up with a flexible method. They intend to add a disclaimer before the published paper: most, but not all, of this certificate has been verified. However, this idea has been criticized by many mathematicians. Finally, after consulting another mathematician, the Mathematical Yearbook made a Solomon-style decision. Put half of all the papers, publish the proofs that have been verified by traditional methods, and discard the data calculated by computers.
In fact, a series of debates around Kepler's conjecture are largely about whether students should be allowed to use the high-end version of calculators in math classes, but both sides of the debate have become professional mathematicians, making it more difficult to choose the value judgment. The focus of the problem is that if Hiles' proof is accepted, it means that the computer is assumed to be completely correct when performing calculations, and there will be no minor program errors. And whether this is really the case, it is difficult for human beings to judge by their own abilities. As John Conway, a professor of mathematics at Princeton University, said in an interview with The New York Times, "I don't like them (computer proofs) because you feel like you don't know what happened."
This is undoubtedly a very unacceptable result for the mathematics community, which has always pursued the principle that truth can be judged by logic and operation and clearly and concisely proved as "good mathematics". Moreover, the operation of the computer is not impeccable. Intel has been using calibration tool software to check the algorithm of its computer chip, hoping to avoid the data operation error of 1994 Pentium chip from happening again.
However, some optimistic mathematicians point out that since the best computer can beat the world chess champion in the competition, the future computer should also be able to solve the mathematical problems that have baffled the greatest mathematicians. But it seems that this is not the key to the problem. Kepler said that mathematics is the only good metaphysics. It is always ironic to answer his conjecture in such a metaphysical way with a computer.