Навье — Стокс, упаковка сфер и Lean: как ИИ пришёл в большую математику Как уложить одинаковые шары максимально плотно? С апельсинами на прилавке всё кажется очевидным. А вот доказательство оптимальной упаковки в восьми измерениях появилось только в 2016 году. Спустя десять лет ИИ-агент Gauss помог завершить перевод этого доказательства на формальный язык Lean. Правда, к тому моменту люди уже проделали огромную подготовительную работу. А в сентябре 2026 года OpenAI объявила, что её новая модель решила задачу тысячелетия Навье — Стокса. Здесь речь уже идёт о поиске ранее неизвестного доказательства, а не формализации готового. Заявление вызвало немало вопросов, в том числе о корректности результата и степени самостоятельности ИИ. И это уже совсем другая история.