OpenAI published a GitHub repository called openai/math containing 719 mathematical manuscripts across 372 problem families, which the company says were produced by an internal model working on open research problems, according to the repository.
About 42% of the collection's top-line results include formal proofs written in the Lean proof assistant, OpenAI said, a step meant to verify the model's claims by machine rather than rely on the model's own account of its reasoning.
The repository includes manuscript maps, overviews and a formalization catalog, and covers results across multiple mathematical disciplines, including work related to the Mahler conjectures and the Mezard-Parisi formula, according to the project. It is released under the Apache 2.0 license.
OpenAI said the collection documents its model's performance on open problems at varying stages of verification, and the repository invites outside mathematicians to check the work.
Mathematical claims from a language model are easy to generate and hard to trust. Publishing both the manuscripts and machine-checkable Lean proofs for nearly half of the top results gives outside mathematicians a way to verify the claims directly instead of taking OpenAI's word for it, which is the harder and more useful kind of release.