Модель Astra от OpenAI решила десять сложных открытых математических задач Большинство из этих задач оставались недоказанными в течении десятков лет. Новая мультиагентная модель Astra смогла доказать их и формализировать доказательства при помощи Lean. Эту модель на этой неделе Сэм Альтман представил в Вашингтоне, это будет первая модель которая пройдёт через новый процесс государственного одобрения на релиз. Самое впечатляющее — на решение всех десяти задач суммарно ушло токенов меньше чем на $2000, по расценкам Sol. OpenAI пытались решить и другие сложные задачи, пока что безуспешно, но потенциал масштабирования здесь огромный. Блогпост Lean код доказательств @ai_newz