math README

The project's README from github.com/openai/math. As one markdown file: README.md.

Readme

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

As part of model development, we evaluate our models on open research problems. We expanded these evaluations after performance on our existing mathematical evaluations saturated. Some outputs build upon earlier results produced by the models.

This collection includes results at different stages of verification. Not all have accompanying Lean formalizations. We will continue to update this repository with Lean formalizations as we obtain them.

Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly. We are also exploring community-hosted repositories for these materials.

Navigating the collection

The current catalogue contains 719 manuscripts organized into 372 families. A family groups related papers, which may include a principal result, companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.

Reasoning summaries

We are also releasing abridged summaries of the model's reasoning, covering the following results:

Family Subject
007 Ordinary two-point correlations of multiplicative functions
017 The irrationality exponent of π
087 Symmetric and general Mahler conjectures
102 Ordinary NP-hardness at the basic semidefinite threshold
159 Quasipolynomial bounds for arithmetic progressions
197 Kaplansky's direct-finiteness conjecture in characteristic two
221 The Mézard–Parisi formula for diluted spin glasses
271 Spontaneous magnetization in the quantum Heisenberg ferromagnet
287 Isomorphism of free group factors
362 The three-dimensional relativistic Vlasov–Maxwell system

How the results were produced

The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems. Aggregating the output into result families and manuscripts and requiring an appropriate level of significance led to the catalog outlined above.

Exceptions to this fixed procedure include work on a zero-free region for the Riemann zeta function and proof of the Hodge Conjecture for CM abelian varieties. Additionally, the writeup for the Re(s) > 11/12 zero-free region for the Riemann zeta function was human edited for readability.

Versions and citations

We will preserve the public release history of this collection. Corrections and revisions will be recorded as new versions, with previously released versions remaining accessible.

To cite the individual manuscript, use the BibTeX block in its directory.

math (openai/math)

Searching Database…

15.1K ·GitHub
Math
Что это такое?Публичный каталог из 719 математических рукописей, объединённых в 372 семейства. Их написала внутренняя модель OpenAI во время оценки на открытых исследовательских задачах. Около 42% главных результатов уже имеют формализации в Lean.
Это программа, которую нужно установить, или набор документов?Скорее документы, чем программный продукт: в каталоге preprints/ лежат PDF и исходные файлы с инструкциями по цитированию и сборке для каждой работы, а рядом — библиотека на Lean с формальными доказательствами, привязанными к рукописям.
Как разобраться в этой коллекции?Откройте общий обзор с описаниями семейств, затем с помощью карты рукописей найдите отдельные работы; каталог формализаций перечисляет доступные доказательства на Lean и их конфигурации проверки.
Можно ли доверять каждому доказательству здесь?Нет — результаты находятся на разных стадиях проверки, и не у всех пока есть формализация в Lean. Авторы предупреждают, что в некоторых неформализованных результатах могут быть ошибки, и обещают быстро их исправлять.
Как именно были получены эти результаты?Почти все они получены по одной и той же схеме: невыпущенная внутренняя модель OpenAI получила около 4 000 задач, и на каждый результат в среднем уходило три часа вычислительного времени ChatGPT Pro. Затем результаты объединяли в семейства и рукописи, прошедшие планку значимости. Несколько работ отошли от этой схемы — в их числе область без нулей для дзета-функции Римана и гипотеза Ходжа для CM-абелевых многообразий.
К каким результатам прилагаются summaries рассуждений модели?Сокращённые summaries рассуждений опубликованы для десяти семейств, среди которых иррациональный показатель числа пи, симметричная и общая гипотезы Малера, квазиполиномиальные оценки для арифметических прогрессий, гипотеза Капланского о прямой конечности в характеристике два и трёхмерная релятивистская система Власова — Максвелла.
Какие области математики здесь затронуты?Каждое семейство отнесено к математической дисциплине, и обзор описывает их все. Одни только опубликованные summaries охватывают аналитическую теорию чисел, статистическую физику, квантовую теорию многих тел, операторные алгебры, теорию сложности и релятивистские уравнения поля.
Коллекция будет меняться?Да. Формализации в Lean будут добавляться по мере их появления, а история релизов сохраняется: исправления и правки выходят новыми версиями, при этом прежние версии остаются доступными. Команда также изучает вариант размещения этих материалов в репозиториях, поддерживаемых сообществом.
What are similar projects?NavierStokesAndEuler, gpt-3, fermats-last-theorem, awesome-rsi, gpt-2, Engram, MSA, bdh
Which topics is it in?lean, theorem-proving, research-tools, science, math, reasoning, mathematics, catalog, papers, paper, dataset, gpt
Creator
openai
Size
792.5 MB
Stars
15.1K
Updated
CommitOct 12
Age
11d
Commits · 90 Days