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