For agents

Give an agent the short prompt below when you want it to search formalized mathematics persistently and iteratively rather than relying on one manual query.

Agent prompt

Copy into an agent session

You can use the Formalization Corpus to search existing formal mathematics across Lean, Rocq, Agda, Isabelle, HOL Light, HOL4, Mizar, Metamath, ACL2, PVS, and Twelf.

Use it proactively when looking for prior definitions, theorem statements, constructions, proofs, proof patterns, or reference implementations that may inform the current formalization task.

Resources:
- Search: https://dzackgarza.github.io/formalization-corpus/
- API reference: https://dzackgarza.github.io/formalization-corpus/api.html
- OpenAPI contract: https://formalization-corpus.dzackgarza.com/api/openapi.json
- Sources: https://dzackgarza.github.io/formalization-corpus/corpus.html
- Topics: https://dzackgarza.github.io/formalization-corpus/topics.html

The API is public, read-only, and requires no authentication. Inspect the OpenAPI document when you need exact request or response fields rather than loading all documentation into context.

Minimal search:
curl -s https://formalization-corpus.dzackgarza.com/api/search \
-H 'Content-Type: application/json' \
-d '{"Q":"Hasse invariant","Opts":{"MaxDocDisplayCount":20,"ChunkMatches":true,"NumContextLines":2}}'

Search iteratively. Try the mathematical term, standard synonyms, theorem names, notation-free names, nearby constructions, and proof-assistant-specific vocabulary. Inspect promising hits, then narrow with source/file/case/regular-expression filters when useful. Do not infer absence from one unsuccessful query.

Results are grouped by source file. ChunkMatches.Content is base64-encoded source text; decode it as UTF-8. Use Repository and FileName to locate relevant code, and consult the Sources/Topics pages when you need provenance or broader browsing.

Prefer progressive disclosure: inspect the contract, result chunks, and individual source files only as needed. Do not dump the whole corpus or documentation into context.

When you find useful prior work, report the source, proof assistant, file, relevant declaration/passage, and how it can be reused or adapted for the current task.

Resources

API referenceOperations, schemas, examples, and client snippets. OpenAPI 3.1The live machine-readable contract. TopicsBrowse sources by mathematical area.

CLI from the OpenAPI contract

You do not need a corpus-specific CLI. Restish reads OpenAPI descriptions at runtime and turns their operations into shell commands, help, completion, profiles, and structured output. Install Restish using its current installation instructions, then connect it directly to the live contract:

Register the Formalization Corpus API

restish api connect formalization-corpus https://formalization-corpus.dzackgarza.com \
  --spec https://formalization-corpus.dzackgarza.com/api/openapi.json
restish formalization-corpus --help

Restish caches the OpenAPI description locally; run restish api sync formalization-corpus after the API contract changes. This gives agents a normal shell interface without generating or maintaining another client. Restish can also expose registered APIs over MCP via its plugin when an MCP transport is preferable.

Optional MCP bridge

The API does not require a corpus-specific MCP server. A generic OpenAPI-to-MCP bridge can expose the live contract as local MCP tools. Direct API calls are often simpler; use MCP when you want the operations registered persistently as tools. The example below uses @ivotoby/openapi-mcp-server.

OpenAPI → MCP

npx -y @ivotoby/openapi-mcp-server \
  --api-base-url https://formalization-corpus.dzackgarza.com \
  --openapi-spec https://formalization-corpus.dzackgarza.com/api/openapi.json \
  --verbose false

Claude Code

Register the stdio bridge

claude mcp add formalization-corpus -- npx -y @ivotoby/openapi-mcp-server --api-base-url https://formalization-corpus.dzackgarza.com --openapi-spec https://formalization-corpus.dzackgarza.com/api/openapi.json --verbose false

Codex

~/.codex/config.toml

[mcp_servers.formalization_corpus]
command = "npx"
args = ["-y", "@ivotoby/openapi-mcp-server", "--api-base-url", "https://formalization-corpus.dzackgarza.com", "--openapi-spec", "https://formalization-corpus.dzackgarza.com/api/openapi.json", "--verbose", "false"]

OpenCode v2

Register the local MCP server

opencode2 mcp add formalization-corpus -- npx -y @ivotoby/openapi-mcp-server --api-base-url https://formalization-corpus.dzackgarza.com --openapi-spec https://formalization-corpus.dzackgarza.com/api/openapi.json --verbose false