2 материалов
Пост проекта Xena называет формализацию Великой теоремы Ферма на 13 миллионов строк, сгенерированную Claude, и попытку с упаковкой сфер вкладом с малой долговременной ценностью, тогда как 950 участников Mathlib и 65 рецензентов поддерживают планку качества.
Главные треды HN: факты из обсуждений, разные стороны, голоса инсайдеров. Email, Telegram или RSS.
Его противопоставление — Mathlib против Mathslop: понятная математика, отобранная людьми, против вывода ИИ, верного, но нечитаемого: доказательство на 200 000 строк, которого никто не осмысливает. Если статус даёт только доказывание, а машины доказывают лучше, математики становятся ненужными.
Тред возразил с двух сторон. Не-математик пожал плечами: если нечитаемые, но верные теоремы позволяют строить полезное — какая разница? Другой вспомнил «добычу истины» Грега Игана и единственный козырь людей: модели всё ещё слабы в визуальном мышлении.
