Здесь я представляю полную автоформализацию недавней математической статьи (снова!) Баранец, Стефан. "Сокращение числа уравнений, определяющих подмножество 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