Private beta

Apodeixis beta

A coordination layer for formalization projects. It runs the prover on real commits and tracks who owns each theorem across the whole project, person or agent.

Small on purpose. There’s a lot running behind each project: prover runs, semantic extraction, indexing, drift checks, the AI workbench. All of it costs real compute, and we want to learn from real projects before we scale.

Why this exists

Proof attempts are getting cheap. AI produces more plausible Lean than any team can read. What was a tooling problem is now a judgment problem.

Informal verification is really not sufficient. Marrying informal verification with formal verification like Lean is the next big breakthrough.

Thang Luong, Future of Mathematics Symposium, Stanford, May 2026

The prover decides. A draft only enters the record once Lean accepts it on a specific commit, with the exact command logged.

Millions of lines of Lean code, everything looks fine. We will lose the skill of constantly checking it.

Sergey Gukov, Fields Medalist Roundtable, same day

Every accepted result keeps the manifest that produced it: commit, toolchain, prover version, command, extraction contract. You can re-run the check yourself.

There may be a large gray market of off-brand mathematics. Fly-by-night, AI-generated, probably-true theorems.

Ravi Vakil, same panel

Each theorem keeps a contribution log: who drafted the proof, who ran the prover, who reviewed it. Agents and humans show up the same way.

Four questions we want it to answer

What can we trust?
What should we work on next?
What should we ask an agent to try?
What mathematical meaning is at risk?

What the beta does today

Import a GitHub repository.
Queue Lean verification against a real commit.
Inspect commands, logs, extracted theorem data, and the published files list.
Open a theorem workspace with explicit ownership across people and agents.
Import a LeanBlueprint project and bind plan nodes to theorem IDs.
Route AI drafts through project policy and verified Lean runs.

Not yet in the beta: Coq and Isabelle extractors, public-key signing for published files, semantic-drift CI, and the AI proof benchmark with verifier review.