#lean
-
Модель Anthropic продвинулась в решении гипотезы Римана
Неопубликованная модель Anthropic не доказала гипотезу Римана, но заметно расширила границу, до которой её справедливость подтверждена. Работу проверили штатные математики компании и формализовали в Lean.
-
OpenAI анонсировала Astra — модель, решившую десять давних математических задач
OpenAI представила пока не выпущенную модель Astra, которая во внутренних испытаниях получила десять значимых результатов в математике и теоретической информатике. Компания называет её своей «следующей крупной моделью».
-
Ложное «опровержение» гипотезы Коллатца обнажило баг в ядре Lean
В ядре системы доказательств Lean нашли ошибку корректности: с помощью ИИ было построено формально принятое, но неверное «опровержение» гипотезы Коллатца. Автор Lean Леонардо де Моура опубликовал разбор случившегося.