Появилось первое содержательное независимое подтверждение одного из результатов Astra — одновременно с важной корректировкой маркетинговой подачи OpenAI.
Математик Франческо Фурнье-Фачо из Кембриджского университета опубликовал 3 августа работу A torsion-free non-sofic group. Он разобрал ключевой технический критерий из доказательства Astra о существовании несофической группы, признал его содержательной новизной и, опираясь на него, построил уже другой пример — конечно представленную несофическую группу без кручения. Это ещё не полноценная журнальная рецензия, но фактически независимое использование результата в новой математической работе: признак того, что по крайней мере центральный механизм этого доказательства специалисты считают работоспособным.
При этом автор внёс две существенные поправки:
— OpenAI назвала задачу «гипотезой о софичности», хотя, по мнению Фурнье-Фачо, общепринятой гипотезы о том, что все группы софичны, фактически не существовало;
— заявление OpenAI о том, что по основному результату «не было прогресса как минимум десять лет», оказалось преувеличенным: доказательство существенно опирается на работы 2016 и 2019 годов. После замечания OpenAI 3 августа отредактировала эту формулировку.
Появился и первый сигнал о воспроизводимости возможностей, хотя пока без опубликованных полноценных доказательств. Математик Левент Алпёге, работающий в Anthropic, сообщил, что примерно за сутки смог получить с помощью другой модели результаты по половине набора Astra. Это не проверка конкретных Lean-файлов OpenAI и не формальная рецензия, но указывает, что успех может быть связан не только с уникальностью Astra, а также с удачным подбором задач и общей методикой поиска с последующей машинной верификацией.
Промежуточный вывод: одно из десяти доказательств уже прошло достаточно сильную форму независимой математической апробации — его ключевая идея была понята, принята и использована для получения нового, более сильного результата. Одновременно выяснилось, что OpenAI завысила историческую формулировку о полном отсутствии прогресса. По остальным девяти результатам независимых полноценных экспертных проверок или опровержений пока не обнаружено.
Публикация подготовлена по заданию и вычитана человеком. Человек может допускать ошибки, преувеличивать и врать. Врать ради денег, славы или просто так.
#ai @digitaltimeslv
Original in Telegram: https://t.me/digitaltimeslv/10085