Blaster: Lean 4 Proof Automation

how it works

Lean → Optimizer → SMT → Result

Blaster doesn't call Z3 directly. It first simplifies your goal through ~40 algebraic rewriting passes, then emits a minimal SMT-Lib 2 query.

Lean Goal

x > 0 → (if x > 0 then x + 1 else x - 1) > 0

your theorem

Optimizer

x > 0 → x + 1 > 0

branch eliminated via hypothesis

SMT-Lib 2

(assert (not (=> (< 0 x) (< -1 x))))

minimal query to Z3

Z3

unsat

unsatisfiable → valid

Result

✓ Valid · 4ms

goal closed

examples

What Blaster handles today

higher_order.lean click to run →

#blaster [ ∀ (x : Nat) (xs : List Nat), !xs.isEmpty → (xs.map (Nat.add x)).head! ≥ x]

✓ Valid·higher-order

polymorphism.lean click to run →

#blaster [ (∀ (α) (a b : α) [BEq α], a == b → a = b) → ∀ (x y : Either α β) [BEq α] [BEq β], x == y → x = y]

✓ Valid·polymorphism + typeclass

mutual_inductive.lean click to run →

theorem A_self_size (a : A) : (A.self a).sizeA = a.sizeA + 1 := by blaster

✓ Valid·mutually inductive

counterexample.lean click to run →

-- Blaster finds a witness #blaster [∀ (α : Type) (x : Term α), sizeOfTerm x < 10]

✗ Falsified·counterexample

quant_functions.lean click to run →

#blaster [ (∀ (β) (x : Term (List β)) (f : Term (List β) → Nat), f x > 10) → ∀ (x y : Term (List α)) (f : Term (List α) → Nat), f x + f y > 20]

✓ Valid·quantification over functions

state_machine.lean click to run →

-- invariants hold ∀ states, ∀ depths #kind (max-depth: 1) [counterStateMachine]

✓ Valid·k-induction

getting started

Add Blaster to your project

lakefile.lean

require Blaster from git "https://github.com/input-output-hk/Lean-blaster" @ "main"

usage

import Blaster.Tactic theorem add_comm (a b : Nat) : a + b = b + a := by blaster -- ✓ Valid · 8ms

View on GitHub Documentation

Stop writing proofs.Blast them.

Lean → Optimizer → SMT → Result

What Blaster handles today

Add Blaster to your project

Stop writing proofs.
Blast them.