# disprove

Attempt to disprove theorems by proving the negation.

## Input Parameters

`content` · str · required · Lean source code

The Lean source code to be processed by this tool.

`names` · list[str] · Theorem names to process

Optional list of theorem names to process. If not specified, all theorems are processed. Requesting a name not found in the code returns an error. When `theorems_only` is `false`, these select over all declarations (not just theorems).

`indices` · list[int] · Theorem indices to process

Optional list of theorem indices to process (0-based). Supports negative indices: `-1` is the last theorem, `-2` is second-to-last, etc. If not specified, all theorems are processed. When `theorems_only` is `false`, these select over all declarations (not just theorems).

`terminal_tactics` · list[str] · default: `['grind']` · Tactics to try when attempting to disprove

Tactics tried in order to prove the negation. `grind` often works for false statements. Defaults to 'grind'.

`theorems_only` · bool · default: `True` · Process theorems/lemmas only

If `true` (default), only `theorem`/`lemma` declarations are processed. Set to `false` to process all declaration kinds (`def`/`instance`/`abbrev`/`opaque`/etc). When `false`, `names` and `indices` select over all declarations rather than just theorems.

Note: on this tool, operations on non-theorem kinds are a no-op.

`verbosity` · float · default: `0` · Pretty-printer verbosity level (0-2)

0=default, 1=robust, 2=extra robust. Higher levels produce more explicit type annotations. Use when default output has ambiguity errors.

`ignore_imports` · bool · default: `True` · Ignore import mismatches

Controls import statement handling:

- `true` (default): Ignore the imports in `content` and substitute the environment's default header. This uses the pre-built cached environment, so it is fast. The substituted code is returned in the `content` field.
- `false`: Process the imports in `content` exactly as written. This is significantly slower (the cached environment cannot be reused) and may produce inconsistent or incorrect results if a required dependency such as `Mathlib.Tactic` is missing. A warning is returned in these cases. See the troubleshooting page for more details.

`environment` · str · required · Lean environment or version

The Lean environment to use for evaluation. Each environment includes a specific Lean version and pre-built dependencies (typically Mathlib).

Available environments: `lean-4.28.0`, `lean-4.27.0`, `lean-4.26.0`, etc.

`timeout_seconds` · float · default: `120` · Max execution time in seconds

Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 900 seconds (15 minutes).

## Output Fields

`content` · string · Processed Lean code

The Lean code that was actually processed. May differ from input if `ignore_imports=true` caused header injection.

`lean_messages` · dict · Messages from Lean compiler

Messages from the Lean compiler with `errors`, `warnings`, and `infos` lists. Errors here indicate invalid Lean code (syntax errors, type errors, etc.); an empty `errors` list means the code compiles.

If the tool allows declaration selection and a `names`/`indices` selection is given, elaboration is skipped for the proofs of unselected declarations, so this field reflects only the selected declarations and is otherwise incomplete.

`tool_messages` · dict · Messages from disprove tool

Messages from the disprove tool with `errors`, `warnings`, and `infos` lists. Errors here indicate tool-specific issues (not Lean compilation errors).

`results` · dict · Map from theorem name to disprove result

Each theorem maps to a string indicating the outcome of the disprove attempt.

`negated` · dict · Map from theorem name to negated goal

Each theorem maps to the negated goal type that was attempted (the statement whose proof would disprove the theorem).

`disproved_theorems` · list · List of theorems that were disproved

List of theorems that were disproved

`timings` · dict · Execution timing breakdown

Timing information in milliseconds for various stages of processing.