1979 was an important year in China. This year has witnessed many major events, 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 breaking points in China's modern history. Compared with the magnificent new era opened in 1979, the beginning of Chinese intelligence (AI) research in 1979 can only be regarded as an inconspicuous wave in the historical tide, but in the history of Chinese intelligence, this is a groundbreaking event.
A still from the documentary Horizon Series: In Search of Artificial Intelligence (2012).
The earliest school of artificial intelligence was the symbolist school, and the earliest batch of artificial intelligence scientists were mostly mathematicians and logicians, who combined computers with their own research after the birth of computers to enter the field of artificial intelligence. In China, it was also mathematicians who turned the first page of artificial intelligence research. In 1979, whether it was the "Wu method" in machine proofs going to the world, or the computer science summer symposium comparable to the Dartmouth Conference, mathematicians were behind it. It was also from this year that Chinese Gong Intelligent began to catch up with the world.
"A Brief History of Chinese Worker Intelligence: From 1979 to 1993", by Lin Juncenfeng, People's Posts and Telecommunications Publishing House, August 2023.
Wu Wenjun pushed open the door for Chinese engineering intelligence research to the world
In January 1979, at the invitation of the Institute for Advanced Study in Princeton, mathematician Wu Wenjun boarded a flight to the United States with $25,000.
Accompanying him was the 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, and will study and exchange for a period of time at the Institute for Advanced Study in Princeton. The theme of Chen Jingrun's exchange is naturally "1+2", and the main content of Wu Wenjun's exchange, in addition to his old line of topology, is more about the history of ancient Chinese mathematics and mathematical mechanization, and he wants to use the 25,000 US dollars he carries to buy a computer for the research of mathematical mechanization.
When Wu Wenjun won the first prize in natural science of the Chinese Academy of Sciences (hereinafter referred to as the Chinese Academy of Sciences) 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 proof, and 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's achievements as a Chinese researcher in artificial intelligence-related fields.
Inadvertently, Wu Wenjun pushed open the door to the world of Chinese engineering intelligence research. 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, and analyzed the original and clean source of ancient Chinese arithmetic, and developed unique insights in many aspects.
In the 70s of the 20th century, 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 Advanced Scientific Research. By this time, Wu Wenjun had already restored the ancient proof of Hidaka formula, and noted the "constructive" and "mechanized" 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, a process that lasted two months.
The machine theorem proves that the original idea originated from Gottfried Wilhelm Leibniz's calculus inference and later evolved symbolic logic. Later, David Hilbert launched the "Hilbert Plan" in 1920, hoping to rigorize the entire mathematical system in a strict axiom. Simply put, if this plan is realized, it means that for any mathematical conjecture, no matter how difficult it is, we will always be able to know whether the conjecture is correct or not, and prove or disprove it. Hilbert meant by "Wirmüssen wissen, wir warden wissen" (we must know, we must know).
However, shortly thereafter, in 1931, Kurt Gödel proposed Gödel's incompleteness theorem, which completely shattered Hilbert's formalist ideal. But anyway, Gödel left a window when he closed the door. The doctoral thesis of the French genius mathematician Jacques Herbrand laid the foundation for the theory of proof and recursion of mathematical logic, and Elbrant, after Gödel's incompleteness theorem was proposed, checked his thesis and left a sentence - Gödel and I did not contradict the results, and wrote a letter to Gödel asking for advice. Gödel replied to Elblanc, but Elbron could not wait for the letter, and 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 proofs was also named after Elbron, and Wu Wenjun won the fourth Elbron Outstanding Achievement Award in Automatic Reasoning in 1997.
Other mathematicians 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 determinable," which also laid the foundation for machine proofs. In 1936, Turing revisited Gödel's 1931 results of the proof and computational limitations in his seminal paper On Computable Numbers, with an Application to the Entscheidungsproblem, and replaced Gödel's formal language based on universal arithmetic with an abstract device in simple form now called a Turing machine. It is proved that all computable processes can be simulated with a Turing machine. This is also an important theoretical basis for computer science and artificial intelligence. The earliest school of artificial intelligence, the semiotic school, is also extended on the basis of formal logic operations.
Going back to Wu Wenjun, he went to work at the Beijing Radio No. 1 Factory, which produced computers, in the 70s of the 20th century, and at that time he began to be exposed to computers and machine theorem proofs. "How to exert the power of computers and apply them to his own mathematical research" became Wu Wenjun's interest. Later, Wu Wenjun began to study the history of ancient Chinese mathematics, and summarized the geometric algebraization tendency and algorithmic ideas of ancient Chinese mathematics. After discovering the different ideas of ancient Chinese mathematics and Western mathematics, he decided to do machine proofs of geometric theorems in a different way.
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 proving came from the mathematical logician Wang Hao, who studied under the famous philosopher and "the first person in Chinese philosophy" Jin Yuelin during his studies in the Department of Mathematics of Southwest United University, and then went to Harvard University in the United States to study the formal axiom system created by Quinn under the famous philosopher and logician W.V. Quine (W.V. Quine) and obtained a doctorate. As early as 1953, Wang Hao began to think about the possibility of using machines to prove mathematical theorems.
In 1958, Wang Hao used a propositional logic program on a IBM7041 computer to prove all the first-order logic theorems in Principia Mathematica, and the following year completed the proof of all 200 propositional logic theorems. The significance of Wang Haozhi's work is to announce the possibility of using computers for theorem proofs. When he returned to China in 1977, he participated in a number of seminars that affected the long-term development of mainland science and technology, and gave six special speeches at the Chinese Academy of Sciences, which had a significant impact on domestic machine proof research. To get back to the point, there is still a gap between Wang Hao's previous proof of the propositional logic theorem in "Principles of Mathematics" and the machine proof of the geometric theorem that Wu Wenjun wants to achieve, the former has more components of symbolic logic, and the latter has elements of reasoning. At that time, there were many studies abroad on machine proofs of geometric theorems, but they all ended in failure.
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 Cartesian thought, he transformed geometric problems into algebraic problems by introducing coordinates, and then mechanized them according to ancient Chinese mathematical ideas. Wu Wenjun even combined Cartesian thought with ancient Chinese mathematical thought to propose a line for solving 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 solving systems of equations, and all problems solving systems of equations can be transformed into problems of algebraic equations solving single arguments.
Ancient Chinese mathematics and Western modern mathematics are two different systems. Without resorting to "modern tools" such as trigonometric functions, calculus, factorization, and higher-order equation solutions in modern mathematics, Wu Wenjun restored the proof methods of "Rigao Diagram Theory", "Great Derivation and Seeking One Technique" and "Multiplication Prescription Technique" in the "Zhou Qiu Suanjing" and "Nine Chapters of the Book of Numbers" according to the knowledge and customary thinking reasoning of the ancients at that time. He believed that ancient Chinese mathematics had its own uniqueness, and Qin Jiushao's method was structurable and mechanizable, and the numerical solution of higher-order algebraic equations could be found with a small calculator. In the absence of high-performance computing equipment at that time, Wu Wenjun's ability to make full use of ancient Chinese mathematical ideas to reduce dimensionality for research was also a valuable thing.
The first theorem that Wu Wenjun proved along this line of thought was Feuerbach's theorem, which proved that "the nine-point circle of a triangle is tangent to its inscribed circle and three paratangent circles". This is one of the most beautiful theorems in plane geometry, which can be seen in Wu Wenjun's aesthetic. At that time, there was no computer, so Wu Wenjun used his own hands to calculate it. A feature of the "Wu method" is that it produces a large number of polynomials, and the maximum polynomials involved in the proof process are hundreds of terms, which is very difficult to calculate, and any mistake in one step will lead to the failure of subsequent calculations. In the Spring Festival of 1977, Wu Wenjun successfully verified the method of machine proof of geometric theorems by hand arithmetic for the first time, and later, Wu Wenjun proved Simson's theorem on a Great Wall 2031 produced by Beijing Radio No. 1 Factory.
Wu Wenjun published the related research article "Elementary Geometry Determination Problems and Mechanized Proofs" in Science China in 1977 and sent the article to Wang Hao. Wang Hao spoke highly of Wu Wenjun's work, and replied that Wu Wenjun use the existing algebra package and 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 this time: the Great Wall 203 could use machine language, but the instruction systems of different computers were not universal, and it would not work to use existing algebraic packages. Therefore, 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 solution of higher-order equations.
Wu Wenjun's research on machine proof of geometric theorems has been strongly supported by Guan Zhaozhi. Guan Zhaozhi studied in France and was one of the founders of the French branch of the Chinese Association of Scientists, uniting a group of outstanding patriotic intellectuals, Wu Wenjun being one of them. At that time, Wu Wenjun's Institute of Mathematics of the Chinese Academy of Sciences had a complicated relationship, and some factions thought that doing machine proofs was "deviant" 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, saying that Wu Wenjun could do whatever he wanted. Later, when Guan Zhaozhi "set up a separate mountain" in 1979 and established the Institute of Systems Science of the Chinese Academy of Sciences, Wu Wenjun also followed Guan Zhao to the Institute of Systems Science of the Chinese Academy of Sciences.
In the early 80s of the 20th century, the former office building of the Institute of Systems Science of the Chinese Academy of Sciences (now Rongke Building) (from left: Xu Guozhi, Wu Wenjun, Indian scholar, Guan Zhaozhi, "Chinese Worker
A Brief History of Intelligence: From 1979 to 1993).
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, pointed out 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, and the result was really guarded by Wu Wenjun. Li Chang was very open-minded and built Harbin Institute of Technology into a first-class university in China when he was the president of Harbin Institute of Technology (hereinafter referred to as "Harbin Institute of Technology") in the 50s of the 20th century. Among the six key universities in China identified in 1954, HIT was the only one that was not located in Beijing. Li Chang also gave great support to Wu Wenjun's work, and the $25,000 foreign exchange that Wu Wenjun went to the United States to buy computers was specially approved by Li Chang. With this computer, many theorems were quickly proved.
The 70s of the 20th century were also the golden age of machine theorem proofs. In 1976, two American mathematicians proved the four-color theorem using 1,200 hours of computation time spent on high-speed electronic computers, solving a problem that mathematicians had failed to solve for more than 100 years. The reason why the four-color theorem can be proved is because the irreducible set and the inevitable set are finite, and 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 use the computing power of the computer to violently exhaust and prove them one by one. Metaphorically, this method is like restoring a Rubik's cube – taking it apart and putting it back together – which is not elegant but works. We now say that GPT-31 "vigorously produces miracles", in fact, the proof of the four-color theorem is the ancestor of "vigorous miracles".
However, this practice of brute-forcing theorem proofs using computer computing power cannot be generalized. The first step in the proof of the theorem, the formalization of the theorem, requires a complete and rigorous formulation. There is a little story about mathematicians about this. An astronomer, a physicist and a mathematician are traveling to Scotland by train, and they see a black sheep outside the window, and the astronomer begins to exclaim: "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: "There is at least one heaven and earth in Scotland, at least one sheep, and this sheep is black on at least one side." There is also a passage that says that mathematical problems are divided into two categories: one is "This is also to be proven?" One category is "Can this be proven?" ”。
This shows how difficult it is for a proof to be recognized by other mathematicians. Similarly, formalizing a theorem in an interactive theorem prover requires filling in all the technical details in order to complete the "automation" of reasoning, and eventually replace the proof of the theorem with a feasible but computationally intensive solution idea.
In other words, this method still relies on mathematicians' understanding of the theorem, and can only achieve "one theory and one proof", which can only be regarded as a computer-aided proof of the theorem. Therefore, after the four-color theorem was proved by the computer, a group of logicians including Wang Hao put forward different opinions: Has the four-color theorem been proved? This proof method is considered a traditional proof, and the computer only plays the role of auxiliary calculation. It wasn't until 2005 that Georges Gonthier completed the full computerized proof of the four-color theorem, with each step of its logical derivation done by a computer.
Hundreds of mathematical theorems have been proved by computers, but most of these theorems are known, and "machine intelligence" has not yet made a real contribution to mathematics. Machine theorem proofs rely on algorithms. In the early stages, researchers often try 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 class and one proof". This is also agreed by Wang Hao, who believes that his early work and the method used by Wu Wenjun have in common, 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 specially visited Wang Hao at Rockefeller University, and his work was valued in the machine theorem community and had a certain relationship with Wang Hao's recommendation.
The "Wu method" really spread, allowing machine theorem proof to make the first breakthrough in the 80s of the 20th century, thanks to an international student in the United States who had listened to Wu Wenjun's machine theorem proof course - Zhou Xianqing. Zhou Xianqing originally wanted to take the graduate school of Wu Wenjun's machine proof, but he thought that differential geometry was his weakness and was afraid that he would not be able to pass the exam, so he was finally admitted to the University of Science and Technology of China (hereinafter referred to as "the University of Science and Technology of China"), and later went to the Institute of Computing Technology of the Chinese Academy of Sciences to take a training fee, and audited Wu Wenjun's geometry proof course.
In 1981, Zhou Xianqing went to study at the University of Texas at Austin, which at that time was the king of theorem proofs, and both research groups at the university had won the Hebrand Prize, the highest award for theorem proof. Zhou Xianqing mentioned Wu Wenjun's work to Robert Boyer, and Boyer felt that it was very new and continued to ask, but Zhou Xianqing only knew that he was converting geometry into algebra, and the specific details could not be explained.
Woody Bledsoe then asked Zhou Xianqing and another student, Wang Tiecheng, to collect information, and Zhou's doctoral dissertation was an implementation of Wu's method. Wu Wenjun quickly sent two articles, both with his signature to Bledsoe. In the two years that followed, the two articles were copied nearly a hundred times by the University of Texas at Austin and sent around the world, and Wu's method became widely known.
In 1983, the National Conference on Machine Proof of Theorems was held in Colorado, USA, and Zhou Xianqing gave a report entitled "Proving Geometric Theorems by Wu Method" at the conference. The general program developed by Zhou Xianqing can automatically prove more than 130 geometric theorems, including the proof of difficult theorems such as Moller's theorem, Simson's theorem, Feuerbach's nine-point circle theorem and Dislag's theorem. Later, the proceedings of this conference were officially published in 1984 as volume 29 of the American "Contemporary Mathematics" series, and two related papers sent by Wu Wenjun were also included.
In June 1986, Turing Award winner John Hopcroft and others organized a seminar on geometric automatic reasoning, part of the report of which was included in the December 1988 issue of "Artificial Intelligence" special issue, the introduction article of the special feature introduced the new method of algebraic geometry proposed by Wu Wenjun, believing that this method not only made great contributions to the progress of geometric reasoning, but also made great contributions to the three major application problems of artificial intelligence (robotics and motion planning, machine vision, Solid Modeling) also has important application value. Since then, Hopcroft has worked closely with many universities in China, and there are research institutions led by him at Shanghai Jiao Tong University, Peking University, and Hong Kong Chinese University (Shenzhen), and Wu Wenjun and the "Wu Method" are probably the beginning of his China complex.
The 1988 Artificial Intelligence special begins with an overview of Wu's method (illustrated in A Brief History of Chinese Intelligence: From 1979 to 1993).
Reservations for artificial intelligence: the school of mathematical mechanochemistry
Although these academic activities naturally and closely associate Wu Wenjun's name with the concept of artificial intelligence, Wu Wenjun himself still has reservations about the reference to "artificial intelligence". According to his words: "The program of artificial intelligence is written by my own hands one by one, each instruction is an action that must be executed mechanically, it has no intelligence at all, the so-called 'artificial intelligence' is the mechanical execution of human thinking process, not the computer has intelligence." Therefore, Wu Wenjun used Wang Hao's "mathematical mechanization" to describe his work. In his 1977 paper "The Problem of Elementary Geometric Determination and Mechanization Proof" published in Science in China, Wu Wenjun wrote a note to clarify the origin of mechanized ideas:
Our algorithms for mechanized proofs of elementary geometric theorems mainly involve the use of polynomial techniques, such as arithmetic operations and simple elimination. It should be noted that these were the creations of Chinese mathematicians during the Song and Yuan periods of the 12th-14th centuries, and at that time there was a fairly high degree of development. ...... In fact, the mechanization of geometric problems and the systematic solution of algebraic methods was one of the major achievements of Chinese mathematicians at that time, long before the advent of analytic geometry in the 17th century.
Artificial intelligence is an interdisciplinary discipline, and mathematics is naturally one of the basic disciplines related to artificial intelligence. But from the above statement, the purpose of Wu Wenjun's machine proof is to better prove and assist in the discovery of new mathematical theorems, which are two circles with the research of artificial intelligence. In the context of artificial intelligence being criticized and questioned at that time, Wu Wenjun's reservation of artificial intelligence was actually a self-preservation strategy for him, and Nick of Wuzhen Think Tank once said that Mr. Wu Wenjun was a "human spirit" among mathematicians.
At the "Computer Science Summer Seminar" held by Jilin University in 1979, although the content of artificial intelligence was discussed in groups, it was still called "intelligent simulation" to the outside world. Words are sensitive to deeds, which may be the reason why Wu Wenjun has not suffered a major impact. The "Wu method" opened the Chinese school of mathematical mechanization of automatic reasoning and equation solving. Since 1983, Wu Wenjun has been recruiting graduate students to study machine proof. Earlier students included Hu Sen (1983-1986, master's degree), Wang Dongming (1983-1987, Ph.D.), Gao Xiaoshan (1984-1988, Ph.D.), Liu Zhuojun (1986-1988, Ph.D.), and Li Ziming (1985-1988, Master's degree). This group of students later became the backbone of domestic mathematical mechanization research.
Influenced by Wu's method, there are also two talents of Peking University's numerical power system, Hong Jiawei and Zhang Jingzhong. At that time, Wu Wenjun's two earliest graduate students, Hu Sen and Wang Dongming, discovered that many figures, if drawn correctly, could be theorems. This was soon turned into a theorem by Honjawe, who used an example to prove a geometric theorem , also known as the single-point illustration method. Zhang Jingzhong is a student of the 1954 class of Peking University's Department of Mathematics, one level higher than Hong Jiawei (in fact, the 1955 class of Peking University's Department of Mathematics is also full of talents). Zhang Jingzhong was transferred to Xinjiang in 1957, and later when Peking University teachers looked for Zhang Jingzhong, they still learned from Hong Jiawei.
Another mathematician who had a deep friendship with Zhang Jingzhong was Yang Lu. In the sixties and seventies of the twentieth century, Zhang Jingzhong and Yang Lu discussed geometric algorithms and function iterations, and Yang Lu proposed to directly study the properties of geometric figures through the distance relationship between points, without establishing a coordinate system. This has something in common with Wu Wenjun's combination of ancient Chinese mathematical ideas and Cartesian thought. In 1979, Zhang Jingzhong was transferred to work at the Chinese University of Science and Technology, and in 1985, he was transferred to the Chengdu Mathematical Science Research Office of the Chinese Academy of Sciences, and Yang Lu also completed his work transfer almost at the same time. That is, at the end of the 70s of the 20th century, Zhang Jingzhong and Yang Lu began to enter the field of machine theorem proof.
In 1984, when Hong Jiawei conceived the illustration method, Zhang Jingzhong suggested with him that it is easier to implement with a set of examples than an example. In 1989, Zhang Jingzhong and Yang Lu developed Hongjiawei's method and proposed the numerical parallel method, and the ideas of the examples were different. Zhang Jingzhong's work was guided and supported by Wu Wenjun, and in May 1992, Zhang Jingzhong went to Wichita State University in the United States, and Wu Wenjun wrote a three-page English recommendation letter to Zhang Jingzhong. Another contribution of Zhang Jingzhong to Chinese intelligence was to cooperate with Xie Jinchao, the leading teacher of the 1990 mathematics comprehensive experimental class of Chengdu No. 7 Middle School, to do the realization of the machine theorem proof of Wu's method, and it was Xie Jinchao's proud protégé Wang Xiaochuan who was the gold medalist in IOI11996 and later founded Sogou as CEO.
Turning back to Wu Wenjun, Wu Wenjun has been committed to the research and promotion of mathematical mechanization since the 80s of the 20th century, and has been supported by Professor Cheng Minde of Peking University. Cheng Minde, Wu Wenjun and two other mathematicians Chen Shengshen and Hu Guoding are the proponents of "China's mathematics should be the first to catch up with the world's advanced level in the 21st century", and are the founders of the Mathematics Tian Yuan Fund, Cheng Minde's other identity is the deputy head of the information science group of the Department of Information Technology Science of the Chinese Academy of Sciences, and he and the leader of the information science group, Chang Yi, have made no small contribution to the development of China's informatization and artificial intelligence.
In early 1990, Cheng Minde directed the preparation of an international feedback material on machine proof research and submitted it to the leadership of the National Science and Technology Commission (hereinafter referred to as "Science and Technology Commission"). At that time, the research of the fifth generation of intelligent computers in Japan was once in a hot state, but finally abandoned due to major flaws in mathematical theories and methods, and the research of Wu's method is expected to provide new mathematical concepts for the development of intelligent computers. In June, the leaders of the Department of Basic Research and High Technology of the State Science and Technology Commission (hereinafter referred to as the "Basic Department") went to the Institute of Systems Science of the Chinese Academy of Sciences to discuss how to further support Wu Wenjun's machine proof work, and Wu Wenjun, Cheng Minde and others participated in the symposium. Shortly after the symposium, the Foundation Division allocated 1 million yuan to support the research of machine proof. With this grant, Wu Wenjun soon established the Mathematical Mechanization Research Center at the Institute of Systems Science of the Chinese Academy of Sciences, with Wu Wenjun as the director and Cheng Minde as the director of the academic committee, and the daily work was presided over by Wu Wenda of the Beijing Computing Center. Cheng Minde also collaborated with Academician Shi Qingyun to apply the Wu method to overall vision, and supervised graduate student Li Hongbo to create a new direction for machine proof of geometric theorems.
A still from "Artificial Intelligence: Fuxi Awakens" (2016).
After the establishment of the Research Center for Mathematical Mechanization, Wu Wenjun further studied the symbolic and numerical mixing algorithms from the perspective of application. He pointed out in the early 90s of the 20th century that symbolic computing and numerical computing are two different calculation methods to solve problems in the development of science and technology, symbolic computing can obtain accurate and complete solutions to problems, but the amount of calculation is large and the form of expression is often very complex; Numerical calculations can quickly deal with many practical application problems, but generally only local approximate solutions can be obtained.
Wu Wenjun once proposed that all engineering problems should eventually be transformed into mathematical problems, and all mathematical problems should eventually be transformed into equation solving problems, and the research of hybrid algorithms also provides an effective comprehensive method for solving optimization problems proposed by the Mathematical Mechanization Research Center in the follow-up mathematical mechanization and automatic reasoning platform and the National Key Basic Research and Development Program (973 Program) project "Mathematical Mechanization Methods in Mechanism and CNC Technology". In recent years, machine proofs have not only been used to prove and assist in the discovery of new mathematical theorems, but also created or developed new methods and algebraic tools to solve computer-aided design, robot control, computer vision, and other related mathematical problems.
Step out of the math circle and dedicate yourself to unleashing the power of computers
In addition to Wu Wenjun, there was another mathematician in China who was famous in the field of machine theorem proof, he was Wang Xianghao of Jilin University. Unlike Wu Wenjun, Wang Xianghao is not limited to applying computers to mathematical research, but jumps out of the mathematical circle and is committed to exerting the power of computers, which has played a key role in the systematic development of artificial intelligence.
Wang Xianghao was born in Anping County, Hebei Province in 1915 and loved mathematics since he was a child. In the summer of 1946, Wang Xianghao received a scholarship from the U.S. Department of State to study at Princeton University. He chose algebra as his research direction, and his mentor was Emil Artin, a famous contemporary algebraist, so he was a brother with John Tate, winner of the Wolf Prize and Abel Prize. Wang Xianghao obtained his master's degree in just one year. In the remaining two years, he earned another doctorate. In addition to being more diligent and hardworking than ordinary people, another reason for being able to get a master's degree and doctorate in such a short time is probably that the financial aid is not enough (this is also a common state for students studying in the United States at that time), and I want to finish my studies quickly. It can be seen that people's potential under pressure is endless.
Wang Xianghao returned to China in 1949 after defending his doctoral dissertation, and was hired as an associate professor in the Department of Mathematics of Peking University, his alma mater, teaching professional courses such as algebraic number theory and other basic courses. Among the students at that time was Ding Shisun, the later president of Peking University. After returning to China in 1951, Wu Wenjun also taught mathematics at Peking University, and the two became acquainted ever since. Later, Wang Xianghao went to Jilin University to preside over the work, and the doctoral dissertation defense would generally invite Wu Wenjun to join the defense committee, and other people who were often invited were Lu Ruzhen and Dong Yunmei. Plus Wang Xianghao, a doctoral defense, four academicians sit, the lineup is very luxurious.
In 1952, Wu Wenjun was transferred to the Institute of Mathematics of the Chinese Academy of Sciences, and Wang Xianghao went north to Jilin University, where he successively became the first head of the Department of Mathematics and the Department of Computer Science of Jilin University, and served as the vice president. In 1955, with his previous research in algebraic number theory and the supplement to Grunwald's theorem, Wang Xianghao was elected as the first member of the Chinese Academy of Sciences (that is, later academicians of the Academy of Sciences), one of the first 9 members of the mathematics, and Wu Wenjun was the 10th member of the mathematics, so Wang Xianghao was more senior than Wu Wenjun.
A still from the documentary "The Secret Rules of Modern Life: Algorithms" (2015).
Wang Xianghao was also the first academician to switch from mathematics to computer. In 1955, Wang Xianghao formulated a research plan in the Department of Mathematics of Jilin University, which included computational mathematics. In the following year, the State Council completed the formulation of the "1956-1967 Long-term Plan for the Development of Science and Technology" (referred to as the "12-year Science and Technology Plan"), which listed computers, automation, electronics, and semiconductors as key areas for rapid development, which also accelerated the pace of computational mathematics construction in Jilin University.
From 1957 to 1959, Jilin University hired Soviet expert Mesovskikh to run a lecture class on computational mathematics, attended by Xu Zhuoqun and Xu Cuiwei of Peking University, Jiang Erxiong of Fudan University, Kang Lishan of Wuhan University, and others. The two-year lecture class has allowed a group of local teachers such as Li Ronghua, Li Yuesheng, Feng Guochen to grow, coupled with Wang Xianghao, which is enough to establish Jilin University's leading position in the field of computational mathematics in China. During this period, Wang Xianghao concurrently served as the director of the Department of Computational Mathematics, and he also transferred from mathematics to the field of computer science and became the founder of the computer science department of Jilin University.
Wang Xianghao's main research at that time was the attribution principle, which is also one of the three algorithms for theorem proof. The attribution principle was proposed by John Alan Robinson after improving Elbrown's theorem in 1965, but its application scope is relatively narrow, Wang Xianghao and his student Liu Xuhua made many improvements to the attribution principle on this basis, proposed generalized attribution and lock semantic attribution, and pointed out the errors of ordered linear attribution (OL attribution) proposed abroad, and proposed a modified ordered linear attribution (MOL attribution).
Wang Xianghao established a number of research groups in Jilin University, and the most fruitful were the multi-valued logic group led by him, the automata group, and the computer algebra group. Later, Jilin University established the Department of Computer Science in 1976, and several major research directions of the Department of Computer Science also evolved from the previous group, and in the process of approaching artificial intelligence, two major directions were gradually formed: automatic reasoning models and their proofs, expert systems and knowledge engineering, the former led by Liu Xuhua, the latter by Guan Jiwen. These important achievements of basic theoretical research also laid the foundation for Wang Xianghao to first advocate artificial intelligence research in China.
In the 70s of the 20th century, Jilin University due to the early development of computational mathematics research, three generations of old, middle, and young teachers, and the oldest member of the faculty in this field, Wang Xianghao, sat and organized, and became the center of computer and artificial intelligence research at that time. At that time, many domestic colleges and universities established computer departments, and Jilin University also received many teachers who came to "learn from the experience", which also laid the foundation for the "Computer Science Summer Seminar" held in 1979.
In the 70s of the 20th century, mathematics and logic were the mainstream of artificial intelligence
From July 23 to 30, 1979, the Computer Society of the Chinese Institute of Electronics (the predecessor of the China Computer Society) held the "Computer Science Summer Seminar" in Jilin University, which was jointly organized by Jilin University, Peking University, Institute of Computing Technology of the Chinese Academy of Sciences, and Jilin Institute of Computer Technology, Wang Xianghao served as the leader of the conference leading group, and other members of the conference group included Wu Yunzeng, Wu Wenjun, Liu Shengli, Lu Ruzhen, Cao Lubing, Wu Zhiheng, Zhang Zhaoqing, Luo Zhukai, Chen Bingcong, Jin Chunzhao, Zhang Minghua, Xu Kongshi, Wu Wenjun, Wu Yunzeng, Lu Rujun, and Zhang Minghua made special academic reports at the plenary meeting. The conference is divided into four topics: intelligent simulation (artificial intelligence), basic theory and operating system of computer science, formal language and compilation theory, hardware theory and application.
Artificial intelligence is the most important direction of this symposium - in March 1978, the National Science Conference formulated the "1978-1985 National Science and Technology Development Plan Outline" (referred to as the "Eight-Year Planning Outline"), which listed "intelligent simulation" as an important research direction of computer science, and also drove a group of researchers to get involved in the field of artificial intelligence. Wu Wenjun has just completed the Wu method of machine proof of geometric theorems, and this breakthrough has aroused the interest of many researchers at home and abroad. In the conference presentation session on the morning of July 25, 1979, Wu Wenjun gave a report on the machine proof of geometric theorems. In the breakout sessions, he personally served as the leader of the intelligent simulation group. With Wu Wenjun sitting in town, the discussion of the intelligent simulation group was also a little more lively than the other groups.
Computer Science Summer Symposium Representative Certificate (provided by He Huacan, "A Brief History of Chinese Intelligence: From 1979 to 1993" illustration).
After Wu Wenjun, Lu Rujun of the Institute of Computing Technology of the Chinese Academy of Sciences gave a report, and the topic of the report was "Engineering Implementation of Software Porting". Lu Rujun is also a mathematician, graduated from the Department of Mathematics of the University of Jena in Germany in 1959, "changed careers" into the field of computer science in 1972, and advocated and presided over a series of software projects aimed at software mechanical generation and automatic portation (hereinafter referred to as the "XR Project") from 1975 to 1981. At that time, computer research was gradually carried out in China, but the number of software was small, the cost of writing was high (according to Lu Rujun's statistics, the development cost of a computer instruction was about $10), and software became a stumbling block to hinder the popularization of computers. The XR plan solved the problem of software migration between different platforms by targeting several types of computers widely used in mainland China, and promoted the solution of the lack of software in domestic machines at that time. Lu Rujun later extended this knowledge-based intelligent software engineering idea to the knowledge engineering language TUILI (reasoning) and the national seventh five-year research project "expert system development environment", and won the first Wu Wenjun Artificial Intelligence Science and Technology Award for his outstanding contributions in the field of artificial intelligence.
Two other conference presentations the next morning were also related to artificial intelligence. Wu Yun was a well-known mathematical logician and computer scientist from Peking University, one of the organizers, who has successively taught in the Department of Philosophy, Department of Mathematics and Computer Science of Peking University, and has made considerable achievements in every field, from philosophy to mathematics, from mathematical logic to computers. Wu Yun recognized early on that philosophy and mathematical logic are the foundation of computer science, and at this conference, the theme of his presentation was "Hilbert's tenth problem and computerization". Hilbert's tenth problem is a problem related to solving equations, and masters such as Gödel, Church, and Turing have key research on this problem, and the computerization of this problem is the understanding and exploration of the nature of computation, which is of great guiding significance.
The last guest speaker was Zhang Minghua from Tsinghua University. Zhang Minghua stayed on after graduating from the Department of Mathematics of Tsinghua University in 1952 and was one of the earliest teachers in the teaching of computational mathematics at Tsinghua University. He then specialized in computational theory and basic theories of computer science, and wrote the book Computability Theory. Computability is not only the foundation of computer science, but also the key to artificial intelligence. The basic ideas of computable theory were used in programming, resulting in recursive processes and recursive data structures, and the topic of his presentation at the conference was "Data Flow Analysis". Zhang Minghua also published a paper called "The Equivalence Problem of Block Diagram Format" at this conference, which was rated as an excellent paper in the conference and recommended to the National Computer Annual Conference.
This conference is actually a "bottom-up meeting" for Chinese engineering intelligence research. Many participants began to contact artificial intelligence after "intelligent simulation" was listed as an important direction of computer science, and it was only one year before the conference was held, it was difficult to have in-depth understanding and research, and Jilin University showed a first-mover advantage in artificial intelligence research, Wang Xianghao's "Generalized Summary", Guan Jiwen's "Maximum Period Theorem of Linear Automata" and "Parity of Linear Automata", Liu Xuhua's "Lock Semantic Attribution Principle and Fuzzy Logic" were selected as excellent papers at the conference.
Another outstanding school is Wuhan University. The papers of two students of Zeng Xianchang, Liu Chuchang and Dai Dawei ("Mechanical Algorithm for Dai Dejing Problem" and "Graph Algorithm for Dedekind Problem", respectively) were also selected as excellent papers at the conference. Zeng Xianchang, who together with Wu Wenjun and Wang Xianghao, is known as the "three masters of machine proof", also switched from mathematics to computers. Zeng Xianchang was born into a mathematical family, his father was an influential expert in the history of mathematics and calendars, and one of the founders of the Chinese Mathematical Society. In 1928, when the National Wuchang Sun Yat-sen University was transformed into "National Wuhan University", Zeng Zhaoan was a member of the preparatory committee. Zeng Xianchang is a student of mathematician Tang Mizhen, he stayed in the United States in the late 40s of the 20th century, studied mathematics at Columbia University like his father, and followed the instructions of his father Zeng Zhaoan to conduct field research on the world's first electronic computer that appeared in Philadelphia in the late 40s of the 20th century. When Zeng Xianchang returned to China, he brought back a batch of materials on computer science, which played an important reference role in the establishment of the Department of Computer Science of Wuhan University in the 70s of the 20th century.
A still from the documentary "The Secret Rules of Modern Life: Algorithms" (2015).
Zeng Xianchang has been engaged in the teaching of mathematics and computer science for a long time, he is knowledgeable and profound, fluent in English, Russian, German, French and Japanese, in the Department of Mathematics and Computer Science for undergraduates mainly taught number theory, advanced algebra, equation theory, algebraic integer theory, modern algebra, mechanical solution of equations and other courses, for graduate students to open theorem machine proof, machine learning, intelligent software engineering and other courses, compiled and published "Equation Theory", "Advanced Algebra", "Algebraic Number Theory", "Algebraic Structure" and other important textbooks. Due to his outstanding academic achievements in mathematical theory and theorem proof in computer science, he was appointed by the Ministry of Education as the head of the Chinese delegation to attend the International Computer 1979 Annual Conference in Washington, D.C., USA; At the end of the same year, he attended the 1979 International Parallel Processing Conference held in the suburbs of Detroit, USA, and published two papers, which were published in the proceedings of the conference, which attracted the attention of domestic and foreign counterparts.
Wuhan University has produced many academic families in its history, and the Zeng family father and son are among the best. In 1958, Wuhan University built two "principal's buildings" across the road in the new third district, and the father and son of Zeng Zhaoan and Zeng Xianchang lived at Gate No. 1. In the 70s of the 20th century, Wuhan launched the "one meter seven rolling mill" project, the project convened relevant researchers from various universities in Wuhan to collaborate on key problems, many technical documents in the early stage were translated by Zeng Zhaoan, Zeng Xianchang also participated in the use of computers to optimize the "one meter seven rolling mill" project. In 1978, the Department of Computer Science was established at Wuhan University, and Zeng Xianchang also became the first tutor of the Department of Computer Science of Wuhan University to recruit graduate students. At that time, when the Department of Computer Science was established, the graduate enrollment of Wuhan University had ended, and the students had already reported to the school, and the Department of Mathematics temporarily allocated three people from this group of students who had been studying for more than two months to study Zeng Xianchang's graduate students in the Department of Computer Science, and the research topic selected by Zeng Xianchang for this group of graduate students was the proof of the machine theorem.
The ultimate goal of Wang Xianghao and Zeng Xianchang's research on machine theorem proofs is to achieve automatic reasoning, which is also the direction that many mathematicians naturally pay attention to after studying to a certain extent. Fields Medal winner Vladimir Voevodsky switched from algebraic geometry to the study of automatic reasoning and formal verification because after some of his work was constructed as counterexamples, he doubted many of his work and many proofs, and began to try to replace unreliable manual inspection with reliable machine verification. Wu Wenjun believes that he is still a mathematician, but Wang Xianghao and Zeng Xianchang jump out of mathematical research itself, starting from automatic reasoning, and applying the ability of automatic reasoning to other scenarios to achieve intelligence.
With the same goals and similar backgrounds, there is also a lot of cooperation between the two teams, Wang Xianghao and Zeng Xianchang. If the graduate student graduation defense must be attended by external experts according to the regulations, the Department of Computer Science of Wuhan University and the Department of Computer Science of Jilin University agreed that the graduate students of the two schools would defend together, so that there was no need to invite people from other units. Liu Chuchang, Zeng Xianchang's earliest graduate student in the Department of Computer Science, recalled to this writer that at that time, the two universities set up a five-member defense committee, Professor Wang Xianghao, Professor Guan Jiwen and Professor Liu Xuhua at Jilin University, and Professor Zeng Xianchang and Professor Hu Jiuqing at Wuhan University. Since there are many graduate students in the Department of Computer Science of Jilin University, the defense is always arranged in Jilin University. After that, Liu Xuhua, Guan Jiwen, Liu Chuchang and others also jointly organized a number of academic activities such as the University Artificial Intelligence Academic Conference and the first National Automatic Reasoning Symposium.
In addition, it is worth mentioning He Huacan from Northwestern University. He Huacan published a paper called "Introduction to Intellectualism" at the conference, which is prominent among many researchers who have just entered the field of artificial intelligence. He Huacan was also selected by Wang Xianghao and Wu Wenjun as the deputy leader of the artificial intelligence team to assist Wu Wenjun in convening the group members.
Judging from the content of the above paper, artificial intelligence in this period is still artificial intelligence in a narrow sense, and the focus of researchers' research is mostly limited to theorem proofs and formal logic - it is not surprising that the 70s of the 20th century was the era of symbolism, and mathematics and logic were the mainstream of artificial intelligence.
This conference helped Jilin University establish the position of the leader of artificial intelligence research, and the artificial intelligence research of Jilin University has also entered an unprecedented period of prosperity. In addition to playing an active role in promoting the field of artificial intelligence in early China, Jilin University has also cultivated several generations of outstanding scholars, including Guan Jiwen, Liu Xuhua, Liu Dayou, etc.; Alumni who have blossomed overseas include Li Kai, academician of the American Academy of Engineering, foreign academician of the Chinese Academy of Engineering, and professor at Princeton University, and Zhang Chengqi, author of the first Chinese article in Artificial Intelligence magazine and chairman of the Australian Council on Artificial Intelligence, all of whom are from Jilin University and have been guided by Wang Xianghao. After the conference, more and more sister universities came to Jilin University to understand artificial intelligence. In 1980, the Ministry of Education entrusted Jilin University to hold an artificial intelligence research class, and 16 universities including Tsinghua University and Beijing Institute of Aeronautics sent teachers to Jilin University to study artificial intelligence. In this research class, He Huacan also participated in the study as a teacher representative of Northwestern Polytechnical University, which led to another story.
This article is selected from "A Brief History of Chinese Intelligence: From 1979 to 1993", some subheadings are added by the editor, not the original text. It has been authorized by the publishing house to publish.
Original author/Lin Jun Cen Feng
Excerpt / He Ye
Editor/Zhang Jin
Introduction proofreader/Zhao Lin