La investigación sobre la mecanización matemática ha logrado avances en la investigación sobre la demostración mecánica de teoremas de geometría elemental. Las demostraciones de teoremas geométricos de sistemas axiomáticos son muy poco mecánicas. Tomando como ejemplo la geometría en los cursos de la escuela secundaria, la demostración de un teorema a menudo requiere pensar mucho, ideas ingeniosas, adición aleatoria de líneas auxiliares y demostraciones tortuosas. Cómo utilizar computadoras para realizar razonamientos automáticos, especialmente demostraciones automáticas de teoremas geométricos, ha sido un tema de investigación a largo plazo en la comunidad académica. La llamada prueba mecanizada de teoremas tiene como objetivo proporcionar un método unificado para una clase de teoremas (puede haber miles de teoremas), de modo que cada teorema de esta clase de teoremas pueda demostrarse de acuerdo con este método. En el proceso de prueba, en cada paso adelante, hay reglas a seguir para determinar qué hacer a continuación y cómo hacerlo. De "una teoría, una prueba" a "un tipo, una prueba" es un salto en la comprensión y práctica de las matemáticas. El Sr. Wu creó un método mecanizado para demostrar teoremas en geometría elemental (generalmente refiriéndose a la geometría sin operaciones diferenciales, como la geometría euclidiana, la geometría no euclidiana, la geometría afín, la geometría proyectiva, la geometría algebraica, etc.), que se conoce internacionalmente como "Método de Wu", logrando por primera vez demostraciones mecánicas eficientes de teoremas geométricos. El "método de Wu" también se puede utilizar para el descubrimiento automático de teoremas geométricos y la derivación automática de relaciones desconocidas. Los logros pioneros del Sr. Wu Wenjun rompieron el estancamiento a largo plazo en la investigación de la comunidad internacional de razonamiento automático sobre las demostraciones automáticas de teoremas geométricos y también colocaron a mi país en una posición de liderazgo en este campo. La destacada contribución del Sr. Wu le valió el "Premio Herbrand" de 1998, el premio más alto de la comunidad internacional de razonamiento automático. (Este premio se otorga cada dos años, con un máximo de una persona en cada sesión. Hasta ahora, todos los ganadores son líderes en la comunidad del razonamiento automático).