Программа Горенстейна 1972 года разбила работу на 16 этапов.…
Программа Горенстейна 1972 года разбила работу на 16 этапов. Объявление о завершении в 1983 году оказалось преждевременным. Квазитонкий случай Ашбахер и Смит закрыли в 2004 году на 1221 странице; ещё один пробел, связанный с M₂₂, устранили в 2008 году. Второе поколение доказательства систематизирует материал, но ещё не завершено. Axiom выбрала первое поколение, хотя карту зависимостей строила с опорой на тома второго.
Проект опирался на прежние формализации и карту из 108 этапов и примерно 380 задач. Агенты распределяли леммы и делегировали недостающие предпосылки; математики разбирали препятствия, инженеры поддерживали систему. Lean может принять вывод из дополнительной гипотезы, которая ещё не доказана, оставив исходную задачу открытой. Так было с одним вариантом теоремы о сигнальных функторах, объясняющей согласование локальных подгрупп. Из-за недоказанных предпосылок пришлось удалить десятки тысяч строк и пересмотреть план.
Агенты создавали доказательства быстрее, чем Lean успевал их перепроверять. Помогли распределённое кеширование сборок, параллельные проверки и отдельно проверяемые сертификаты тяжёлых конечных вычислений. Для математической связности незавершённые этапы дробили на точные утверждения и требовали короткого Lean-доказательства, что вместе они закрывают исходный этап.
Для Monster команда сообщает о формализации построения через алгебру Грисса размерности 196 884, доказательства простоты и распознавания по структурным признакам. Эти три задачи требуют отдельных аргументов.
Проект опирался на прежние формализации и карту из 108 этапов и примерно 380 задач. Агенты распределяли леммы и делегировали недостающие предпосылки; математики разбирали препятствия, инженеры поддерживали систему. Lean может принять вывод из дополнительной гипотезы, которая ещё не доказана, оставив исходную задачу открытой. Так было с одним вариантом теоремы о сигнальных функторах, объясняющей согласование локальных подгрупп. Из-за недоказанных предпосылок пришлось удалить десятки тысяч строк и пересмотреть план.
Агенты создавали доказательства быстрее, чем Lean успевал их перепроверять. Помогли распределённое кеширование сборок, параллельные проверки и отдельно проверяемые сертификаты тяжёлых конечных вычислений. Для математической связности незавершённые этапы дробили на точные утверждения и требовали короткого Lean-доказательства, что вместе они закрывают исходный этап.
Для Monster команда сообщает о формализации построения через алгебру Грисса размерности 196 884, доказательства простоты и распознавания по структурным признакам. Эти три задачи требуют отдельных аргументов.