EQP розв'язує проблему Роббінса
10 жовтня 1996 року програма EQP, створена в Аргоннській національній лабораторії, знайшла доведення того, що кожна алгебра Роббінса булева. Пошук тривав близько восьми днів на процесорі RS/6000 і зайняв близько 30 мегабайтів пам'яті. Питання поставив Герберт Роббінс невдовзі після 1933 року; ні він, ні Гантінгтон доведення не знайшли, а згодом задачу вивчали Тарський і його учні.
Чому це важливо
Програма автоматично розв'язала відкриту задачу, над якою математики працювали з 1930-х років і в якій, за сторінкою, з початку 1980-х не було суттєвого поступу. Машина вже не перевіряла й не повторювала людське доведення, а знайшла своє.
Проблема: чи можна в аксіоматиці булевої алгебри, яку Е. В. Гантінгтон подав 1933 року, замінити його рівність простішою рівністю Роббінса. Сторінку Вільяма Мак-К'юна про розв'язок опубліковано в жовтні 1996 року; EQP схожий на відому програму Otter тієї самої лабораторії, але має асоціативно-комутативну уніфікацію й обмежений рівностями. Протокол програми: версія EQP 0.9 червня 1996 року, завдання почалося 2 жовтня 1996 року, суперечність знайдено на 678 232-й секунді. Стаття Мак-К'юна, подана до Journal of Automated Reasoning 22 січня 1997 року, описує, як ішов пошук. Спроба, що привела до розв'язку, тривала п'ять тижнів, з 6 вересня по 11 жовтня 1996 року, щонайбільше на трьох звичайних робочих станціях UNIX. Близько чотирнадцяти багатоденних пошуків забрали разом близько п'яти тижнів процесорного часу. Вдалий пошук ішов майже 8 днів, вивів 49 548 рівностей і довів, що кожна алгебра Роббінса задовольняє умову, яку раніше вручну довів достатньою Стів Вінкер. Машина взялася за задачу 1979 року, коли Вінкер, студент, що гостював в Аргонні, почув про неї від Джоела Бермана. Із посиланням на телефонну розмову з Роббінсом у жовтні 1996 року стаття каже, що задача не походить від помилки Гантінгтона, як твердить поширена легенда. Чого запис не стверджує: року самої гіпотези Роббінса — сторінка пише лише «невдовзі після» 1933-го, стаття — «у 1930-х». Статтю прочитано в остаточній авторській версії березня 1997 року, а не в журнальному наборі.