Lean

Каждый логический шаг классификации, то есть теоремы о том, что любая конечная простая группа — циклическая простого порядка, знакопеременная, типа Ли или одна из 26 спорадических групп, — проверен ядром Lean. Формализация содержит 2,05 миллиона деклараций и 100 вех, а команда опубликовала альтернативный путь для затронутого случая.

Математики в треде удивились, что пробелов оказалось так мало.

На корпусе Silesia roc-deflate отстаёт от libdeflate по медиане на 8,9% на Ryzen 9 3900X и на 2,6% на MacBook Pro с M1.

Заявленный выигрыш — множитель (log n)^ε при ε = 2^-182, который в треде высмеяли как микроскопический. Харви называет его «чудовищно огромным»: это первая трещина в границе, которую он считал жёстким физическим пределом.

Ответ геймдев-разработчика на HN: «Это не похоже на здоровое место для нас».

Пост проекта Xena называет формализацию Великой теоремы Ферма на 13 миллионов строк, сгенерированную Claude, и попытку с упаковкой сфер вкладом с малой долговременной ценностью, тогда как 950 участников Mathlib и 65 рецензентов поддерживают планку качества.

От аспирантов теперь ожидают $200 в месяц за доступ к моделям вроде Sol и Fable — Гарвард уже оплачивает подписку каждому студенту, постдоку и преподавателю на математическом факультете.

Не всех в треде впечатлил результат: один комментатор поднял историю цитирований гипотезы Якобиана и обнаружил, что математики сузили пространство поиска ещё в 1983 году — ИИ не открыл новую территорию, а просто наконец её обошёл.

Его противопоставление — Mathlib против Mathslop: понятная математика, отобранная людьми, против вывода ИИ, верного, но нечитаемого: доказательство на 200 000 строк, которого никто не осмысливает. Если статус даёт только доказывание, а машины доказывают лучше, математики становятся ненужными.

Тред возразил с двух сторон. Не-математик пожал плечами: если нечитаемые, но верные теоремы позволяют строить полезное — какая разница? Другой вспомнил «добычу истины» Грега Игана и единственный козырь людей: модели всё ещё слабы в визуальном мышлении.