# 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:

```text
├── 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`
└── 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](https://github.com/google-deepmind/formal-conjectures/tree/auto_oeis/FormalConjectures/OEIS/Auto) 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](https://github.com/google-deepmind/formal-conjectures/blob/auto_oeis/FormalConjectures/OEIS/Auto/THEOREM_MAPPING.txt).
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](https://github.com/google-deepmind/formal-conjectures/tree/main/FormalConjectures/ErdosProblems).


## Building

Ensure you have Lean 4 installed (see [installation instructions](https://lean-lang.org/lean4/doc/quickstart.html)).

To build the project and verify all proofs, run:

```bash
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](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Too.20many.20open.20files.20in.20system/near/569952616).

## 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.