Axiom Math сообщила об автоматизированных доказательствах в Lean на фоне ускорения гонки в математике с ИИ

Axiom Math сообщила, что ее система Axiom Prover недавно получила несколько решений открытых исследовательских задач, полностью автоматизированных и формализованных в Lean без вмешательства человека. Компания также заявила, что установила мировой рекорд для задачи о четности функции разбиений.

Это произошло после стремительной борьбы за результат в задаче о ограниченных разрывах между простыми числами: Юлия Сталлеман улучшила показатель с 246 до 240, Axiom Math достигла 212, а OpenAI Astra позднее — 186. Axiom ожидает новых аналогичных состязаний с OpenAI и Anthropic, признавая, что конкуренты могут быстро превзойти ее результаты.

Axiom описала ИИ как инструмент, усиливающий возможности математиков, и отметила, что математические вопросы, включая пока нерешенную гипотезу Римана, сохраняются. Компания ожидает расцвета научных исследований в ближайшие шесть—восемь месяцев, однако это прогноз, а не подтвержденный результат.