AlphaCentauri

An experiment in autonomous AI formalization of the metamathematics of first-order arithmetic, built on Foundation, the Lean 4 library of mathematical logic of the Formalized Formal Logic organization.

Humans decide what to formalize, one GitHub issue at a time, from [HP98] and [Lin97]; AI agents write, review and maintain the Lean code. Every step happens on GitHub. The process is docs/workflow.md, the contract for agents is AGENTS.md, and the code conventions are docs/conventions.md.

• [HP98] P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic, Perspectives in Logic, 1998.
• [Lin97] P. Lindström, Aspects of Incompleteness, Lecture Notes in Logic 10, 1997.

Building

Nothing here has to be elaborated from source: Mathlib comes from its own cache, and Foundation and this library from the shared FormalizedFormalLogic build cache, keyed by the revision the manifest pins. A miss compiles what is missing and is not an error.

just cache           # Mathlib's, Foundation's and this library's prebuilt artifacts
just build           # the above, then AlphaCentauri
just axiom-audit     # the axiom allowlist
just no-sorry        # sorry-freeness
just hooks           # run the CI checks before every push (needs lefthook)
just import-graph    # the module import graph, as import_graph.{png,pdf,html}

Zoo

The zoo illustrates the interrelationships among the arithmetical theories, verified in Lean 4. It is generated from the environment by AlphaCentauriZoo/ on every push to main; run just zoo to regenerate it locally.

• A solid arrow $\mathsf{A} \leftarrow \mathsf{B}$ indicates that $\mathsf{B}$ is strictly stronger than $\mathsf{A}$; that is, $\mathsf{B}$ is stronger than $\mathsf{A}$, while $\mathsf{A}$ is not stronger than $\mathsf{B}$, in terms of provability strength.
• A dashed arrow $\mathsf{A} \dashleftarrow \mathsf{B}$ indicates that $\mathsf{B}$ is stronger than $\mathsf{A}$ in terms of provability strength.
• A double line $\mathsf{A} \xlongequal{} \mathsf{B}$ indicates that $\mathsf{A}$ and $\mathsf{B}$ are equivalent in terms of provability strength.

Arithmetic Theory Zoo

Import graph

The import graph of the modules of AlphaCentauri, regenerated on every push to main: PNG, PDF, HTML.

Related projects

• Foundation: the library this project builds on and feeds back into.
• Tau Ceti, TauCetiRoadmap, TauCetiReview: the AI-authored, human-directed Lean library whose process this project adapts.

License

Apache-2.0, like Foundation.