AI creates novel proofs.
But who checks them?

AI models settled mathematical conjectures standing for decades, and autonomously verified sophisticated programs. But they can also be wrong with great confidence, producing broken proofs that look just like working ones. Proof assistants are a remedy for this challenge.

Download and install – or ask your agent to do it for you.

Isabelle The frontier proof assistant: every step of a proof checked, down to the axioms. BSD-style licence Download → PIDE MCP Connects your agent to Isabelle, working autonomously or side by side with you. LGPL-3.0 Download →

Meet Isabelle, a frontier proof assistant.

Proof assistants, like Isabelle, verify every step of a proof, all the way down to the axioms. Isabelle stands behind many of the biggest verified software and formal proof libraries ever built.

seL4 OS kernel The first OS kernel proved functionally correct – now running air-traffic and maritime control systems. sel4.systems → AWS Nitro Isolation Engine The first formally verified hypervisor, backing the world's largest cloud. aws.amazon.com → Apple corecrypto The cryptographic core of Apple's operating systems, with its post-quantum algorithms proved correct. security.apple.com → Archive of Formal Proofs One of the largest formal libraries for mathematics and computer science in the world. isa-afp.org →

40 years of research and engineering created a sophisticated system that not only checks proofs but also helps you write them. Isabelle ships the strongest automation of any proof assistant, most notably sledgehammer. And now, your agent gets to swing the hammer too.

Meet PIDE MCP, your agent's line to Isabelle.

PIDE MCP is your agent's live, two-way line to Isabelle. Thanks to Isabelle's powerful PIDE document engine, it can edit, query, and explore without ever waiting. You decide which tools it gets, and you can even add your own. Reactive, parallel, extensible.

One coding agent wired to three live Isabelle sessions A robot holds a tin can with three strings running from it, labelled PIDE MCP, to three Isabelle sessions: HOL, HOL-Analysis and HOL-Library. It edits two proofs and searches the third session for a definition. Both proofs come back with an error and the robot looks glum; it edits them again using what the search turned up, and this time both check clean, so it smiles. PIDE MCP HOL Scratch.thy lemma "(∑i<n. 2*i+1) = (n::nat)^2" sorry by auto by (induct n) (auto simp: power2_eq_square) 1 subgoal left checking… error · Failed to finish proof finished · 0 errors HOL-Analysis Cont.thy lemma "continuous_on S (λx::real. x * sin x)" sorry by simp by (intro continuous_intros) 1 subgoal left checking… error · Failed to apply initial proof method finished · 0 errors HOL-Probability Cauchy.thy lemma "Cauchy X ⟹ convergent (X::nat ⇒ real)" (no theories loaded) ↳ Cauchy X = cauchy_filter (filtermap X sequentially) session ready · no theories Cauchy.thy · 1 theory loaded find_entities · line 4 7 entities · Cauchy · HOL.Topological_Spaces:3557
  • Never blocked Answers stream in while Isabelle is proving. Your agent can always keep going.
  • One agent, many Isabelles PIDE MCP lets agents control several Isabelle sessions. Parallel and autonomously.
  • Built your way Choose which tools your agent gets, and build new ones that fit your project.

It speaks MCP, the language of your agent.

PIDE MCP is an ordinary MCP server, compatible with the agent you already use – Claude Code, Codex, OpenCode, and many more – each gets its own line to Isabelle.

Coding agents that speak MCP Four coding agents around an Isabelle editor. Point at one and it opens its own connection: an initialize message goes out, a response comes back, and the editor names it. Claude Code holds the line until another agent takes it. HOL Scratch.thy theorem "sqrt 2 ∉ ℚ" sorry no client connected connected · Claude Code connected · Codex connected · OpenCode connected · your agent initialize response Claude Code initialize response Codex initialize response OpenCode initialize response …and many others

Let your agent work autonomously or work beside it.

Hand it a goal, a paper, a book and come back to a formalised result. Or stay and work alongside it in symbiosis. Switch at any moment.

An agent and a person fixing the same proof together The robot is wired into a file and tries a proof that almost works; Isabelle reports an error and the robot looks glum. The woman at the same file says "let me help", runs Sledgehammer, and the missing lemma turns up – then both are smiling. HOL Scratch.thy lemma "(∑i<n. 2*i+1) = (n::nat)^2" sorry by (induct n) auto by (induct n) (auto simp: power2_eq_square) sledgehammer 1 subgoal left checking… error · Failed to finish proof sledgehammer: (auto simp: power2_eq_square) finished · 0 errors edit get_state 1 error let me help

Now take on what seemed out of reach.

  • Mathematical discovery Autoformalization of classic results, and long-standing arguments settled for good.
  • Verified software Verified compilers, kernels, controllers that do the right thing and the right thing only.
  • Security and cryptography Protocol and cryptographic guarantees checked down to the axioms.
  • Living libraries Large formal libraries ported, refactored, and repaired while everything underneath keeps moving.

Get started today.

Download and install – or ask your agent to do it for you.

Isabelle The frontier proof assistant: every step of a proof checked, down to the axioms. BSD-style licence Download → PIDE MCP Connects your agent to Isabelle, working autonomously or side by side with you. LGPL-3.0 Download →

Want to know more?

PIDE MCP Preprint Learn more about the design of PIDE MCP. PDF · Zenodo Read it →
Questions and Support Contact us on the PIDE MCP stream on Isabelle Zulip or message Kevin Kappelmann. Isabelle Zulip Ask →