Getting Started

Here are some resources to help you get started with Deduce.

• Installing Deduce
• Running Programs
• AI-assisted proof completion in Emacs (C-c C-a)
• Calling Deduce from an AI assistant (MCP)
• Learning Deduce

Installation

To get started with Deduce, follow these steps:

1. Install Prerequisites
2. Install Deduce
3. Choose a Text Editor

Install Prerequisites

You will need Python version 3.10 or later. Here are some instructions and links to download Python for many computer systems.

You will also need the Lark parsing library, which you can install by running the following command in the same directory as deduce.py

Install Deduce

You can find the stable releases of Deduce on github. Download the zip file and unpack it. To check that Deduce is working, go into the top deduce directory, and run python on the deduce.py script and the provided example file. (There is no executable for Deduce.)

You should see the following response from Deduce.

This response means that all the proofs in example.pf are complete and flawless! Most of the time you will be working on incomplete or flawed proofs and Deduce will try to give you helpful feedback. For example, if you replace the proof in example.pf with a ? as follows

and run Deduce again, you will see the following response.

The latest development branch of Deduce (not stable) is available here on github. It includes the source code for Deduce and for the Deduce web site.

Install and Configure a Text Editor

You can write Deduce in any text editor you want, and run Deduce through the terminal. For the editors below, we ship extensions that add syntax highlighting and (for Emacs) an interactive proof-editing experience backed by Deduce's Language Server Protocol (LSP) implementation.

• Emacs — bundled in the Deduce repo at editor/emacs/. Includes both a major mode (highlighting + indentation) and an LSP client with goal-at-cursor, refine-hole, case-split, induction skeleton, and more.

• VS Code — in-tree at editor/vscode/. Currently ships the debugger integration; syntax highlighting and the LSP client are on the roadmap.

Emacs

Requires Emacs 29.1 or newer (older Emacs would need a third-party eglot package, which is unsupported).

1. Install the Python LSP dependencies (only required if you want the interactive features beyond syntax highlighting):

This installs pygls (for the LSP server) and mcp (for the MCP server documented in the next section). Skip this if you only want syntax highlighting.

2. Add to your Emacs init file. Without use-package:

With use-package:

Opening any .pf file then enters deduce-mode automatically. With deduce-lsp loaded, eglot connects on first save (the first connection bootstraps the standard library; subsequent calls are warm). deduce-fill-hole is independent — see Set up an AI Assistant below for its API-key / model configuration.

3. Try the keybindings. Inside a .pf buffer:

Key	Action
M-.	Jump to a symbol's definition.
M-x imenu	Outline of top-level theorems / definitions / unions.
C-c C-g	Show the proof goal at point in a popup buffer.
C-c C-r	Refine the hole ? at point. Picks a tactic template by goal shape (e.g. arbitrary x:T for all x:T. ..., ?, ? for P and Q, reflexive for an obvious equality).
C-c C-c	Case split. Cursor on a ?; prompts (with TAB completion) for an in-scope variable, then replaces the ? with a switch skeleton (one branch per constructor) or cases (for or-shaped hypotheses).
C-c C-i	Induction skeleton. Cursor on a ? whose goal is all x:T. P(x) with T a union; replaces the ? with induction T and one case per constructor, including IH<N> bindings on recursive arguments.
C-c C-e	Eliminate / use-fact. Cursor on a ?; prompts for a hypothesis label and replaces the ? with a tactic chosen by the hypothesis's shape (destructure for and, cases for or, apply ... to ? for if then, H[?] for all, obtain ... from H for some, replace H for equality).
C-c C-f	Fill hole with a given. Cursor on a ?; replaces it with conclude <goal> by <label> for an in-scope hypothesis whose formula equals the goal. Auto-applies on a single match; otherwise prompts.
C-c C-a	Ask AI to fill the ? at point. Spawns an LLM-driven proof-completion sidecar; emacs stays interactive while the model iterates (up to 5 attempts, first valid proof wins). Requires API-key configuration — see AI-assisted proof completion in Emacs below.

For full details — including troubleshooting, customization, and a manual smoke test — see editor/emacs/README.md.

VS Code

The VS Code extension lives in-tree at editor/vscode/ and supersedes the older out-of-tree HalflingHelper/deduce-mode (no longer maintained). Today the extension ships the debugger integration: gutter breakpoints, the call-stack panel, the locals view, and the Debug Console all work over the same DAP adapter (python3 -m lsp.dap_server) the Debugger guide describes for the command line.

Syntax highlighting and the LSP-client wiring (goal-at-cursor, refine, case split, etc.) are tracked in editor/vscode/README.md's roadmap; for those interactive features today, use the Emacs mode above.

Running Deduce Programs

As mentioned above, Deduce is run by providing the deduce.py script with a *.pf file.

Suppose you have written thew following program in a file named hello.pf.

This program defines a new union type called Greeting, defines a variable world, and prints it out.

To run it, type the following command from within the deduce directory, or use the run functionality provided by your deduce editor.

You should see the output

AI-assisted proof completion in Emacs

C-c C-a asks a language model to fill the ? at point. The Emacs mode spawns the tools/claude_fill_hole sidecar, which requests a candidate proof, validates it against deduce.py, and splices the first valid one back into your buffer. Emacs stays interactive while the model iterates (up to five attempts; the first valid proof wins).

The binding comes from deduce-fill-hole — make sure your init file has (require 'deduce-fill-hole) from the Emacs setup above. You'll also need an API key for whichever model provider you point the sidecar at.

1. Install the sidecar's Python dependencies:

This pulls in anthropic and openai; the sidecar picks one at run time based on your backend choice.

2. Pick a backend and set its API key. Three common setups:

Anthropic / Claude (default; best quality, paid):

Indiana University REALLMs (free for IU researchers/faculty/staff, hosted on-prem):

OpenAI (paid):

Add the export line to your shell init file (~/.zshrc, ~/.bashrc, …) so the variable is available in every Emacs session. On macOS GUI Emacs, where shell variables sometimes fail to propagate into the GUI environment, the exec-path-from-shell package is a reliable fix.

3. (Optional) Pin the model and tune attempts. By default the sidecar uses claude-opus-4-7 (Anthropic backend) or gemma-4-31B-it (OpenAI-compat). To override:

The full set of defcustoms (with defaults) is reachable via M-x customize-group RET deduce-fill-hole RET, and documented in the editor/emacs/README.md customization table.

4. Try it. Open a .pf file with a ? to fill, place point on the ?, and press C-c C-a. The mode line shows progress; when the model returns a valid proof, it replaces the ? automatically. If every attempt fails validation, the sidecar surfaces its last error in the echo area and leaves the buffer as it was.

Calling Deduce from an AI assistant (MCP)

An AI assistant like Claude Code, Claude Desktop, or Cursor can call Deduce as a tool — checking a file, inspecting a proof goal, refining a hole, case-splitting — all driven by your conversation with the assistant.

Deduce supplies the bridge: an MCP (Model Context Protocol) server at lsp/mcp_server.py that speaks JSON-RPC on stdio and exposes Deduce's checking and proof-editing helpers as MCP tools. Your assistant brings its own login and model choice; on the Deduce side you install the server's Python dependencies, register the server with your assistant, and you're set.

The instructions below assume Claude Code is installed and authenticated; the shape is similar for other MCP clients (check their docs for the exact config-file location).

1. Install the MCP server's Python dependencies. Skip this if you already installed the LSP requirements above:

This pulls in the mcp Python package. Note which interpreter python3 resolves to here (which python3); step 2 must launch the same interpreter, or Claude Code will start a Python that doesn't have mcp installed.

2. Register the Deduce MCP server with your assistant. For Claude Code, create (or edit) .mcp.json in your Deduce checkout:

This form requires claude to be launched from the Deduce checkout (so Python can find the lsp package). To launch claude from a different directory — e.g. a separate proofs directory — give the absolute path to mcp_server.py instead. The server bootstraps itself from the file's location, so it works from any cwd:

To skip the standard library prelude, add "env": {"DEDUCE_NO_STDLIB": "1"}.

Alternative CLI registration. The default scope is local (per-user, per-project — won't be picked up by other contributors); pass --scope project to write to .mcp.json in the current directory instead:

After creating .mcp.json, restart claude so it discovers the new server. On first start in a project with .mcp.json, Claude Code prompts you to trust the server before invoking its tools.

3. Try it out. Start claude from the directory matching the .mcp.json form you picked in step 2 — the Deduce checkout for the -m lsp.mcp_server form, or anywhere for the absolute-path form — and ask something concrete:

Claude will call the Deduce MCP server's check_file tool, see the diagnostics, and respond. The full tool list:

Tool	What it does
check_file	Type-check and proof-check a .pf file; returns diagnostics.
goal_at	Return the proof goal + givens at a cursor position.
definition_of	Jump from a symbol to its declaration.
list_symbols	Outline of top-level theorems / definitions in a file.
refine_at	Refine a ? based on the goal's shape.
case_split_at	Replace a ? with a switch / cases skeleton on a chosen variable.
splittable_vars_at	List in-scope variables that case_split_at can target.
induction_skeleton_at	Replace a ? with an induction T skeleton.
eliminate_at	Replace a ? with a tactic that uses a chosen hypothesis.
eliminable_vars_at	List in-scope hypotheses that eliminate_at can target.
fill_from_given_at	Replace a ? with conclude <goal> by <label>.
matching_givens_at	List in-scope hypotheses whose formula equals the goal.

These are the same operations the Emacs mode binds to C-c C-r, C-c C-c, C-c C-i, C-c C-e, and C-c C-f — the assistant has the same proof-editing toolkit you do.

Deduce Introduction

This introduction to Deduce has two parts. The first part gives a tutorial on how to write programs in Deduce. The second part shows how to write proofs in Deduce.

• Programming in Deduce
• Writing Proofs in Deduce

I recommend that you work through the examples in this introduction. Create a file named examples.pf in the top deduce directory and add the examples one at a time. To check the file, run the deduce.py script on the file from the deduce directory.

The Deduce Reference manual is linked below. It provides an alphabetical list of all the features in Deduce. The Cheat Sheet gives some advice regarding proof strategy and which Deduce keyword to use next in a proof. The Syntax Overview page provides a brief overview of the syntax structure of deduce.

• Reference Manual
• Cheat Sheet
• Syntax Overview

Command Line Arguments

The deduce.py script supports command line arguments which are documented below. If an argument is not preceded by one of the keywords listed below, then it is treated as the name of a file or directory and will be processed by Deduce.

--dir directory-name

Tells Deduce to include the given directory-name in the list of directories to search when importing a file. For example, if test.pf imports Curry, and Curry.pf resides in a folder named howard, then --dir howard will allow test.pf to import Church. Note that --dir expects a directory name, not an individual file.

The rest of the command line arguments are useful primarily for the authors of Deduce. Users of Deduce can ignore them.

--no-stdlib

Deduce, by default, will import the entire standard library (in /lib of the Deduce repository). However if this argument is supplied, it will not do so.

--lalr

Deduce normally uses a custom recursive descent parser to parse any input files, however this argument will make Deduce instead use lark's LALR parser. This argument exists solely for checking that Deduce.lark maintains parity with the recursive descent parser.

--recursive-descent

Tells Deduce to use the recursive descent (default) parser. If --lalr is also supplied, then only the recursive descent parser will be used.

--recursive-directories or -r

Instead of only processing files in the specified directories, Deduce will also descend into any subdirectories.

--suppress-theorems

When a file contains one or more proof declarations inside of it, Deduce will create a .thm file. However, this argument makes it such that Deduce never creates such files.

--traceback

Prints out the exception if processing a file triggers an error.

--unique-names

Prints out all variables and types with an unique name. For example, if a program defines a variable x in several different scopes, x would instead be printed out as x.1 in one scope and printed as x.2 in a different scope.

--verbose

Makes Deduce print out the debug logs. It is generally recommended to use --traceback instead, as this argument can make Deduce print out thousands of lines.

By default, --verbose only prints debug logs for the current file. If ran as --verbose full it also prints debug logs for all imported files as well.

--error

Deduce will expect all files that it processes to contain an error. If there is a file that does not contain an error, Deduce will exit with a return code of 255.

--no-check-imports

Deduce will no longer check the proofs of imported files.

--compile

Translate the file to a self-contained C program instead of just checking it. Pair with -o <path> to control the output filename. See Compiling Deduce Programs to C for the full walkthrough.