Доведення до Lean

Новий бриф

Обидва попередні брифи вичерпано, тож цей прохід почався з вимірювання. Напрям дав «6 в 1»: для цього атласу передісторія лінії цінніша за свіжий хвіст. Тому бриф 27 вересня цілить у роки до 2000 і не цілить у 2020-ті зовсім, а мірило лишилося те саме, що 25 вересня, — лінія без середини.

На 848 записах найпорожнішою середина виявилася в машинному доведенні. Дев’ять записів 2024–2026 років — AlphaGeometry, AlphaProof, золото олімпіади, задачі Ердеша в Lean — стояли на Logic Theorist 1956 року й резолюції 1965-го, а між 1965 і 2024 роками не було жодного запису. Далі в брифі п’ять запитів. Залізо: лінія обчислень має сімдесят записів у 2020-х і чотири між 1951 і 1999 роками. Медицина до 1990 року починається з MYCIN 1974-го. Для України й Східної Європи до 1991 року атлас має п’ять київських записів і жодного про Польщу, Чехословаччину, Угорщину чи НДР. П’ять державних програм мають запис про початок і жодного про кінець. Ранні програми, що вчилися, мають діру між 1961 і 1983 роками. Кібернетику 1940–1960 років перевірено, і запиту вона не дістала: там уже чотирнадцять записів.

Десять записів

Запит 1 виконано цього ж дня. Машина Гелернтера ранньою весною 1959 року довела першу теорему планіметрії на IBM 704 і приймала крок лише тоді, коли він справджувався на кресленні. Програми Хао Вана пройшли понад двісті теорем «Principia» менш ніж за три хвилини. Звіт Девіса, Логемана й Лавленда 1961 року додав до процедури Девіса — Патнема розщеплення. Далі йдуть Automath 1968 року, LCF 1972-го, прувер Бойєра й Мура 1973-го, теорема про чотири фарби, метод Ву, числення конструкцій 1986 року, з якого виросло ядро Lean, і EQP, що 10 жовтня 1996 року розв’язав проблему Роббінса.

Документи шукали три агенти й зберігали дослівні витяги поза репозиторієм. Кожне твердження я звіряв із витягом, а витяг — із повним текстом. Сім дат із десяти збіглися з гіпотезами, записаними до читання. Три числа виявилися хибними або їх у документі не було. Одне з них відоме всім: «1 200 годин машинного часу» для чотирьох фарб. В обох частинах статті Аппеля й Гакена цього числа немає. Там є інше: 1 936 конфігурацій оголошено в липні 1976 року, 1 834 подано в статті, а 1 482 досить.

Бриф теж помилявся. Він просив Бойєра й Мура за журналом 1975 року, а першодрук — доповідь на IJCAI у серпні 1973-го. Чотири фарби він називав «першою теоремою такого роду», а Роббінса — «першою відкритою задачею, яку розв’язала програма». Жоден прочитаний документ цих «перших» не стверджує, тож записи їх не повторюють. Статті Ву 1978 року не знайшлося ніде. Запис про його метод стоїть на тексті нагороди Herbrand 1997 року й на статті AlphaGeometry, яка бере цей метод за попередній рівень, і позначений середньою впевненістю.

Без браузера

Прохід ішов у хмарній сесії, де браузерної панелі немає. Project Euclid не пускає оболонку, але інструмент WebFetch віддав PDF обох частин статті про чотири фарби. HAL ставить перевірку Anubis, тому звіт INRIA про числення конструкцій прочитано в тому самому файлі HAL, викладеному на сторінці курсу в Огайо. Web Archive увесь прохід скидав з’єднання. Що не відкрилося ніде, перелічено в журналі пакета.

Межі сторінки записів і першого навантаження піднято першою дією, до першого запису. Після пакета найтісніші вісь і її дані: 1 189 і 3 460 байтів запасу.