Машина Гелернтера доводить теореми геометрії
Ранньою весною 1959 року IBM 704 у дослідницькому центрі IBM із програмою приблизно на 20 000 інструкцій довів свою першу теорему евклідової планіметрії. Машина Герберта Гелернтера приймала підціль лише тоді, коли та справджувалася на кресленні, і так відкидала хибні кроки ще до спроби їх довести.
Чому це важливо
Уперше машина доводила теореми не логіки, а шкільної геометрії, користуючись кресленням так, як людина. Ідея, що модель світу підказує, які кроки варто пробувати, і питання допоміжних побудов від цієї машини ведуть до AlphaGeometry 2024 року.
За статтею Гелернтера, Гансена й Лавленда 1960 року, без креслення програма породжувала на кожному кроці близько 1 000 підцілей, а з ним приймала в середньому 5; перевірка на кресленні, за авторами, не могла призвести до хибного доведення. Програма написана мовою обробки списків, яку компілював FORTRAN; на час статті збережено понад п'ятдесят доведень. Гелернтер і Рочестер ще 1958 року описували задум як наслідок Дартмутського проєкту. Чого запис не стверджує: скільки хвилин машина витрачала на задачу — стаття 1960 року цього не каже; і днів паризької доповіді 1959 року — її не прочитано.