DOCSEARCHbyAlgolia
Submit Docs

AlphaProof Nexus Results

repository·main·Indexed 42 days ago

https://github.com/google-deepmind/alphaproof-nexus-results

A collection of successful Lean formal proofs and corresponding natural language mathematical proofs generated by AlphaProof Nexus. Includes data categorized by research areas such as AICollaborator, ErdosProblems, OEIS, and StacksProject, with instructions for verifying proofs using Lean 4 and lake.

Tokens
733
Snippets
2
Records
2
Agent score
6%

What's inside AlphaProof Nexus

  1. Understand the AlphaProof Nexus Results repository structure

    main

    This repository contains mechanically formalized Lean proofs and informal natural language math proofs generated by AlphaProof Nexus. The data is organized into two main directories:

    • APNOutputs/: Contains Lean proofs generated by AlphaProof Nexus, categorized by research area (e.g., AICollaborator, ErdosProblems, OEIS, StacksProject).
    • NaturalLanguageProofs/: Contains human-written prose proofs that follow the structure of the Lean proofs discovered by AlphaProof Nexus.

    Note that this repository only includes problems where successful proofs were discovered. For unsolved problems or the complete set of attempted OEIS problems, refer to the formal-conjectures repository.

    ├── APNOutputs/ -- Lean proofs generated by AlphaProof Nexus
│   ├── AICollaborator/ -- For section `Deployment in Mathematics Research`
│   ├── 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

  2. Build and verify AlphaProof Nexus proofs

    main

    To build the project and verify all Lean proofs, you must have Lean 4 installed on your system.

    Follow these steps:

    1. Fetch the necessary cache using lake.
    2. Build the project.

    Note on Parallelism: On large machines, you may encounter issues with too many open files. You can limit the number of threads used by lake by setting the LEAN_NUM_THREADS environment variable.

    # Fetch cache
lake exe cache get

# Build and verify proofs
lake build

# If running on a large machine, limit parallelism to avoid system limits
LEAN_NUM_THREADS=64 lake build