Source: Turing Community

Author: Lin Jun Cen Feng

Wu Wenjun at work (May 12, 1919-May 7, 2017). Source: Academy of Mathematics and Systems Science, Chinese Academy of Sciences

1979 was an important year in China. Many major events took place in this year, and it is also regarded as an important turning point in China's politics, economy, science and technology, culture and other fields and one of the important period breakpoints in modern Chinese history. Compared with the magnificent new era opened in 1979, the start of artificial intelligence (AI) research in China in 1979 can only be regarded as an inconspicuous wave in the historical tide, but in the history of artificial intelligence in China, This is a groundbreaking event.

The earliest school of artificial intelligence was the school of symbolism. Most of the earliest artificial intelligence scientists were mathematicians and logicians. They combined computers with their own research after the birth of computers, thus entering the field of artificial intelligence. In China, it was also mathematicians who opened the first page of artificial intelligence research. In 1979, whether it was the "Wu Method" in machine proofs that went to the world, or the holding of the Computer Science Summer Symposium comparable to the Dartmouth Conference, there were mathematicians behind it. It is also from this year that China's artificial intelligence has started to catch up with the world.

The proposer of "Wu Method" is none other than the mathematician Wu Wenjun. Together with Wang Xianghao and Zeng Xianchang, he is called the "Three Masters of Machine Proof". In the late 1970s, Wu Wenjun, who was nearly sixty years old, started from the study of ancient Chinese mathematics and created a new field of mathematical mechanization. He proposed the "Wu Method" for proving geometric theorems with computers, which is considered a pioneering work in the field of automatic reasoning.

1. Wu Wenjun opened the door for China's artificial intelligence to go to the world

In January 1979, at the invitation of the Institute for Advanced Study in Princeton, mathematician Wu Wenjun boarded an exchange flight to the United States with $25,000 in his pocket.

He was accompanied by mathematician Chen Jingrun. The two are the first batch of scientists invited to study and visit the United States after the establishment of diplomatic relations between China and the United States. They will study and exchange at the Institute for Advanced Study in Princeton for a period of time. The topic of Chen Jingrun's exchange is naturally "1+2", and the main content of Wu Wenjun's exchange on this trip, in addition to his old profession of topology, is more about the history of ancient Chinese mathematics and mathematical mechanization. He wants to use the 25,000 yuan he brought Dollars buy a computer for the study of mathematical mechanization.

When Wu Wenjun won the first prize of natural science from the Chinese Academy of Sciences (hereinafter referred to as "Chinese Academy of Sciences") in 1979, mathematical mechanization had become his main research direction. This research direction has also attracted the attention of the world. Wu Wenjun's research method is called "Wu Method" in the field of machine theorem proving. The highest award of China's intelligent science and technology "Wu Wenjun Artificial Intelligence Science and Technology Award" uses Wu Wenjun's name to commemorate Wu Wenjun as a Achievements of Chinese researchers in AI-related fields.

Inadvertently, Wu Wenjun opened the door for China's artificial intelligence research to go global. Wu Wenjun's research on the history of ancient Chinese mathematics began around 1974. At that time, Guan Zhaozhi, deputy director of the Institute of Mathematics of the Chinese Academy of Sciences (hereinafter referred to as the "Institute of Mathematics of the Chinese Academy of Sciences"), asked Wu Wenjun to study ancient Chinese mathematics. Wu Wenjun quickly discovered the important difference between the ancient Chinese mathematical tradition and the modern Western mathematical tradition inherited from ancient Greece. He conducted a thorough analysis of ancient Chinese arithmetic and developed unique insights in many aspects.

In the 1970s, foreign academic exchanges began to gradually recover. In 1975, Wu Wenjun went to France for exchange and gave a report on ancient Chinese mathematical thought at the French Institute of Advanced Science. At this time, Wu Wenjun had restored the ancient proof of Rigao's formula, and noticed the "structural" and "mechanistic" characteristics of ancient Chinese mathematics. In the Spring Festival of 1977, Wu Wenjun verified the feasibility of the geometric theorem machine proof method by hand calculation, and the process lasted for two months.

The original idea of machine theorem proving comes from Gottfried Wilhelm Leibniz's calculus reasoner, and later evolved from symbolic logic. Later, David Hilbert (David Hilbert) launched the "Hilbert Project" in 1920 on this basis, hoping to strictly axiomatize the entire mathematical system. Simply put, if this plan is realized, it means that for any mathematical conjecture, no matter how difficult it is, we can always know whether the conjecture is correct, and prove or deny it. This is what Hilbert meant when he said "Wir müssen wissen, wir werden wissen" (we must know, we must know).

However, shortly thereafter, in 1931, Kurt Gödel proposed Gödel's incompleteness theorem, which shattered Hilbert's ideals of formalism. But anyway, when Gödel closed the door, he still left a window. The doctoral dissertation of French genius mathematician Jacques Herbrand laid the foundation for the proof theory and recursion theory of mathematical logic. After Godel’s incompleteness theorem was proposed, Herbrand checked his thesis and left In a word - Gödel and my results are not contradictory, and I wrote a letter to Gödel for advice. Gödel replied to Erblan, but Erblan failed to wait for the letter. He died in a mountaineering accident two days after Gödel replied at the age of 23. Later, the highest award in the field of theorem proving was also named after El Brown, and Wu Wenjun won the fourth El Brown Award for Outstanding Achievement in Automatic Reasoning in 1997.

Other mathematicians have supplemented Gödel's theorem. Shortly after Gödel proved that "first-order integers (arithmetic) are undecidable", Alfred Tarski proved "first-order real numbers (geometric and algebraic) are decidable", This also lays the groundwork for machine proofs.

In 1936, Turing in his important paper "On Computable Numbers, with an Application to the Entscheidungsproblem" (On Computable Numbers, with an Application to the Entscheidungsproblem) of Gödel's 1931 proof and computation restrictions As a result, the discussion was reworked, and Gödel's formal language based on general arithmetic was replaced by a simple form of abstract device now called a Turing machine, and it was proved that all computable processes can be simulated by a Turing machine. This is also an important theoretical basis for computer science and artificial intelligence. The earliest school of artificial intelligence - the symbol school is also extended on the basis of formal logic operations.

Going back to Wu Wenjun, he worked in the Beijing Radio No. 1 Factory that produced computers in the 1970s, and at that time he started to get in touch with computers and machine theorem proving. "How to make full use of the power of the computer and apply it to his own mathematics research" has become what Wu Wenjun is interested in. Later, Wu Wenjun began to study the history of ancient Chinese mathematics, and summarized the geometric algebraic tendency and algorithmic thinking of ancient Chinese mathematics. After discovering the different ways of thinking between ancient Chinese mathematics and Western mathematics, he decided to use a different method to do machine proofs of geometric theorems.

At that time, Wu Wenjun read many foreign articles and fully understood the machine proof. At that time, the most cutting-edge research on machine theorem proving came from mathematical logician Wang Hao. During his studies in the Department of Mathematics of Southwestern Associated University, he studied under the famous philosopher and "the first person in Chinese philosophy" Jin Yuelin, and then went to Harvard University in the United States. The famous philosopher and logician Willard von Quinn (WV Quine) studied the formal axiom system founded by Quine and obtained a doctorate. As early as 1953, Wang Hao had already started thinking about the possibility of proving mathematical theorems with machines.

In 1958, Wang Hao used a propositional logic program on an IBM 7041 computer to prove all the first-order logic theorems in "Principles of Mathematics", and completed the proof of all 200 propositional logic theorems in the following year. The significance of Wang Haozhi's work lies in announcing the possibility of using computers to prove theorems. When he returned to China in 1977, he participated in several symposiums affecting the long-term development of my country's science and technology, and gave 6 special lectures at the Chinese Academy of Sciences, which had a significant impact on domestic machine proof research.

Closer to home, there is still a gap between Wang Hao’s previous proofs of propositional logic theorems in "Principles of Mathematics" and the machine proofs of geometric theorems that Wu Wenjun wants to achieve. The former has more symbolic logic components, while the latter has reasoning components. . At that time, there were many studies abroad on machine proofs of geometric theorems, but all ended in failure.

Second, from the mechanization of ancient Chinese mathematical thought to the "Wu Method"

In Wu Wenjun's view, the experience of failure is also very important, it will tell you which roads will not work. Inspired by Descartes' thought, he transformed geometrical problems into algebraic problems by introducing coordinates, and then mechanized it according to ancient Chinese mathematical thinking. Wu Wenjun even combined Cartesian thought with ancient Chinese mathematical thought, and proposed a route to solve general problems:

All problems can be transformed into mathematical problems, all mathematical problems can be transformed into algebraic problems, all algebraic problems can be transformed into problems of solving equations, and all problems of solving equations can be transformed into solving single variables Algebraic equation problems.

Ancient Chinese mathematics and Western modern mathematics are two different systems. Wu Wenjun restored the "Zhou Bi Suan Jing" according to the knowledge and customary thinking and reasoning of the ancients at that time without using "modern tools" such as trigonometric functions, calculus, factorization, and high-order equation solutions in modern mathematics. The proof methods of "Rigao Tushuo", "Dayanqiuyishu" and "Zengchengkaifangshu" in "Nine Chapters of Shushu". He believes that ancient Chinese mathematics has its own unique features. Qin Jiushao's method has the characteristics of construction and mechanization, and the numerical solution of high-order algebraic equations can be obtained with a small calculator. In the absence of high-performance computing equipment at that time, Wu Wenjun was able to make full use of ancient Chinese mathematical ideas to conduct research on dimensionality reduction, which is also commendable.

The first theorem Wu Wenjun proved according to this idea was Feuerbach's theorem, which proved that "the nine-point circle of a triangle is tangent to its inscribed circle and three circumscribed circles". This is one of the most beautiful theorems in plane geometry, which can be seen in Wu Wenjun's aesthetics. There was no computer at that time, so Wu Wenjun calculated by hand. One of the characteristics of "Wu's method" is that a large number of polynomials will be generated. The largest polynomial involved in the proof process has hundreds of items. This calculation is very difficult, and any error in one step will cause subsequent calculations to fail. In the Spring Festival of 1977, Wu Wenjun successfully verified the method of geometric theorem machine proof for the first time by hand calculation. Later, Wu Wenjun proved Simson's theorem on a Great Wall 203 produced by Beijing Radio No. 1 Factory.

Wu Wenjun published the related research article "Elementary Geometry Determination Problems and Mechanized Proof" in "Chinese Science" in 1977, and sent the article to Wang Hao. Wang Hao spoke highly of Wu Wenjun's work, and wrote back to suggest that Wu Wenjun use the existing algebra package and consider implementing Wu's method with a computer. Wang Hao did not realize the difference between the computers used by the top scholars in China and the United States at this time: the Great Wall 203 can use machine language, but the instruction systems of different computers are not universal, and it is not feasible to use the existing algebra package. So, later, Wu Wenjun simply borrowed a small calculator from the Institute of Mathematics of the Chinese Academy of Sciences as a gift from a foreigner who visited the Institute of Mathematics of the Chinese Academy of Sciences, converted the given proposition into an algebraic form, and then used Qin Jiushao's method to calculate the higher-order equation. untie.

Wu Wenjun's research on the machine proof of geometric theorems was strongly supported by Guan Zhaozhi. Guan Zhaozhi had studied in France and was one of the founders of the French branch of the Chinese Association of Scientists. He united a group of outstanding patriotic intellectuals, and Wu Wenjun was one of them. At that time, the Institute of Mathematics of the Chinese Academy of Sciences where Wu Wenjun worked had complicated relationships. One faction believed that doing machine proofs was "rebellious", and hoped that he would continue to engage in topology research; Guan Zhaozhi, who had transferred from topology and functional analysis to control theory, was particularly supportive and understood him. Let's say that Wu Wenjun can do whatever he wants. Later, when Guan Zhaozhi established the Institute of Systems Science of the Chinese Academy of Sciences in 1979, Wu Wenjun followed Guan Zhao to the Institute of Systems Science of the Chinese Academy of Sciences (Figure 1-1).

Figure 1-1 The original office building of the Institute of Systems Science, Chinese Academy of Sciences (now Rongke Building) in the early 1980s (from left: Xu Guozhi, Wu Wenjun, Indian scholar, Guan Zhaozhi)

To prove more complicated theorems, better machines are needed. Academician Wang Dezhao, then director of the Institute of Acoustics of the Chinese Academy of Sciences, gave advice to Wu Wenjun. He told Wu Wenjun when and where Li Chang, secretary of the party group and vice president of the Chinese Academy of Sciences, would appear, but Wu Wenjun really caught him. Li Chang was very open-minded. When he served as the president of Harbin Institute of Technology (hereinafter referred to as "HIT") in the 1950s, he turned HIT into a national first-class university. Among the six national key universities identified in 1954, Harbin Institute of Technology is the only one not located in Beijing. Li Chang also gave great support to Wu Wenjun's work. Wu Wenjun's foreign exchange of 25,000 US dollars to buy a computer in the United States was specially approved by Li Chang. With this computer, many theorems were quickly proved.

The 1970s were also the golden age of machine theorem proving. In 1976, two American mathematicians proved the four-color theorem by using a high-speed electronic computer with 1200 hours of calculation time, and solved the difficult problem that mathematicians had not solved for more than 100 years. The reason why the four-color theorem can be proved is that irreducible sets and unavoidable sets are finite. The "map coloring" problem of the four-color theorem seems to have infinitely many maps, but in fact they can be attributed to more than 2000 kinds Basic shapes, and then use the computing power of the computer to brute force and prove them one by one. Metaphorically speaking, this approach is like solving a Rubik's cube—taking the cube apart and putting it back together—inelegant but effective. We now say that GPT-3 "makes miracles with great effort", but in fact the proof of the four-color theorem is the ancestor of "miracles with great efforts".

However, this practice of using computer computing power to brute force theorem proofs cannot be generalized. The first step in theorem proving, the formalization of the theorem, requires a complete and rigorous formulation. On this point, there is a little story about a mathematician. An astronomer, a physicist and a mathematician traveled to Scotland by train. They saw a black sheep outside the window. The astronomer began to sigh: "Why are all sheep in Scotland black?" The physicist corrected: " It should be said that some sheep in Scotland are black." And the most rigorous expression comes from mathematicians: "In Scotland there exists at least one world, and there is at least one sheep, and this sheep is black on at least one side." There is another joke , said that mathematical problems are divided into two categories: one is "this also needs to be proved?", and the other is "this can also be proved?". From this we can see how difficult it is for a proof to be recognized by other mathematicians. Similarly, to formalize a theorem in an interactive theorem prover, it is necessary to fill in all the technical details in order to complete the "automation" of reasoning, and finally replace the theorem with a feasible but computationally intensive problem-solving idea. prove. In other words, this method still relies on mathematicians' understanding of theorems, and can only achieve "one theory and one proof", which can only be regarded as computer-aided proofs of theorems.

Therefore, after the four-color theorem was proved by computer, a group of logicians including Wang Hao put forward different opinions: Has the four-color theorem been proved? This kind of proof method is regarded as traditional proof, and the computer only plays the role of auxiliary calculation. It was not until 2005 that Georges Gonthier completed the complete computerized proof of the four-color theorem, and every step of its logical derivation was completed by a computer. At present, people have proved hundreds of mathematical theorems with computers, but most of these theorems are known, and "machine intelligence" has not yet made a real contribution to mathematics.

Machine theorem proving relies on algorithms. In the early stage, researchers often tried to find a super algorithm to solve all problems, but Wu Wenjun applied ancient Chinese mathematical ideas to the field of machine proof of geometric theorems, achieving "one type, one proof". This point was also agreed by Wang Hao. He believed that his early work had something in common with the method used by Wu Wenjun, that is, first find a relatively controllable subfield, and then find the most effective algorithm according to the characteristics of this subfield. When Wu Wenjun visited the United States in 1979, he also went to Rockefeller University to visit Wang Hao. His work was valued in the field of machine theorem, which had a certain relationship with Wang Hao's strong recommendation.

The "Wu method" really spread, making the first breakthrough in machine theorem proving in the 1980s, thanks to Zhou Xianqing, an overseas student in the United States who had listened to Wu Wenjun's machine theorem proving course. Zhou Xianqing originally wanted to take Wu Wenjun's graduate degree in the field of machine proof, but he thought that differential geometry was his weakness, so he was afraid that he would not be able to pass the exam, so he finally got admitted to the University of Science and Technology of China (hereinafter referred to as "University of Science and Technology of China"), and later went to the Institute of Computing Technology of the Chinese Academy of Sciences as Dai Pei, In this regard, I audited Wu Wenjun's geometric proof course.

In 1981, Zhou Xianqing went to the University of Texas at Austin to study abroad. At that time, the University of Texas at Austin was known as the king of theorem proving. Zhou Xianqing mentioned Wu Wenjun's work to Robert Boyer. Boyer thought it was very fresh, so he continued to ask, but Zhou Xianqing only knew that it was transforming geometry into algebra, and could not explain the specific details.

After that, Woody Bledsoe asked Zhou Xianqing and another student Wang Tiecheng to collect data. Zhou Xianqing's doctoral thesis was the realization of Wu's method. Wu Wenjun quickly sent two articles, both of which he signed to Bledsoe. In the next two years, these two articles were copied by the University of Texas at Austin nearly a hundred times and sent to all over the world, and the Wu method became widely known.

In 1983, the National Academic Conference on Proving Theorems by Machines was held in Colorado, USA. Zhou Xianqing gave a report entitled "Proving Geometry Theorems Using Wu's Method" at the conference. The general program developed by Zhou Xianqing can automatically prove more than 130 geometric theorems, including proofs of more difficult theorems such as Moller's theorem, Simson's theorem, Feuerbach's nine-point circle theorem and Desargues' theorem. Afterwards, the collection of papers of this conference was officially published in 1984 as the 29th volume of the series "Contemporary Mathematics" in the United States, and two related papers sent by Wu Wenjun were also included in it.

In June 1986, Turing Award winner John Hopcroft (John Hopcroft) and others organized a seminar on automatic geometric reasoning, and part of the report of the seminar was included in the "Artificial In the special edition of "Intelligence", the introduction article of the special edition specially introduces the new method of algebraic geometry proposed by Wu Wenjun. Vision, solid modeling) also have important application value (Figure 1-2). Since then, Hopcroft has worked closely with many universities in China. He has research institutes led by him in Shanghai Jiao Tong University, Peking University, and the Chinese University of Hong Kong (Shenzhen). Wu Wenjun and Wu Fafang are probably the beginning of his Chinese complex .

Figure 1-2 An overview of Wu's method in the opening chapter of the special edition of "Artificial Intelligence" in 1988