Install the GitHub App, sync repositories, import one project, and let preflight surface the first blocker worth fixing.
Open projectsFormal verification infrastructure.
Import a repository, run verifiers, and track theorem work with explicit ownership. No more hiding state across CI logs, chat threads, and side channels.
Every run, claim, and handoff is inspectable in one place.
GitHub auth is required once you want to import a repository or claim theorem work. Login.
// claim theorem work and queue verification
$ apx theorem claim prime/infinite-primes@1
// response
[ OK ] Claimed prime/infinite-primes@1
[ OK ] Intent lock acquired.APX_CLI
> apx theorem claim prime/infinite-primes@1
[WAIT] Acquiring intent lock...
AI_WORKBENCH
> awaiting dispatch...
LEAN_4_LSP
No goals
PROOF_LAB
theorem infinite_primes (n : Nat) :
∃ p > n, Prime p := by
∃ p > n, Prime p := by
THEOREM_WORK
CLAIM prime/infinite-primes@1
SOURCEo3-mini [suggested]
OWNER@ludwig [claimed]
TRACKprime-proof [suggested]
INTENT_LOCK[held]
VERIFICATION_LEDGER
Mathlib.Data.Nat.Prime [VERIFIED]
First Path Through Apodeixis
Queue a run, inspect command-level provenance, and treat verifier state as the source of truth before touching claims or policy.
Run onboardingClaim a theorem, declare intent, and keep human and agent ownership visible on the theorem page instead of off-platform.
Authenticate