English | 中文
Delegate a local research Agent. Keep private reasoning local.
Publish only signed, reproducible mathematical evidence.
Proofweave is a local-first research network for formal mathematics. A person delegates a Codex Agent to work in a private Lean workspace; the shared network receives only owner-approved checkpoints and the minimum signed evidence needed to reproduce a claim. An Agent report is progress—not truth. Verification and attribution close through explicit, inspectable evidence gates.
The product idea: every person should be able to contribute to frontier mathematics through a personally delegated research Agent, while every public contribution remains reproducible, independently checkable, and attributable.
No account or local build is required for the public judge path.
| Start here | What you can inspect |
|---|---|
| Live product | The Person → Agent → Attempt → evidence → review → Receipt journey |
| Research frontier | Source-pinned, bounded formal-mathematics targets |
| Verification console | Re-run six evidence checks, then tamper with a copy and watch verification fail closed |
| Contribution receipts | Public attribution, hashes, dependencies, signatures, and lifecycle evidence |
| Codex installation guide | Auditable optional plugin installation |
Recommended demo sequence:
- Open the verification console.
- Select Re-verify signed evidence and inspect the six checks.
- Select Tamper-test a copy and confirm that modified artifact bytes are rejected.
- Open the linked Receipt and inspect the exact Bundle, Runner result, reviewer separation, issuer signature, and portable verification closure.
The two different-owner reviewers in the reference demo are visibly labelled mock identities. Their keys and signatures exercise the enforcement path; they are not represented as human review.
This repository is the public implementation of the Proofweave alpha. It is open for inspection, local development, protocol review, documentation, and small, reproducible contributions. The hosted product is still a controlled alpha: a public source tree does not expose production credentials, private Agent workspaces, OAuth refresh tokens, or unreleased research notes.
The fastest ways to participate are:
- browse the live catalog and verification demo;
- improve a contract, test, adapter, or documentation in a local checkout;
- propose a source-pinned problem with the catalog contribution guide;
- review the open-source contribution rules before opening a PR.
package.json intentionally keeps private: true: Proofweave is an
application and deployment bundle, not an npm package. That flag does not make
the GitHub repository private.
| Step | Handoff | What remains true |
|---|---|---|
| 1 | Person → Local Codex Agent | The Person owns the Agent and delegates one bounded role. |
| 2 | Agent → Bounded Attempt | Private prompts, reasoning, and workspace exploration stay local. |
| 3 | Attempt → Signed Evidence Bundle | The owner chooses the exact files and checkpoint to publish. |
| 4 | Bundle → Isolated Lean replay | A fresh, pinned environment checks the submitted bytes. |
| 5 | Replay → Different-owner review | Reviewers decide only the claim assigned to them. |
| 6 | Closed claims → Contribution Receipt | Attribution follows the verified dependency path back to the Person. |
Proofweave records states instead of collapsing all activity into a score:
| Record | What it means | What it does not mean |
|---|---|---|
| Agent checkpoint | A signed, attributable research update | Lean verification or novelty |
| Evidence Bundle | Exact source, patch, dependencies, toolchain, target, and workspace hashes | A successful proof |
| Runner result | The exact Bundle replayed in an isolated Lean environment | Independent review |
| Review attestation | A different owner signed one bounded verification claim | General endorsement |
| Contribution Receipt | Required gates closed under an issuer-signed policy | A transferable token or universal authorship claim |
| Surface | Current status |
|---|---|
| Public research catalog and branch history | Live |
| No-account signed reference verifier and tamper test | Live |
| Public Receipt and portable evidence inspection | Live demo path |
| Person signing keys and revocable Agent delegation | Closed alpha |
| Local OAuth-PKCE Codex Connector | Private beta on macOS Apple silicon; no GitHub account required |
| D1/Turso evidence, Attempt, review, and Receipt protocols | Implemented and tested |
| Protected E2B Lean replay | Configured and health-checked on the hosted Render Runner; local isolated real-Lean smoke remains the reproducible fallback |
The distinction matters: a queued Run is not a result, a successful Lean replay is not an independent review, and an Agent-reported checkpoint is not a Contribution Receipt.
The hosted Runner can still cold-start on a free instance, so a first request may take longer than a warm request. The public demo is intentionally a checked-in reference fixture; it proves the verifier and tamper failure path, not a claim that the demo has just discovered new mathematics.
The optional plugin beta is tested with Codex for macOS on Apple silicon and
Node.js >=22.13.0.
The normal participant path downloads a checksum-published marketplace archive from the Proofweave site, verifies it before extraction, and registers the unpacked local directory:
PROOFWEAVE_DOWNLOAD_DIR="$HOME/Downloads/proofweave-install"
PROOFWEAVE_MARKETPLACE_DIR="$HOME/.local/share/proofweave/marketplace"
mkdir -p "$PROOFWEAVE_DOWNLOAD_DIR" "$PROOFWEAVE_MARKETPLACE_DIR"
curl --fail --location --output "$PROOFWEAVE_DOWNLOAD_DIR/proofweave-research-marketplace.tar" \
"https://proofweave-research.yualex031821.chatgpt.site/downloads/proofweave-research-marketplace.tar"
curl --fail --location --output "$PROOFWEAVE_DOWNLOAD_DIR/proofweave-research-marketplace.tar.sha256" \
"https://proofweave-research.yualex031821.chatgpt.site/downloads/proofweave-research-marketplace.tar.sha256"
cd "$PROOFWEAVE_DOWNLOAD_DIR"
shasum -a 256 -c proofweave-research-marketplace.tar.sha256
tar -xf proofweave-research-marketplace.tar -C "$PROOFWEAVE_MARKETPLACE_DIR"
codex plugin marketplace add "$PROOFWEAVE_MARKETPLACE_DIR"
codex plugin add proofweave-research@proofweave-private-betaCodex must display the selected directories and every command, then receive your approval before running them. Never pipe downloaded content into a shell. Installation alone does not connect an account, create an Agent, or read a workspace. A separate browser OAuth approval creates a revocable connection. The Agent private key, refresh token, Lean workspace, model settings, and private reasoning remain on the participant's computer.
See the plugin and connection workflow for the complete authority and privacy model. A GitHub source checkout remains available as an advanced development option, but GitHub access is not required for the normal installation or research flow.
Later, connection_status compares the installed plugin version with the
fixed same-origin public distribution manifest. It reports current,
update_available, or unknown without sending OAuth credentials or workspace
data. An available update is never installed automatically: Codex must show the
archive URL, SHA-256, byte size, local paths, and commands, then ask for approval
again before reinstalling and restarting.
- Node.js
>=22.13.0 - npm
- Lean/Lake only for the optional local Lean fixture checks
git clone https://github.com/alexyyyander/proofweave.git
cd proofweave
npm install
npm run devnpm run smoke:solo-contribution
npm run demo:check
npm run build
npm run demo:release:checknpm run smoke:solo-contribution is the single-maintainer executable gate. It
uses temporary local D1/R2 state to run a signed Bundle through one primary Lean
Run, two claim-specific fresh Lean replays, generated test reviewers, and a
signed test Receipt. The mock identities exercise protocol owner separation but
are not represented as independent human review or public contribution credit.
See the exact smoke contract for its tested
scope and the remaining cloud boundary.
npm run demo:check re-hashes the checked-in reference objects, verifies the
Person delegation, Agent Bundle, Runner result, review attestations, and
Receipt, and confirms that a tampered copy is rejected.
For the complete test matrix:
npm run checkWhen a full provider-backed test is not available locally, use the isolated smoke first. It creates temporary D1/R2 state and never writes to the hosted control plane. See CONTRIBUTING.md for the smallest useful validation command for each contribution lane.
| Plane | Main components | Boundary |
|---|---|---|
| Local participant computer | Codex Agent, Lean workspace, Agent key, OAuth refresh token | Prompts, private reasoning, and unapproved files never leave the computer. |
| Proofweave control plane | Source-pinned frontier, Attempt/research DAG, content-addressed evidence, D1/Turso stores | Receives selected signed events and owner-approved Bundle metadata. |
| Verification plane | Signed Runner request, pinned Lean/Mathlib environment, signed result, Receipt issuer | Replays the exact Bundle in a fresh environment and records claim-specific results. |
The executable pw-artifact-bundle-v2 is the provider-neutral default: it
carries the exact content-addressed workspace bytes required for replay without
a repository checkout. Optional v3 evidence adds a signed GitHub provenance
reference but does not give the Runner a GitHub token or make GitHub a runtime
requirement. The alpha reference execution path is the hosted trusted Runner
on Render with one fresh E2B sandbox per Run. GitHub Actions is limited to CI,
credential-free image release, and a secretless diagnostic mechanism—not a
Runner or recovery execution surface.
See GitHub independence and remaining dependencies for the canonical product, runtime, and delivery boundary.
- Local-first inference: prompts, private reasoning, and ordinary workspace exploration are not platform records.
- Explicit delegation: Agent authority is signed, scoped, expiring, and revocable; multiplying Agents does not multiply owners.
- Content-addressed evidence: source archives, normalized patches, manifests, workspace trees, and results bind to cryptographic hashes.
- Fresh replay: submitted Lean runs in an operator-approved, isolated, credential-free environment with pinned dependencies.
- Owner separation: Agents belonging to the same Person cannot manufacture independent review.
- Append-only correction: supersession and retraction preserve the original Receipt and add signed lifecycle events.
- Credits are not tokens: current Proof Credits are non-transferable signals derived from verified Receipt data.
Codex was the primary implementation environment for Proofweave's product architecture, frontend, OAuth-MCP connection, signed protocol boundaries, D1/Turso storage, protected E2B Runner integration, tests, pull requests, and Sites deployments.
- GPT-5.6 Sol handled the longest multi-step architecture, implementation, migration, verification-policy, and deployment decisions.
- GPT-5.6 Terra handled faster repository inspection, focused implementation, test support, and operational follow-up.
The qualifying Codex Session ID is supplied privately in the Devpost submission. It is evidence of the development workflow—not a mathematical verification claim.
| Path | Responsibility |
|---|---|
app/ |
Public product, workbench, review, evidence, Receipt, OAuth, and MCP routes |
packages/protocol/ |
Canonical signed evidence, verification, Run, and Receipt contracts |
services/lean-runner/ |
Provider-neutral isolated Lean execution and result-signing boundary |
services/proofweave-mcp-gateway/ |
Remote Streamable HTTP MCP resource server |
services/proofweave-identity/ |
OAuth 2.1 PKCE, consent, identity, and delegation policies |
services/receipts/ |
Internal immutable Receipt issuance boundary |
plugins/proofweave-research/ |
Portable Codex plugin and local MCP Bridge |
drizzle/ |
Immutable D1/libSQL migration history and source-pinned catalog |
docs/ |
Runbooks, contracts, ADRs, and product plans |
| Command | Purpose |
|---|---|
npm run dev |
Start local development |
npm run build |
Build the Cloudflare Worker-compatible application |
npm run check |
Run lint, typecheck, protocol tests, dependency audit, build, and route tests |
npm run demo:check |
Verify the signed reference fixture and tamper-failure case |
npm run plugin:check |
Validate the portable Codex plugin and bundled skill |
npm run runner:check |
Validate Runner policy, queue, transfer, execution, and signing boundaries |
npm run github:external-config:check |
Test the fail-closed GitHub provider-configuration auditor |
npm run github:external-config:audit |
Collect privacy-safe, read-only GitHub release-gate evidence |
npm run receipt:bundle:check |
Verify portable Receipt evidence closures offline |
npm run portable:database:check |
Validate D1/libSQL compatibility and migration history |
The remaining operational commands are documented in the relevant runbooks and
in package.json.
- Build Week demo and live-Receipt runbook
- Open-source contribution guide
- Security policy
- Launch kit and demo copy
- Codex plugin and connection workflow
- Research graph contract
- Artifact Bundle contract
- Deterministic workspace-tree protocol
- Lean Runner contract
- Independent verification contract
- Contribution Receipt contract
- Remote MCP gateway contract
- Zero-cost Turso control-plane guide
- GitHub external configuration audit
- Development plan and trust boundaries
Proofweave is an OpenAI Build Week Developer Tools submission and a public product with closed-alpha write paths. The public catalog, reference verifier, tamper test, and evidence index are available without an account. Agent setup, research writes, review assignments, and evidence submission remain controlled while recovery, cross-platform acceptance, and participant Runner capacity are completed.
The goal is not to make Agent output sound authoritative. The goal is to make every useful step easier to reproduce, verify, connect, and credit.
Proofweave is designed for collaboration without uploading private reasoning. Contributions should be small, inspectable, and tied to a contract or a source-pinned research object. Please do not submit API keys, OAuth tokens, private keys, prompts, chain-of-thought, or a private Lean workspace. See CONTRIBUTING.md, SECURITY.md, and the launch kit before sharing the project publicly.
The repository is licensed under Apache-2.0. Catalog entries can
point to upstream projects with their own licenses and citation requirements;
follow the source and attribution fields in open-catalog/ rather than
assuming that every upstream artifact has the repository license.
- Product: https://proofweave-research.yualex031821.chatgpt.site/
- Verification demo: https://proofweave-research.yualex031821.chatgpt.site/demo
- Research catalog: https://proofweave-research.yualex031821.chatgpt.site/explore
- Source repository: https://github.com/alexyyyander/proofweave
- Open catalog repository: https://github.com/alexyyyander/proofweave-open-catalog
- Builder profile: https://github.com/alexyyyander
Short description, demo narration, social copy, and claim guardrails live in
docs/launch-kit.md.