Run Grace17 locally

You can start immediately in the browser Workbench: the full proof assistant runs in your browser, and nothing is sent to a server. For command-line use and for developing your own libraries, install it locally.

Requirements#

• Node.js 24 or later.
• Python 3, only for the independent Python checker.
• OCaml 5 with Zarith, only for the independent OCaml checker.

Install#

git clone https://github.com/grace17-prover/grace17.git
cd grace17
npm ci
npm run workbench

Open the local address the last command prints. Grace17 is not yet published as an npm package, though I hope to do that soon.

With Claude Code#

If you'd like to work with Grace17 through an AI agent, it is easy with Claude Code. Clone the repository as above, then install the Grace17 skill from inside Claude Code:

/plugin install grace17 --marketplace grace17-prover/grace17

The skill teaches the agent the write–check loop, the module conventions, and the pitfalls that cost the most time; inside a clone of the repository it loads automatically. The guide for AI agents describes the JSON interfaces the agent then uses to check proofs and read goal states.

Check a file from the command line#

node bin/g17.ts check --foundation ZF --module-root lib examples/Introduction.g17

Add --json for structured output. To see exactly which axioms a theorem depends on:

node bin/g17.ts axiom-audit --foundation ZF --module-root lib examples/Introduction.g17 --theorem Introduction.difference_of_squares

Next steps#

• Read the introduction for a tour from first proofs to the Nullstellensatz.
• Browse Cumulus, the mathematics library; every module opens in the Workbench.
• See building your own library to develop mathematics outside the Grace17 checkout.
• See contributing if you would like to help.