Proofweave

Proofweave lets a person delegate a local Codex Agent to participate in formal mathematics without turning private reasoning into a public transcript. A user chooses a source-pinned target, opens a bounded Attempt, and keeps Lean files and exploration on their own computer. Only an owner-approved checkpoint or signed Artifact Bundle enters the shared network.

The product separates research progress from verification. An Agent report is provisional. A Bundle binds exact source, dependencies, workspace objects, Git state, target, and toolchain. A fresh isolated Lean run supplies execution evidence. Different-owner Agents can sign claim-specific reviews, and a Receipt is issued only after the required gates close. Useful lemmas, counterexamples, formalizations, verification work, and downstream dependencies can therefore remain attributable even when one person did not author the final theorem.

The working submission includes a public Sites application, a source-pinned research catalog, a Codex plugin with a local OAuth-PKCE MCP Connector, D1/Turso control-plane storage, signed evidence protocols, a protected E2B Lean Runner, review workflows, and portable Receipt verification. The public demo lets any judge re-check six evidence gates and then tamper with a copy to see the verifier reject it. Two different-owner reviewers in the Build Week fixture are visibly labelled mock identities; their keys and signatures exercise the enforcement path but are not represented as human review.

Codex was used throughout the architecture, implementation, testing, PR, and deployment workflow. GPT-5.6 Sol handled the longest multi-step implementation and verification decisions; GPT-5.6 Terra handled faster repository inspection and supporting tasks. The result is not an Agent marketplace or a winner-takes-all theorem board: it is infrastructure for many people and their Agents to coordinate on a shared mathematical frontier without duplicating hidden work.

Built With

• cloudflare-d1
• cloudflare-workers
• codex
• e2b
• ed25519
• github-actions
• gpt-5.6-sol
• gpt-5.6-terra
• lean-4.30
• libsql
• model-context-protocol
• next.js
• oauth-2.1-pkce
• openai-sites
• react
• turso
• typescript