🧮 Видеоразбор доказательства Янга — Миллса от OpenAI

Канал How Did They Prove That? разобрал доказательство существования 4D квантовой теории Янга — Миллса: масштабный предел решёточной теории Вильсона, формализованный OpenAI в Lean 4. Исходник OpenAI-YM-20261028 опубликован 11 ноября 2026 — около миллиона строк Lean в 9477 файлах. Комитет пяти физиков счёл его, вероятно, корректным; полная человеческая статья ещё не вышла.

🌍 Впервые LLM выдала формализованное в Lean доказательство задачи тысячелетия. Корректность шагов гарантирует ядро Lean, а не репутация авторов: Lean-код — машинопроверяемый артефакт.

👤 Разбор — в видео, Lean-исходник — на GitHub, 278-страничная рукопись на естественном языке — в scottnarmstrong/yang-mills-informalization. Так ИИ ускоряет фундаментальную математику.

Источник 1: https://www.youtube.com/watch?v=s_9sCVqKQjY

Источник 2: https://github.com/yang-mills-group/OpenAI-YM-20261028