Модель Astra от OpenAI решила десять сложных открытых математических задач

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

Самое впечатляющее — на решение всех десяти задач суммарно ушло токенов меньше чем на $2000, по расценкам Sol. OpenAI пытались решить и другие сложные задачи, пока что безуспешно, но потенциал масштабирования здесь огромный.

Блогпост
Lean код доказательств

@ai_newz