Search formalized mathematics.

Definitions, constructions, theorem statements, and proofs from Lean, Rocq, Agda, Isabelle, HOL Light, HOL4, Mizar, Metamath, ACL2, PVS, and Twelf.

Browse

SourcesSources grouped by proof assistant. TopicsSources organized by mathematical topic. For agentsA compact prompt, API pointers, and optional MCP setup. APIJSON search endpoint, query syntax, and response format.