Использование LLM для создания машинно-проверенных математических доказательств — новая спорная практика. Ценность здесь заключается не в авторстве, а в способности человека направлять и валидировать работу ИИ без глубокой экспертной подготовки. Дискуссии вокруг этого метода разделили участников на два лагеря. Одни считают такой подход «эксплуатацией человеческого капитала» и «stripmining» академических знаний, утверждая, что автор не заслуживает признания, если лишь оплачивал токены и задавал вопросы, не понимая сути. Другие полагают, что умение управлять LLM, формулировать запросы и интегрировать результаты в строгие формальные системы — это редкий навык, требующий интеллекта. Сдвиг в вычислительной культуре характеризуется переходом от «волшебников», понимающих систему, к «колдунам», использующим непонятные силы. Это подчеркивает различие между «know-that» (знания от LLM) и «know-how» (глубокое понимание). При этом доступность изложения новичка часто делает сложную математику понятнее традиционных лекций. Ключевым вкладом является использование Lean и Palomar для машинной проверки, что обеспечивает надежность и задает новый стандарт, где такая проверка становится обязательной. Процесс постоянной перепроверки результатов напоминает работу опытных разработчиков, а не пассивное потребление. Рекомендации по работе с LLM в математике: * не принимать результаты без объяснений, проверять логику и требовать ответственности за каждое утверждение; * упрощать доказательства, искать паттерны, сопоставлять части с известными теоремами; * использовать LLM в роли критика из научного журнала для углубления понимания; * проверить литературу на предмет дублирования доказательства. Ограничения и проблемы: * Экономическая неустойчивость: затраты в $40 000 за 40 миллиардов токенов зависят от личных ресурсов, а не от системной поддержки. * Интеллектуальный барьер: LLM пока не способны формулировать глубокие нетривиальные гипотезы на уровне Конвея; один из комментаторов назвал ИИ «великим фильтром», застрявшим на локальном максимуме развития. * Проблема признания: чтобы вклад был воспринят серьезно, автору следует демонстрировать глубокое понимание контекста, а не просто исправлять опечатки в письмах математикам.