Заслушался сказок классный прошлогодний видосик "Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters"
где два пацанчика пиарят свой Mathematical Superintelligence :)
Harmonic: AI for Formal Mathematical Reasoning

С тех пор они подорожали раз в 10, почти до миллиарда долларов.

Ну, да, 90% в задачках MiniF2F, золотая медаль на IMO 2025 (5 из 6) и т.д.
Ну, да, оба со стэнфордским образованием, один даже у Тао учился, хотя потом сразу ушли в IT-AI-бизнес (беспилотные машинки и прочая попса...).
Ну, да, прикрутили теорем-прувер (завтипчики) Lean4.

Хотя так-то на выходе у них как не было ничего, так и нету что потрогать вживую. Только красивый пиар :)

Вакансия их понравилось: Part-time Lean Expert. Яб пошёл.

Фронт ищут под Expo (классная кстати кросс-платформная либа, не знал про такую)

А Research Engineer, Formal Methods вот на фуллтайм.
The initial focus of this position will be on advancing mathematical theorem proving using cutting-edge AI techniques. The successful candidate will play a key role in developing new algorithms and models that integrate AI with formal methods to solve complex problems in theorem proving and beyond.
Apply formal verification techniques using Lean or similar frameworks to formally verify safety critical systems

А решатели свои они пишут на плюсах: 17 из 30 сложных геометрических задач в AG-30 решены за 0.4 секунды на одном ядре 3.1 ГГц, и кодера тоже ищут (но и Python обязателен; у меня в Лаборатории теперь, кстати, тоже :).

Да, но...
For a while during the IMO, we had nearly 500,000 CPUs running Lean code at the same time with 95-100% utilization, which shows that the solution we built worked.

Вообще у них действительно немало больших и сложных научных(?) статей, где они типа достаточно подробно разбирают свои подходы, хотя подобные тексты сегодня не сложно генерить с хорошим AI, всё равно никто ничего не разберёт :)
Например свежак Aristotle: IMO-level Automated Theorem Proving

Мои 2 коп что их система смотрится уж слишком многоуровневой и перегруженной, с кучей слоёв абстракций. Сами судите:

- LLM-ка, обученная на Lean/SMT
- proof-search agent с деревом поиска и тактиками (имхо, самая слабая часть всей архитектуры - это архитектура самого Lean4, прежде всего концепция тактик)
- интеграция с лином через JSON-RPC
- версионированный датапайплайн self-play/self-mining
- RL с обратной связью от пруф-ассистента
- кэш фактов, бустинг через эвристики выбора лемм
- IDE-оболочка: чат, редактор с подсветкой, step-through доказательств, интеграция с Lean infoview
...

Главные вопросики:
- долгий и дорогой proof‑search + kernel‑check, возможно ли в принципе масштабировать на реальные кодобазы хотя бы в десятки тысяч строк кода?
- хрупкость по версии/ядру/тактикам Lean 4, да и сама его хилая экосистема и слабенькие датасеты вне mathlib

Ну и в целом насколько вообще переносятся "скиллы" решения математических задач на формальную верификацию? Получится ли хоть что-то перенести из хорошо формализованных задачек MiniF2F в суровый прод, тем более КИИ?

Так-то пайпу "Lean + генерация verification conditions + SMT/модел-чекинг" в принципе должно быть пофиг, что задачки, что верификация, но без очень мощного инженерного моста тут не обойтись, а в их проекте и так уже дофига всего накручено.

Наблюдение продолжаю 😎