How it works
Built on one record.
Everything on the platform writes to, or reads from, the same record. Here is what happens when a commit is checked, when an agent is asked to try a proof, when a statement quietly changes meaning, and how a blueprint reads it all back. These mirror the real services.
Verification
A commit is checked by the prover on isolated infrastructure, and the result is recorded with the manifest that produced it. Nothing enters the record on trust. The prover certifies the proof; whether the statement means what you intended is a separate question (see drift below).
- push (HMAC verified)
- policy guard, enqueue [queued]
- claim (SKIP LOCKED) [running]
- clone, run checker (lake build)
- command runs, logs
- index theorems, sign attestation
- complete [succeeded], recompute status
Tables: build_jobs, job_command_runs, artifact_attestations. Re-check any result at /api/v1/jobs/{id}/verify.
AI workbench
An AI run is gated by project policy before it starts, dispatched through a queue, and routed to a provider you control. The output lands as a suggestion, never a silent commit, and is attributed the same way a person would be.
- queue theorem AI run
- check policy (repo + team)
- allowed + limits
- acquire slot, quotas, insert [queued]
- claim queued run (SKIP LOCKED)
- provider call (BYOK / local)
- output, or 429 / error
- complete / fail, or retry_at (+15s)
Providers: OpenAI, Anthropic, Google, or a local model (BYOK). Policy: ai_enabled, human_gate_required, per-hour and concurrency quotas.
Semantic drift
When a statement changes under a passing build, the indexer compares it against the last verified snapshot and writes a classified finding. The web layer composes a significance band from typed axes and folds away compiler-generated noise, so a weakened theorem does not hide behind churn.
- extract head, tag origin (human / compiler)
- load baseline (repo + prover)
- compare: class, evidence, impact
- persist findings + policy action
- open changes surface
- load findings + stored origins
- compose significance, fold compiler-generated
- findings ranked by significance
Axes: semantic_class, origin (human_authored / compiler_generated), significance band (critical / high / notable / routine).
Blueprint as a lens
Import a LeanBlueprint project and its plan nodes bind to theorem IDs. Node status is then derived from the authoritative record: proof state plus active work, not a status anyone maintains by hand. The plan stays intent, the theorem facts stay authoritative, and the lens joins them.
- import LeanBlueprint
- parse nodes, edges, bindings (node to theorem)
- persist blueprint
- open project map
- load plan + theorem facts
- derive node status (proof + work state)
- plan over real results
Import: POST /api/v1/repos/{id}/blueprints/import/leanblueprint. Bindings: node to theorem_uid, handle, workspace doc, or work item. Edges: depends_on, proves, reduces_to.