Автоформализация с Аристотелем от @HarmonicMath и обратная инженерия с @OpenAI GPT Codex CLI (на самом деле GPT-5.2 с xhigh и всеми экспериментальными функциями включенными). Работая над упражнением из Алгебры Бурбаки о матрицах, я получил почти 900 строк полностью документированного кода на Lean 4, включая все детали доказательства. Затем я передал его - используя подходящий агентный набор - в Codex CLI для обратной инженерии соответствующего файла LaTeX, восстанавливая шаги доказательства непосредственно из Lean, в стиле структурированных доказательств Лесли Лампорта. Это еще не программа Лангланда, но нам нужно, чтобы такая промежуточная математика была автоматизирована. И это происходит сейчас. Я просто построил правильный агентный набор, организовал все в цепочку и извлек текст из Бурбаки (даже эта часть хорошо работала с @grok 4.1, что круто для предварительного просмотра LaTeX в реальном времени). Я закончу документацию и выложу ее на GitHub. Проверьте граф зависимостей - Аристотель справился со всем сам. И доказательство полностью интерактивно. Мы живем в будущем науки сейчас!

В этом посте сообщества я хочу разместить ссылки на некоторые очень увлекательные игры и интерактивные среды (доступные бесплатно), которые помогают людям исследовать высокие концепции как в программировании, так и в математике. Если вы знаете о каком-либо другом интересном месте для посещения, просто напишите ниже. Удачи! Lean: Сборник очень увлекательных программных головоломок, которые помогают вам понять, как математика доказывается и формализуется. Вы больше никогда не посмотрите на сложность 5*7=7*5 так же. NandGame: Вы создаете свой собственный процессор с нуля (даже NAND сделан из более простых схем). Очень затягивающе и супер весело! Quantum Flytrap: Здесь вы наконец-то получите некоторое понимание квантовых вычислений. Ярко, безгранично, увлекательно и математически очень глубоко. Scratch: Учите программирование весело. Euclidea: Узнайте, как выполнять построения с помощью линейки и компаса. Раньше это было частью школьного образования, но теперь это приложение. Весело и очень информативно. Planarity: Попробуйте найти вложение графа, которое показывает, что он действительно планарен. Golly: Универсальный исследователь клеточных автоматов. Если вы хотите углубиться: SageMath: Это мощная система компьютерной алгебры с синтаксисом Python. Она идеальна для курсов, и синтаксис SageMath гораздо ближе к обычному математическому дискурсу. Мне нравится проводить курсы с SageMath. GeoGebra: Вы можете делать доказательства, вычисления и интерактивные апплеты. Это веселый способ изучить многие разные аспекты математики для студентов. Wolfram Demonstration Projects: Сборник математических апплетов, которые могут помочь вам понять очень сложные темы. Вам не нужно Mathematica для работы, но вам нужно его для создания собственных апплетов. The Mechanics of Proof (автор Хизер Макабет): Это книга с интерактивным репозиторием на GitHub, где вы можете более подробно изучить структуру и синтаксис Lean. An Illustrated Theory of Numbers (автор Мартин Х. Уайсман): Это учебник по элементарной теории чисел с приложениями. И эти приложения доступны с сайта в виде сборника бесплатных Jupyter Notebooks, которые обучают вас ключевым концепциям. Graphical Linear Algebra: Иллюстрированный и до некоторой степени интерактивный способ изучения глубоких концепций алгебры. HomotopyContinuation.jl: Это невероятно красивый и интерактивный (с Julia) способ изучения некоторых очень сложных идей из алгебраической геометрии (связанные компоненты, метод гомотопической продолжения) и с приложениями к очень специальным алгебраическим системам, которые возникают из приложений. Вы можете изучать Julia по пути. Mathamaze: Это опыт от Хелены Веррил. Прекрасная геометрия, мозаики, узоры. Просто замечательно. Трудно объяснить: n: путь ниндзя: Если вы думаете, что математика сложна. Учите терпение трудным путем. Внимание: очень затягивает. HyperRogue: Вы можете изучать гиперболическую геометрию в среде rogue-like.

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