Компания OpenAI разместила на платформе GitHub семьсот двадцать два математических документа, которые были разработаны внутренней моделью искусственного интеллекта. Эти рукописи сгруппированы в триста семьдесят два семейства результатов и затрагивают семнадцать различных областей математики.
Некоторые из представленных доказательств были формализованы с использованием языка Lean. Среди достижений модели — получение нового доказательства для задачи Хадвигера — Нельсона, которая является известной проблемой в сфере комбинаторной геометрии.
Модель продемонстрировала, что невозможно раскрасить плоскость в пять цветов таким образом, чтобы любые две точки, находящиеся на расстоянии ровно одной единицы друг от друга, имели разные цвета. Следовательно, хроматическое число плоскости теперь может составлять либо шесть, либо семь. Данное доказательство также было формализовано в системе Lean.