Машина Гелернтера доводить теореми геометрії

Ранньою весною 1959 року IBM 704 у дослідницькому центрі IBM із програмою приблизно на 20 000 інструкцій довів свою першу теорему евклідової планіметрії. Машина Герберта Гелернтера приймала підціль лише тоді, коли та справджувалася на кресленні, і так відкидала хибні кроки ще до спроби їх довести.

За статтею Гелернтера, Гансена й Лавленда 1960 року, без креслення програма породжувала на кожному кроці близько 1 000 підцілей, а з ним приймала в середньому 5; перевірка на кресленні, за авторами, не могла призвести до хибного доведення. Програма написана мовою обробки списків, яку компілював FORTRAN; на час статті збережено понад п'ятдесят доведень. Гелернтер і Рочестер ще 1958 року описували задум як наслідок Дартмутського проєкту; у жовтні 1958 року, за їхньою статтею, програму ще писали (с. 342), а геометра вивчали симуляцією на IBM 704 (с. 344). Доповідь Гелернтера на паризькій конференції (Proceedings of the International Conference on Information Processing, ЮНЕСКО, Париж, 15–20 червня 1959 року, с. 273–282) прочитано двома шляхами: повністю в розділі книги «Computers and Thought» (Фейгенбаум і Фельдман, 1963, с. 134–152), що її передруковує, і лише фрагментами повнотекстового пошуку в позиченому примірнику самих матеріалів, сторінок яких не бачили. Розділ не слово в слово збігається з доповіддю: про довгострокову програму досліджень він каже, що її започатковано в дослідницькому центрі IBM у Нью-Йорку, а уривок першого абзацу доповіді (с. 273; початок речення обрізано) каже, що досягнуто першої мети в симуляції на швидкодійній цифровій машині пристрою, здатного знаходити доведення в планіметрії. Доповідь називає геометричну машину особливою конфігурацією станів IBM 704 (так само й розділ, с. 139). Стенограми доведень у ній закінчуються сумарним часом 0,32, 4,06, 8,08 («з базовими евристиками») і 1,06 («з розширеними евристиками»; в розділі, де ті самі стенограми, стоїть одиниця «хвилини»). Розділ друкує їх трьома додатками, і його текст пов'язує кожен із задачею. Додаток А, теорема про точку на бісектрисі кута: 0,32 хвилини; у тексті — менш як за хвилину. Додаток Б, чотирикутник з однією парою рівних і паралельних протилежних сторін: на 0,88 хвилини машина пише «I am stuck», будує допоміжний відрізок DB, починає задачу заново й закінчує за 4,06; у тексті — менш як за п'ять хвилин. Додаток В, теорема про дві вершини трикутника, рівновіддалені від медіани до сторони, яку вони визначають, двічі: 8,08 хвилини з базовими евристиками й 1,06 з розширеними. За текстом (с. 145), з базовими евристиками це близько восьми хвилин, двадцять чотири кола циклу підцілей, шістдесят одна проміжна підціль і глибина графа дванадцять рівнів, а з розширеними — одна хвилина, чотири кола, двадцять одна підціль і три рівні. Решта часів стенограм не має: задача з випускного іспиту бруклінської технічної школи — менш як п'ять хвилин з розширеними евристиками, тоді як базові за півгодини вичерпали робочу пам'ять (це речення є й у фрагменті пошуку по доповіді, с. 279); діагоналі паралелограма — близько трьох хвилин в обох режимах; ще одна задача з такого іспиту — вісім хвилин проти трьох. День доповіді. У друкованій програмі конференції (Handbook ЮНЕСКО, с. 28–29) доповідь Гелернтера «Realization of a geometry theorem proving machine» стоїть на п'ятницю, 19 червня 1959 року, після обіду (з 15 до 18 години), у засіданні I «Session on Proving of Logical Propositions», третьою з п'яти, між Гілмором і Данхемом зі співавторами. Ту саму п'ятницю й те саме засідання дають документ ЮНЕСКО NS/155 (додаток III, с. 8–9; на прочитаних сторінках без дати) і списки голів у конференційному «Journal» (голова I. I. Basilovsky, заступник S. N. Alexander). Це розклад, складений наперед (довідник — до конференції, «Journal» — у її перші дні), а не звіт про те, що було: годину виступу жоден прочитаний документ не називає, у прочитаних випусках «Journal» зміни для засідання I немає, випуск № 5, мабуть п'ятничний, не бачили, а порядок розділів у томі матеріалів, за його передмовою, не відповідає порядку засідань. Чого запис не стверджує: що відомо, у якому місяці й якого дня відбулося перше доведення. Жоден прочитаний документ цього не називає; є лише «рання весна 1959 року» в статті 1960 року. День доповіді, запланований на 19 червня, не є датою першого доведення. Число 20 000 інструкцій і «ранню весну» знаходять лише в першому абзаці статті 1960 року (в її передруку 1963 року, с. 153, з посиланням на 1959b, яке в бібліографії книги, с. 490, має заголовок паризької доповіді); їх немає ні в розділі книги з доповіддю (с. 134–152), ні, за пошуком у розпізнаному тексті примірника Internet Archive, на с. 273–282 матеріалів, але сторінок оригіналу не бачили, тож там відсутність стоїть на пошуку, а розділ не є копією. Відповідність стенограм задачам і числа з тексту на с. 145 прочитано лише в розділі, не на сторінках доповіді. Першодрук статті 1960 року, як його читали раніше, часу на задачу не називає; її передрук 1963 року друкує стенограми з часом 1,03, 8,12 («I am stuck») і 30,68 хвилини (с. 161, 163).