Здесь я представляю полную автоформализацию недавней математической статьи (снова!) Баранец, Стефан. "Сокращение числа уравнений, определяющих подмножество n-пространства над конечным полем." Анналы факультета наук Тулузы: Математика, сер. 6, т. 33, № 1 (2024): 177–182. Я потратил несколько дней на этот проект. Сначала я запустил Aristotle от @HarmonicMath, который за примерно 15 часов полностью автоформализовал доказательство. Затем, с большой помощью @PietroMonticone, мне удалось создать черновую версию доказательства. Это версия, в которой все части документации в LaTeX становятся интерактивными и могут быть исследованы и изучены. Мы можем видеть зависимости в доказательстве и изучать их отношения. На этапе постобработки я также использовал Grok Heavy и Codex CLI с GPT-5.2 в режиме xhigh, чтобы написать построчный анализ формального доказательства. Это большая помощь для людей, которые не являются профессиональными программистами Lean 4. Вы действительно можете усвоить все шаги доказательства. Я хочу подвести итоги своих впечатлений и того, что я узнал из этого опыта. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

Математические статьи нуждаются в формальной валидации. Обычно это делается неформально рецензентом. Но что если мы могли бы полагаться на что-то более надежное, например, автоформализацию в Lean 4, где роль рецензента была бы сведена к тщательной проверке формулировок определений и теорем? Компиляция автоматически сгенерированного кода станет сертификатом доказательства. Это произошло в более длительном эксперименте, который я провел с Аристотелем вместе с @HarmonicMath. Спасибо @PietroMonticone и @llllvvuu за помощь в настройке плана. Здесь я представляю полную корректную автоформализацию статьи моего друга Стефана Баранчука о последовательностях делимости Чебышёва. Код состоит из примерно 5000 строк высоконетривиального Lean. Он исправляет все несоответствия и пробелы в основной статье (даже доказывая некоторые делегированные предложения). Я собираюсь опубликовать серию таких экспериментов, доказывающих, что в некоторых областях математики, включая элементарную теорию чисел, комбинаторику и анализ (все виды тем, охватываемых Mathlib), мы не так далеки от массового сдвига в документации действительности доказательств. Я думаю, что это будет напряженный год!

Если бы я был студентом сегодня, взаимодействие с современными LLM казалось бы почти обманом. Сегодня утром я случайно сфотографировал доску и попросил ChatGPT-5.2-Pro объяснить контекст, решение и некоторые замечания о знаменитой теореме Шевалье о конструктивных множествах. То, что я получил, былоRemarkably глубоким отчетом, синтезирующим качественный материал по алгебраической геометрии, собранный из интернета. Это поднимает серьезный вопрос: каковы реальные усилия и вызовы для студентов сегодня? Стоимость, безусловно, является одним из факторов, но как только доступ к этим моделям открыт, как следует учиться в этой стране изобилия, где объяснения, ссылки и интерактивное исследование доступны мгновенно? Возможно, борьба больше не заключается в получении информации или даже в понимании отдельных аргументов, а в развитии суждения: знание, какие вопросы задавать, каким объяснениям доверять, как распознавать глубину по сравнению с поверхностной правдоподобностью и как усваивать идеи, а не просто потреблять их. В среде, где ответы в изобилии, настоящая сложность может заключаться в формировании вкуса, математической интуиции и способности ориентироваться, а не тонуть в этом внезапном избытке знаний.