Метод Ву: геометрія як алгебра
У 1977 році математик Ву Веньцзюнь з Академії наук Китаю реалізував на комп'ютері Great Wall 203 з пам'яттю 4K метод, що перетворює теорему елементарної геометрії на систему поліномів і перевіряє її алгебраїчно, і довів теорему про пряму Сімсона. Статтю про метод опубліковано 1978 року в Scientia Sinica.
Чому це важливо
За текстом нагороди Herbrand, після майже двадцяти років, коли машинне доведення геометричних теорем майже не просувалося, воно стало однією з найуспішніших ділянок автоматичного доведення. Через сорок шість років стаття AlphaGeometry бере метод Ву за рівень, який треба перевершити.
За текстом нагороди Herbrand 1997 року, метод спирається на принцип Рітта й теорему про структуру нулів, дає змогу не лише доводити, а й відкривати теореми та знаходити вироджені випадки; 1979 року на HP9835A Ву довів складніші задачі, як-от теорему Морлі, а на Заході метод поширив Ш. Ч. Чжоу в Техаському університеті на початку 1980-х. Стаття AlphaGeometry (Nature, січень 2024) перевіряла метод на тих самих задачах: 10 із 30 олімпіадних задач IMO-AG-30 і 75 % ширшого набору з 231 задачі, якщо відповідь можна дістати за 48 годин. Чого запис не стверджує: жодного твердження з самої статті 1978 року — її прочитати не вдалося, тож запис стоїть на нагороді 1997 року й на статті 2024 року.