Current location - Training Enrollment Network - Mathematics courses - What are the achievements and significance of Wu Wenjun's mathematical mechanization?
What are the achievements and significance of Wu Wenjun's mathematical mechanization?
Since the winter of 1976, Wu Wenjun, a famous professor in China, has been inspired by the idea of ancient mathematical mechanization in China, but he still doesn't know the research results of foreigners. He boldly devoted himself to the research of mathematical mechanization and created the method of mathematical mechanization: starting from the axiomatic system of geometry, introducing coordinates, algebraicizing any geometric problem → expressing the assumptions and conclusions of proving the problem as multivariate polynomial equations → operating on an electronic computer to judge whether the theorem is valid or not.

Professor Wu Wenjun used his own method to prove a series of elementary geometry such as siemsen line, Feuerbach theorem and Mauret theorem on computer. Later, he expanded the scope of proof to non-Euclidean geometry, affine geometry, circular geometry, line geometry, spherical geometry and other fields. At present, using Professor Wu Wenjun's method, more than 600 theorems have been proved, many of which can be proved in a few seconds or even a fraction of a second on an electronic computer. Even some theorems are quite complicated to prove, even if they are handed over to excellent mathematicians, it is quite difficult.

Wu Wenjun, a mathematician in China, has finally realized the dream of mechanical proof of geometric theorems for thousands of years. The birth of the so-called "Wu Fa" has brought a strong impact on the axiomatic deduction system for more than two thousand years.

Professor Wu Wenjun also used his own method to prove that Newton's law can be deduced from Kepler's law through computer programs, which goes beyond the scope of mechanized proof of mathematical theorems and belongs to a wider range of automatic reasoning. In fact, as long as it involves solving equations, Wu's method is useful for problems studied in various scientific fields.

Moore, editor-in-chief of American Journal of Automatic Reasoning, believes that before Wu's method was established, the research on mechanical proof of geometric theorems was in darkness, and Wu not only broke through this silent situation, but also brought brilliant prospects.

Wyeth, an authoritative figure in American automatic reasoning, believes that Wu Wenjun's outstanding contribution in the field of automatic reasoning is indelible and he deserves the highest prize.

Wu Wenjun's wish: "China's traditional mathematics is on the verge of extinction, giving way to western modern mathematics. It's been several centuries, and now it's a critical moment to revive the cause of mathematics in China. In the next century, the mechanized algorithm system founded by China sages should take the lead in the field of mathematics.