The beginning of China's artificial intelligence is closely related to this mathematician

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

Lin Jun Cenfeng | Written by

1979 was an important year in China. Many major events took place in this year, which 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 points in China's modern history. Compared with the magnificent new era opened in 1979, the start of China's artificial intelligence (AI) research in 1979 can only be regarded as an inconspicuous wave in the tide of history, but in the history of China's artificial intelligence, this is a groundbreaking event.

The earliest school of artificial intelligence was the symbolism school. Most of the earliest artificial intelligence scientists were mathematicians and logicians. After the birth of computers, they combined computers with their own research and entered 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 proof going global or the holding of the Computer Science Summer Symposium comparable to the Dartmouth Conference, there were mathematicians behind it. It was also from this year that China's artificial intelligence began to catch up with the world.

The originator of the "Wu Method" is the mathematician Wu Wenjun. He, Wang Xianghao and Zeng Xianchang are known as the "Three Heroes of Machine Proof". In the late 1970s, Wu Wenjun, who was nearly 60 years old, started from the study of ancient Chinese mathematics and pioneered a new field of mathematical mechanization. He proposed the "Wu Method" for proving geometric theorems with computers, which is considered to be a pioneering work in the field of automatic reasoning.

1. Wu Wenjun opened the door for China’s artificial intelligence to go global

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

Accompanying him was mathematician Chen Jingrun. The two were the first group 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 ideas at the Institute for Advanced Study in Princeton for a period of time. The theme of Chen Jingrun's exchange was naturally "1+2", and the main content of Wu Wenjun's exchange, in addition to his old profession of topology, was more about the history of ancient Chinese mathematics and mathematical mechanization. He wanted to use the 25,000 US dollars he brought with him to buy a computer for the research of mathematical mechanization.

When Wu Wenjun won the first prize in natural sciences from the Chinese Academy of Sciences (CAS) in 1979, mathematical mechanization had become his main research direction. This research direction has also attracted worldwide attention. Wu Wenjun's research method is known as the "Wu Method" in the field of machine theorem proving. The highest award in China's intelligent science and technology, the "Wu Wenjun Artificial Intelligence Science and Technology Award", uses Wu Wenjun's name to commemorate his achievements as a Chinese researcher in the field of artificial intelligence.

Unintentionally, Wu Wenjun opened the door for Chinese 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 "CAS Institute of Mathematics"), asked Wu Wenjun to study ancient Chinese mathematics. Wu Wenjun quickly discovered the important differences 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 produced unique insights in many aspects.

In the 1970s, foreign academic exchanges began to gradually resume. In 1975, Wu Wenjun went to France for exchanges and gave a report on ancient Chinese mathematical thought at the French Institute of Advanced Scientific Research. At this time, Wu Wenjun had restored the ancient proof of the Sundance formula and noticed the "constructive" and "mechanized" characteristics of ancient Chinese mathematics. During the Spring Festival of 1977, Wu Wenjun verified the feasibility of the machine proof method of geometric theorems by hand calculation, which took two months.

The original idea of ​​machine theorem proving came from Gottfried Wilhelm Leibniz's calculus inference machine and the symbolic logic that evolved from it. Later, David Hilbert launched the "Hilbert Plan" in 1920 based on this, 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 by "Wir müssen wissen, wir werden wissen" (We must know, we will know).

However, shortly thereafter, in 1931, Kurt Gödel proposed Gödel's incompleteness theorem, which completely shattered Hilbert's formalist ideals. But in any case, Gödel left a window when he closed the door. The doctoral dissertation of the French genius mathematician Jacques Herbrand laid the foundation for the proof theory and recursion theory of mathematical logic. After Gödel's incompleteness theorem was proposed, Herbrand checked his thesis and left a sentence-Gödel and my results are not contradictory, and wrote a letter to Gödel for advice. Gödel replied to Herbrand, but Herbrand did not wait for the letter. He died in a mountaineering accident two days after Gödel's reply at the age of 23. Later, the highest award in the field of theorem proof was also named after Herbrand. Wu Wenjun won the fourth Herbrand Award for Outstanding Achievements in Automated Reasoning in 1997.

Other mathematicians also supplemented Gödel's theorem. Shortly after Gödel proved that "first-order integers (arithmetic) are undecidable", Alfred Tarski proved that "first-order real numbers (geometry and algebra) are decidable", which also laid the foundation for machine proof.

In 1936, Turing re-examined Gödel's proof and computational limitations in his important paper "On Computable Numbers, with an Application to the Entscheidungsproblem", and replaced Gödel's formal language based on universal arithmetic with a simple abstract device now called a Turing machine, proving that all computable processes can be simulated by a Turing machine. This is also an important theoretical foundation for computer science and artificial intelligence. The earliest school of artificial intelligence, the symbolic school, was also extended on the basis of formal logic operations.

Let’s talk about Wu Wenjun. In the 1970s, he worked at Beijing Radio Factory No. 1, which produced computers. At that time, he began to get in touch with computers and machine theorem proving. “How to make full use of the power of computers and apply them to my own mathematical research” became Wu Wenjun’s interest. 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 ideas between ancient Chinese mathematics and Western mathematics, he decided to use a different method to do machine proof of geometric theorems.

At that time, Wu Wenjun read a lot of foreign articles and fully understood machine proof. At that time, the most cutting-edge research on machine theorem proof came from mathematical logician Wang Hao. While studying at the Department of Mathematics of Southwest Associated University, he studied under the famous philosopher and "the first person in Chinese philosophy" Jin Yuelin. Later, he went to Harvard University in the United States to study the formal axiom system created by Quine under the tutelage of the famous philosopher and logician Willard von Quine (WV Quine) and obtained a doctorate. As early as 1953, Wang Hao had begun to think about the possibility of using machines to prove mathematical theorems.

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". The following year, he completed the proof of all 200 propositional logic theorems. The significance of Wang Hao's work is that it announced the possibility of theorem proof using computers. When he returned to China in 1977, he participated in many seminars that influenced the long-term development of science and technology in my country, and gave 6 special lectures at the Chinese Academy of Sciences, which had a significant impact on domestic machine proof research.

Back to the point, there was a gap between Wang Hao's previous proof of the propositional logic theorem in "Principles of Mathematics" and Wu Wenjun's machine proof of the geometry theorem. The former was more symbolic logic, while the latter was more reasoning. At that time, there were many studies on machine proof of geometry theorem abroad, but they all ended in failure.

2. 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, because it will tell you which roads are not feasible. Inspired by Descartes's ideas, he introduced coordinates to transform geometric problems into algebraic problems, and then mechanized them according to ancient Chinese mathematical ideas. Wu Wenjun even combined Descartes' ideas with ancient Chinese mathematical ideas 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 systems of equations, and all problems of solving systems of equations can be transformed into problems of solving algebraic equations with a single variable.

Ancient Chinese mathematics and modern Western mathematics are two different systems. Without the help of modern tools such as trigonometric functions, calculus, factorization, and solutions to higher-order equations, Wu Wenjun restored the proof methods of "Ri Gao Tu Shuo", "Da Yan Qiu Yi Shu", and "Zeng Cheng Kai Fang Shu" in "Zhou Bi Suan Jing" and "Shu Shu Jiu Zhang" according to the ancients' knowledge and conventional thinking. He believes that ancient Chinese mathematics has its own unique features. Qin Jiushao's method is constructive and mechanizable, 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 the time, Wu Wenjun was able to make full use of the dimensionality reduction of ancient Chinese mathematical thinking for research, which is also a rare thing.

The first theorem that Wu Wenjun proved according to this line of thought was Feuerbach's theorem, which proved that "the nine-point circle of a triangle is tangent to its incircle and three circumcircles". This is one of the most beautiful theorems in plane geometry, and Wu Wenjun's aesthetic taste is evident. At that time, there were no computers, so Wu Wenjun calculated by hand. A feature of the "Wu method" is that a large number of polynomials will be generated. The largest polynomial involved in the proof process has hundreds of terms. This calculation is very difficult, and any mistake in any step will lead to the failure of subsequent calculations. During the Spring Festival of 1977, Wu Wenjun successfully verified the method of machine proof of geometric theorems by hand calculation for the first time. Later, Wu Wenjun proved Simson's theorem on a Great Wall 203 produced by Beijing Radio Factory No. 1.

Wu Wenjun published the relevant research article "Elementary Geometry Decision Problem and Mechanized Proof" in "Science China" in 1977 and sent the article to Wang Hao. Wang Hao highly praised Wu Wenjun's work and wrote back to suggest that Wu Wenjun use the existing algebraic package to consider using a computer to implement Wu's method. Wang Hao did not realize the difference between the computers used by the top scholars in China and the United States at that time: Great Wall 203 can use machine language, but the instruction systems of different computers are not universal, and the existing algebraic packages will not work. Therefore, later Wu Wenjun simply borrowed a small calculator from the Institute of Mathematics of the Chinese Academy of Sciences, which was given by a foreigner who visited the Institute of Mathematics of the Chinese Academy of Sciences, converted the given proposition into algebraic form, and then used Qin Jiushao's method to calculate the solution of the high-order equation.

Wu Wenjun's research on machine proof of geometric theorems received strong support from 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 relationship in the Institute of Mathematics of the Chinese Academy of Sciences where Wu Wenjun worked was complicated. One faction believed that doing machine proof was "heretical" and hoped that he would continue to engage in topological research; Guan Zhaozhi, who switched from topology and functional analysis to control theory, was particularly supportive and understanding of him, and said that he would let Wu Wenjun do whatever he wanted. Later, when Guan Zhaozhi "set up a new camp" in 1979 and established the Institute of Systems Science of the Chinese Academy of Sciences, Wu Wenjun also followed Guan Zhaozhi to the Institute of Systems Science of the Chinese Academy of Sciences (Figure 1-1).

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

To prove more complex theorems, better machines are needed. Academician Wang Dezhao, then director of the Institute of Acoustics of the Chinese Academy of Sciences, gave Wu Wenjun guidance. He told Wu Wenjun when and where Li Chang, secretary of the Party Committee and vice president of the Chinese Academy of Sciences, would appear, and Wu Wenjun really waited for him. Li Chang was very open-minded. During his tenure as president of Harbin Institute of Technology (hereinafter referred to as "HIT") in the 1950s, he made HIT a first-class university in the country. Among the six key universities in the country determined in 1954, HIT was the only one not in Beijing. Li Chang also gave great support to Wu Wenjun's work. The $25,000 in foreign exchange that Wu Wenjun used to buy a computer in the United States was specially approved by Li Chang. With this computer, many theorems were quickly proved.

The 1970s was also the golden age of machine theorem proving. In 1976, two American mathematicians used a high-speed electronic computer to spend 1,200 hours of computing time to prove the four-color theorem, solving a problem that mathematicians had not been able to solve for more than 100 years. The four-color theorem can be proved because irreducible sets and inevitable sets are finite. The "map coloring" problem of the four-color theorem seems to have an infinite number of maps, but in fact they can be reduced to more than 2,000 basic shapes, and then the computing power of the computer is used to violently enumerate and prove them one by one. For example, this method is like restoring the Rubik's Cube - taking the Rubik's Cube apart and putting it back together - although it is not elegant, it is indeed effective. We now say that GPT-3 "works hard to produce miracles", but in fact, the proof of the four-color theorem is the ancestor of "works hard to produce miracles".

However, this practice of using computer computing power to brute force theorem proof cannot be promoted. The first step of theorem proof, that is, the formalization of theorem, requires a complete and rigorous expression. Regarding this, there is a short story about a mathematician. An astronomer, a physicist and a mathematician took a train to Scotland. They saw a black sheep outside the window. The astronomer began to sigh: "Why are all the sheep in Scotland black?" The physicist corrected: "It should be said that some sheep in Scotland are black." The most rigorous expression comes from the mathematician: "There is at least one piece of heaven and earth in Scotland, at least one sheep, and at least one side of this sheep is black." There is also a joke that says that mathematical problems are divided into two categories: one is "Does this also need to be proved?", and the other is "Can this 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, all technical details need to be filled in to complete the "automation" of reasoning, and finally replace the proof of the theorem with a feasible but computationally intensive problem-solving idea. In other words, this method still relies on mathematicians' understanding of theorems and can only achieve "one theory, one proof", which can only be regarded as a computer-assisted proof of the theorem.

Therefore, after the four-color theorem was proved by computer, a group of logicians including Wang Hao expressed different opinions: Is the four-color theorem proved? This proof method is considered a traditional proof, and the computer only played an auxiliary role in calculation. It was not until 2005 that Georges Gonthier completed the entire computerized proof of the four-color theorem, and each step of the logical deduction was completed by the 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 stages, researchers often tried to find a super algorithm to solve all problems, while Wu Wenjun applied ancient Chinese mathematical ideas to the field of machine proof of geometric theorems, achieving "one proof for one category". This point was also agreed by Wang Hao, who believed that his early work and the method used by Wu Wenjun had something in common, that is, first find a relatively controllable subfield, and then find the most effective algorithm based on the characteristics of this subfield. When Wu Wenjun visited the United States in 1979, he also went to Rockefeller University to visit Wang Hao. The fact that his work was valued in the machine theorem community was also related to Wang Hao's strong recommendation.

The spread of the "Wu Method" and the first breakthrough in machine theorem proving in the 1980s were all due to Zhou Xianqing, an American student who had attended Wu Wenjun's machine theorem proving course. Zhou Xianqing wanted to apply for a postgraduate degree in Wu Wenjun's machine proof, but he thought differential geometry was his weak point and was afraid that he would not pass the exam. He eventually passed the exam and was admitted to the University of Science and Technology of China (hereinafter referred to as "USTC"), and later went to the Institute of Computing Technology of the Chinese Academy of Sciences for training, and thus audited Wu Wenjun's geometry proof course.

In 1981, Zhou Xianqing went to study abroad at the University of Texas at Austin. At that time, the University of Texas at Austin was the king of theorem proving. Two research groups at the university had won the highest award for theorem proving, the Herbrand Prize. Zhou Xianqing mentioned Wu Wenjun's work to Robert Boyer, who found it very interesting and continued to ask questions, but Zhou Xianqing only knew that it was to transform geometry into algebra, and could not explain the specific details.

After that, Woody Bledsoe asked Zhou Xianqing and another student, Wang Tiecheng, to collect information. Zhou Xianqing's doctoral dissertation was the implementation of Wu's method. Wu Wenjun soon sent two articles, both of which were signed by him to Bledsoe. In the following two years, the two articles were copied nearly a hundred times by the University of Texas at Austin and sent to all parts of the world, and Wu's method began to become widely known.

In 1983, the National Theorem Proving Conference was held in Colorado, USA. Zhou Xianqing gave a report entitled "Using Wu's Method to Prove Geometric Theorems" at the conference. The general program developed by Zhou Xianqing can automatically prove more than 130 geometric theorems, including the proofs of more difficult theorems such as Mohler's Theorem, Simson's Theorem, Feuerbach's Nine-Point Circle Theorem and Desargues' Theorem. Later, the proceedings of this conference were officially published in 1984 as the 29th volume of the American "Contemporary Mathematics" series, and the two related papers sent by Wu Wenjun were also included.

In June 1986, John Hopcroft, a Turing Award winner, and others organized a seminar on automatic geometric reasoning. Some reports from the seminar were included in the December 1988 special issue of Artificial Intelligence. The introductory article of the special issue specifically introduced the new algebraic geometry method proposed by Wu Wenjun, believing that this method not only made a great contribution to the progress of geometric reasoning, but also had important application value in the three major application problems of artificial intelligence (robotics and motion planning, machine vision, and solid modeling) (Figure 1-2). Hopcroft has since worked closely with many Chinese universities, and has research institutes led by him at Shanghai Jiaotong University, Peking University, and the Chinese University of Hong Kong (Shenzhen). Wu Wenjun and Wu's method are probably the beginning of his Chinese complex.

An overview of Wu's method at the beginning of the 1988 special issue of Artificial Intelligence

——Interaction issues——

Do you understand the development of artificial intelligence in China?