disprove

Attempt to disprove theorems by proving the negation. Requires Mathlib.

Python API

result = await axle.disprove(
    content=lean_code,
    environment="lean-4.26.0",
    names=["conjecture1", "conjecture2"],  # Optional
    ignore_imports=False,                   # Optional
)
print(result.disproved_theorems)  # ["conjecture2"]
print(result.results)  # Per-theorem results
print(result.content)  # The processed Lean code

CLI

Usage: axle disprove CONTENT [OPTIONS]

# Disprove all theorems
axle disprove theorems.lean --environment lean-4.26.0
# Disprove specific theorems by name
axle disprove theorems.lean --names main_theorem,helper --environment lean-4.26.0
# Disprove specific theorems by index
axle disprove theorems.lean --indices 0,-1 --environment lean-4.26.0
# Pipeline usage
cat theorems.lean | axle disprove - --environment lean-4.26.0

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/disprove \
    -d '{"content": "import Mathlib\ntheorem solid_fact : 1 = 1 := rfl\ntheorem bold_claim : 2 = 3 := rfl", "environment": "lean-4.26.0"}' | jq

Input Parameters

Name	Type	Required	Description
content	str	Yes	A string of Lean code
environment	str	Yes	Environment to use (e.g., "lean-4.26.0", "lean-4.25.1")
names	list[str]	No	List of theorem names to disprove
indices	list[int]	No	List of theorem indices (0-based, negative allowed)
terminal_tactics	list[str]	No	Tactics to try when attempting to disprove (default: ["grind"])
ignore_imports	bool	No	If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false
timeout_seconds	float	No	Maximum execution time (default: 120)

Note: Specify only one of names or indices. If neither specified, checks all theorems.

Output Fields

Name	Type	Description
content	str	The Lean code that was actually processed (after header injection if imports were ignored)
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists (may under-report errors in proof bodies)
tool_messages	dict	Messages from disprove tool with errors, warnings, infos lists
results	dict[str, str]	Map from theorem name to disprove result message
disproved_theorems	list[str]	List of theorems that were disproved
timings	dict	Timing info: total_ms, parse_ms

Example Response

{
  "content": "import Mathlib\n\ntheorem solid_fact : 1 = 1 := rfl\ntheorem bold_claim : 2 = 3 := rfl\n",
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "results": {
    "solid_fact": "Disprove: failed to prove negation. Remaining goal: `1 = 1`\n",
    "bold_claim": "Disprove: goal is false! Proof of negation by plausible.\n\n===================\nFound a counter-example!\nissue: 2 = 3 does not hold\n(0 shrinks)\n-------------------\n"
  },
  "disproved_theorems": ["bold_claim"],
  "timings": {
    "total_ms": 97,
    "parse_ms": 92
  }
}