A coordination layer for formal proofs.
Import a repository. Run the prover on real commits. Track who owns each theorem, person or agent, across the whole project.
No state hidden in CI logs, chat threads, and side channels. Every run, claim, and handoff lands in one record.
∃ p, n ≤ p ∧ p.Prime := by
What it does
One record of every proof attempt
Apodeixis indexes Lean, Coq, and Isabelle repositories and records, for every theorem: whether the prover accepts it and on which commit, who owns the attempt, what blocks it, and whether the statement has changed.
What can we trust?
Verification is pinned to a commit and command.
A proof counts as verified only when the prover accepts it on a specific commit, with the exact build command stored. Re-run it and you get the same result. Whether the statement says what you meant is tracked separately, as intent and drift.
How verification works →Re-run the manifest yourself. Same result.
What should we work on next?
One status view per repository.
A single triage view per repository. The status pill says whether anything needs attention; the table lists what to act on: unowned proofs, dependency blockers, policy holds.
Open a project →| Proof | State | Why blocked | Owner |
|---|---|---|---|
flt/frey-package-reduction | done | no blocker | @ludwig |
flt/frey-curve-modular | blocked | 4 dependency blockers | unowned |
flt/mod-p-reducible | in_progress | no blocker | @ludwig |
What should we ask an agent to try?
People and agents are tracked the same way.
Claim a theorem and state your intent; the lock is visible to everyone. AI drafts go through project policy and land as suggestions, not silent commits. Humans and agents get the same attribution.
See the workbench →What mathematical meaning is at risk?
Statement changes are classified, not just detected.
A statement can change under a passing build. Apodeixis classifies each change by kind, origin, and significance: compiler-generated noise folds away; a weakened theorem is ranked for review.
Read on drift →The build passes. The meaning moved.
Blueprint as a lens
The plan and the proofs are one object.
Import a LeanBlueprint project and bind each plan node to a theorem. The node state comes from the verified record: done, ready, or blocked, not a status you maintain by hand. The blueprint is a view over real results, not a document beside them.
How the lens works →Node state comes from the record, not a hand-edited doc.