Install the GitHub App, sync repositories, import one project, and let preflight tell you the first real blocker.
Open projects
~*~ apodeixis: formal verification infrastructure ~*~
// 2026
// 2026
# Bring a proof project online, then work theorem-by-theorem.
Apodeixis turns formal proof projects into a web-native theorem workbench: import a GitHub repository as a project, verify it cleanly, claim theorem work, and keep human and agent collaboration explicit.
Built for demo teams and future formalization groups who need discovery, collaboration, and verification to feel like one product instead of a pile of dashboards.
The product boundary is simple: get a project online, open theorem work safely, and make every run and handoff auditable.
// trigger a verification pipeline
$ apodeixis pipeline push --branch main --prover lean4
// response
[ OK ] Job 1337 queued.
[ OK ] Artifact signed: SHA256:4f8b...USER_SESSION
> apodeixis lock acquire
[WAIT] Negotiating...
AI_REASONING_ENGINE
> awaiting evaluation...
LEAN_4_LSP (STATE)
No goals
WORKSPACE_BUFFER
theorem infinite_primes (n : Nat) :
∃ p > n, Prime p := by
∃ p > n, Prime p := by
CLAIM_ROUTER
CLAIM thm/infinite_primes
PROPOSED_BYgpt-5.x [TRACK_PLAN]
OWNER@ludwig [ACKED]
POLICYhuman_gate_required [PENDING]
TRACKprime-proof [SUGGESTED]
INTENT_LOCK[HELD]
VERIFICATION_LEDGER
Mathlib.Data.Nat.Prime [VERIFIED]
## First User Journey
Queue the first run, inspect command-level provenance, and treat verifier state as the source of truth before editing claims or policy.
Run onboardingOpen a theorem, record claim and intent, and keep human and agent ownership visible instead of hidden in side channels.
Authenticate## Why This Workbench
- [+] Discovery and ownership live on theorem pages, not in external spreadsheets or chat threads.
- [+] Human-gated agent work is explicit, so review and responsibility stay legible.
- [+] Verification provenance is attached to theorem and project surfaces, not buried in CI logs.
# Live Project Snapshot
Rust API 401: authentication required