Therefore MCP
Put proof search in your agent.
Create an account token, install the connection, then search proofs and run bounded Lean checks from your working context.
Create an MCP tokenRun once
codex mcp add therefore --url https://therefore.academy/api/mcp --bearer-token-env-var THEREFORE_MCP_TOKENSet THEREFORE_MCP_TOKEN in the environment that launches Codex. The secret is not written to Codex configuration.
Remote MCP
Give an agent proof search and a bounded Lean runner
Connect any client that supports stateless Streamable HTTP. Create a token in Studio, copy it once, and revoke it at any time. The server can read the public catalog and check bounded Lean code. It cannot publish, edit, verify, or delete records.
- search_proofs
- Bounded ranked summaries
- get_proof
- Complete source and provenance
- search_problems
- Dated open-problem records
- get_problem
- Statement, sources, and Lean targets
- search_project_declarations
- Local names and constants
- search_mathlib_source
- 10,000 complete pinned declarations
- search_mathlib_semantic
- Natural-language Mathlib search
- search_mathlib_declarations
- Live structural Loogle search
- search_packages
- All 782 pinned Reservoir packages
- get_package
- Head metadata or linked project detail
- list_projects
- Indexed project compatibility
- check_lean
- Account-limited Lean 4 check
https://therefore.academy/api/mcpTreat the token like a password. Native clients do not rely on browser cookies. Browser origins must be explicitly allowed by the deployment.
Public JSON API
One stable read path for every integration
Search responses omit full source to stay fast. Retrieve one slug for the full declaration, exact commit, source range, toolchain, license, and attribution. These endpoints are anonymous, read-only, and never expose account data or the runner.
Public catalog endpoints
- GET /api/v1/proofs
- Search proof records
- GET /api/v1/proofs/{slug}
- Retrieve a complete proof record
- GET /api/v1/problems
- Search open problem records
- GET /api/v1/problems/{slug}
- Retrieve an open problem record
- GET /api/v1/shapes
- Search project and Mathlib declarations
- GET /api/v1/mathlib
- Search Mathlib by meaning
- GET /api/v1/packages
- Search the pinned package index
- GET /api/v1/packages/{reference}
- Retrieve a package record
GET https://therefore.academy/api/v1/proofs?q=carleson&project=carleson&limit=10GET https://therefore.academy/api/v1/proofs/{slug}GET https://therefore.academy/api/v1/problems?q=prime&lean=yesGET https://therefore.academy/api/v1/problems/{slug}GET https://therefore.academy/api/v1/mathlib?q=the%20order%20of%20a%20group%20element%20divides%20the%20order%20of%20the%20groupGET https://therefore.academy/api/v1/shapes?q=_%20*%20(_%20%5E%20_)GET https://therefore.academy/api/v1/packages?q=additive+combinatoricsPrivate account API
Expensive work stays behind authentication
The browser playground sends signed-in checks to the private account API. Remote clients use MCP bearer tokens instead of browser sessions. Publishing and administration are not part of either programmatic surface.
Boundary at a glance
- /api/v1/*
- Anonymous public catalog reads
- /api/private/v1/*
- Signed-in browser account capabilities
- /api/mcp
- Scoped bearer token, public catalog allowlist, and Lean runner
- Server Actions
- Publishing, profile management, token creation, and administration
VS Code companion
Search from a Lean file
The first extension is implemented independently of Lean's internal editor APIs. Search selected text, find the declaration at the cursor, insert a Lean name, copy an import or citation, and open the pinned source.
Source-ready preview
Therefore for Lean
Marketplace publishing is intentionally separate. It requires a claimed publisher identity, final icon, VSIX review, and release credentials. The extension source and type checks live in this repository now.