google-deepmind/alphaproof-nexus-results

google-deepmind/alphaproof-nexus-results

Description: Lean math proofs generated by AlphaProof Nexus and accompanying natural language prose proofs.

Language: Lean

License: Apache-2.0

Stars: 234

Forks: 19

Open issues: 1

Created: 2026-05-13T09:59:21Z

Pushed: 2026-06-05T14:10:22Z

Default branch: main

Fork: no

Archived: no

README:

AlphaProof Nexus Results

This repository contains mechanically formalized Lean proof and informal natural language math proof results for the AlphaProof Nexus paper. The directory structure is as follows:

├── APNOutputs/ -- Lean proofs generated by AlphaProof Nexus
│ ├── AICollaborator/ -- For section `Deployment in Mathematics Research`
│ │ ├── AdditiveCombinatorics/ -- Additive Combinatorics
│ │ ├── AlgebraicGeometry/ -- Algebraic Geometry
│ │ ├── Graphs/ -- Graph Theory
│ │ ├── Optimization/ -- Optimization Theory
│ │ └── QuantumOptics/ -- Quantum Optics
│ ├── ErdosProblems/ -- For `Erdős Problems` paragraph of `Systematic Evaluation on Open Problems`
│ ├── OEIS/ -- For `OEIS Problems` paragraph of `Systematic Evaluation on Open Problems`
│ └── StacksProject/ -- Problems from the Stacks Project
└── NaturalLanguageProofs/ -- Human-written prose proofs following the structure of the Lean proofs discovered by AlphaProof Nexus
├── AICollaborator/ -- Proofs for subset of problems from AlphaProof Nexus human collaborations
├── ErdosProblems/ -- For Erdős problems
└── OEIS/ -- Proofs for subset of OEIS problems

This repository contains only problems where successful proofs were discovered by AlphaProof Nexus. The complete set of Lean problems originating from OEIS that we attempted with AlphaProof Nexus (including ones that were not solved) is also available, along with a mapping from Lean theorem names to OEIS problems. The complete list of Erdős problems we attempted is described in erdos_problems_attempted.txt, and Lean formalizations for these unsolved problems are available here.

Building

Ensure you have Lean 4 installed (see installation instructions).

To build the project and verify all proofs, run:

lake exe cache get
lake build

Note that on large machines you may need to limit the parallelism of lake by using LEAN_NUM_THREADS=64 lake build or similar. See this zulip thread.

License and disclaimer

Copyright 2026 Google LLC

All software is licensed under the Apache License, Version 2.0 (Apache 2.0); you may not use this file except in compliance with the Apache 2.0 license. You may obtain a copy of the Apache 2.0 license at: https://www.apache.org/licenses/LICENSE-2.0

All other materials are licensed under the Creative Commons Attribution 4.0 International License (CC-BY). You may obtain a copy of the CC-BY license at: https://creativecommons.org/licenses/by/4.0/legalcode

The content may be based on third party sources and may in some cases include third party content. The original source for each conjecture is indicated by a URL within the source file. Third party content may be subject to different licensing requirements. In particular:

• Material from The Online Encyclopedia of Integer Sequences available at

https://oeis.org and released under the Creative Commons Attribution-Share-Alike License 4.0.

• Material from Erdos Problems available at https://www.erdosproblems.com/
• Material provided by Gergely Berczi
• Material provided by Mario Krenn

Unless required by applicable law or agreed to in writing, all software and materials distributed here under the Apache 2.0 or CC-BY licenses are distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the licenses for the specific language governing permissions and limitations under those licenses.

This is not an official Google product.