Встретил сегодня этот мем и вспомнил в тему вчерашние посты.

Aristotle (an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems) так-то внутри использует Монте-Карло, Карл!

пруф: "Aristotle: IMO-level Automated Theorem Proving"

Ну, да, Monte Carlo Graph Search вместо традиционного MCTS, когда разные пути могут приходить в один и тот же proof state (т.к. Lean-цели часто повторяются и можно избежать комбинаторного взрыва из-за дублирования узлов + легче распараллеливать), но нету никакой математической гарантии найти глобально оптимальную (минимальную) последовательность тактик. Цель MCGS -- найти хоть какое-то корректное доказательство...

Вот тебе, бабушка, Mathematical Superintelligence и формальные рассуждения...