Автоматична формалізація з Арістотелям від @HarmonicMath і зворотне інжинірингування з @OpenAI GPT Codex CLI (фактично GPT-5.2 з xhigh і всіма експериментальними перками увімкненими). Працюючи над вправою з алгебри Бурбакі щодо матриць, я отримав майже 900 рядків повністю задокументованого коду Lean 4, включаючи всі деталі доказу. Потім я передав його — використовуючи відповідно спроєктовану агентну систему — до Codex CLI, щоб реверс-інженерити відповідний файл LaTeX, реконструюючи кроки доказів безпосередньо з Lean, у стилі структурованих доказів Леслі Лампорта. Це ще не програма Langlands, але нам потрібно автоматизувати таку математику середнього рівня. І це відбувається зараз. Я просто зібрав правильну агентну систему, все конвеєрував і зібрав текст з Bourbaki (навіть ця частина добре працювала з @grok 4.1, що добре підходить для попереднього перегляду LaTeX наживо). Я закінчу документацію і викладу її на GitHub. Перевірте граф залежностей — Арістотель впорався з цим самостійно. І доказ повністю інтерактивний. Ми живемо у майбутньому науки зараз!

У цьому дописі в спільноті я хочу додати посилання на дуже захопливі ігри та інтерактивні середовища (вільно доступні), які допомагають людям досліджувати високотехнологічні концепції як у програмуванні, так і в математиці. Якщо ви знаєте ще якісь цікаві місця для відвідування, просто напишіть нижче. Розважатися! Lean: Збірка дуже захопливих програмних головоломок, які допомагають вам зрозуміти, як доводиться та формалізується математика. Ви більше ніколи не побачите твердість 5*7=7*5 так само, як і раніше. NandGame: Ви створюєте власний процесор з нуля (навіть NAND зроблений із простіших схем). Дуже затягує і дуже весело! Квантова мухоловка: Саме тут ви нарешті отримаєте розуміння квантових обчислень. Яскраві, безмежні, захопливі та математично дуже глибокі. Скретч: Вчися програмуванню весело. Евклідія: Навчіться виконувати конструкції за допомогою лінійки та компаса. Раніше це було частиною шкільного навчання, а тепер це додаток. Весело і дуже інформативно. Планарність: Спробуйте знайти вкладення графа, яке показує, що він дійсно є плоским. Ого: Найкращий дослідник клітинних автоматів. Якщо хочете копнути глибше: SageMath: Це потужна система комп'ютерної алгебри з синтаксисом Python. Він ідеальний для курсів, а синтаксис SageMath набагато ближчий до звичайного математичного дискурсу. Мені подобається викладати курси з SageMath. GeoGebra: Можна робити докази, обчислення та інтерактивні аплети. Це цікавий спосіб вивчити багато аспектів математики без бакалаврату. Демонстраційні проєкти Wolfram: Збірка математичних аплетів, які допоможуть вам зрозуміти дуже складні теми. Для запуску Mathematica не потрібен, але він потрібен для розробки власних аплетів. Механіка доказу (автор Гізер Макбет): Це книга з інтерактивним репозиторієм на GitHub, де можна більш комплексно дізнатися структуру та синтаксис Lean. Ілюстрована теорія чисел (Мартін Г. Вайсман): Це підручник з елементарної теорії чисел із застосуваннями. А ці додатки доступні на сайті у вигляді збірки безкоштовних зошитів Jupyter, які навчають ключовим поняттям. Графічна лінійна алгебра: Ілюстрованим і частково інтерактивним способом вивчення глибоких концепцій алгебри. HomotopyContinuation.jl: Це надзвичайно красивий і інтерактивний (разом із Джулією) спосіб вивчення деяких надзвичайно складних ідей з алгебраїчної геометрії (зв'язні компоненти, метод продовження гомотопії) та з застосуваннями до дуже спеціальних алгебраїчних систем, які походять із додатків. Ти можеш дізнатися Джулію по дорозі. Mathamaze: Це досвід від Гелени Веррілл. Чудова геометрія, плитка, візерунки. Просто чудово. Важко пояснити: N: Шлях ніндзя: Якщо ви вважаєте, що математика складна. Навчіться терпінню на власних помилках. Попередження: дуже залежність HyperRogue: Гіперболічну геометрію можна вивчити у розбійному світі.

Тут я знову представляю повну автоматичну формалізацію нещодавньої роботи з математики! Баранчук, Стефан. "Зменшення кількості рівнянь, що визначають підмножину n-простору над скінченним полем." Annales de la Faculté des sciences de Toulouse : Mathématiques,. 6, том 33, No 1 (2024): 177–182. Я провів кілька днів над цим проєктом. Спочатку я провів Арістотеля за @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