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