Математики давно просят ИИ-лаборатории показывать настоящие доказател…

Математики давно просят ИИ-лаборатории показывать настоящие доказательства, которые можно проверить, вместо постов в блогах.

OpenAI ответила репозиторием на GitHub: 722 статьи, объединённые в 372 результата.

Их написала внутренняя модель, которую пока не выпустили. Обычные математические тесты она уже прошла почти до потолка, поэтому ей дали около 4 000 открытых исследовательских задач. На один результат уходило в среднем три часа вычислений, а ответы модель оформляла как научные статьи.

Среди задач есть очень известные: гипотеза Малера 1939 года, гипотеза Капланского, изоморфизм факторов свободных групп.

Но проверено пока не всё. Формальное доказательство в Lean, которое проверяет программа, есть у 162 статей из 722. OpenAI сама предупреждает, что в остальных могут быть ошибки.

Теперь слово за математиками. Им наконец есть что проверять

https://github.com/openai/math