Ansatz

Write Clojure. Prove it correct. Run as ordinary JVM code.

Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4. It implements Lean 4's kernel in Java, type-checks proofs against Mathlib (500k+ theorems, 707k declarations) and CSLib (verified algorithms), and compiles verified functions to ordinary Clojure/JVM code.

If you already write malli-instrumented Clojure, Ansatz is the gradual next step: your m/=> schemas become kernel type signatures, your functions become machine-checked, and they still run as ordinary Clojure.

Same kernel, different surface. Ansatz shares Lean 4's CIC kernel — a proof verified in Ansatz is valid in Lean 4 and vice versa. Proofs can be exported to Lean 4 syntax. The difference is the surface language: Lean 4 uses its own syntax; Ansatz uses Clojure s-expressions and runs on the JVM. See Lean 4 for Clojurians for the full comparison, translation guide, and learning path.

(require '[ansatz.core :as a] '[malli.core :as m])
(a/load-init!)   ;; zero-config: the Lean Init environment bundled in the jar

;; The gradual on-ramp: keep your malli schema, change defn → a/defn.
;; The schema becomes the kernel type; the function is machine-checked and
;; still compiles to an ordinary Clojure fn.
(m/=> add2 [:=> [:cat :int :int] :int])
(a/defn add2 [x y]
  (match x [zero y] [(succ k) (+ 1 (add2 k y))]))
(add2 20 22) ;; => 42

;; [:map …] schemas become named-field records: keyword access is kernel-verified,
;; runtime values stay plain Clojure maps
(m/=> dot [:=> [:cat [:map [:x :int] [:y :int]]] :int])
(a/defn dot [p] (+ (:x p) (:y p)))
(dot {:x 2 :y 3}) ;; => 5

;; refinements: an [:int {:min 1}] param carries its bound as a Prop in the kernel
;; type (a Subtype) — and is still used directly as a number in the body
(m/=> pred [:=> [:cat [:int {:min 1}]] :int])
(a/defn pred [n] (- n 1))

;; the differential check: compiled runtime ≡ kernel evaluation on schema-generated
;; inputs — catches elaboration bugs that are well-typed but unfaithful to the source
(require '[ansatz.malli :as am])
(am/check-verified! 'my.ns 'add2 :runs 25) ;; => {:runs 25 :ok 25}

Beyond schemas, full CIC types — here is verified merge, where the kernel proves termination (a lexicographic sizeOf measure, guessed automatically and embedded in the kernel term):

(a/defn merge [xs :- (List Nat), ys :- (List Nat)] (List Nat)
  (match xs
    [nil ys]
    [(cons x xs')
     (match ys
       [nil (cons x xs')]
       [(cons y ys') (if (<= x y)
                       (cons x (merge xs' (cons y ys')))
                       (cons y (merge (cons x xs') ys')))])]))
;; explicit spellings also work:
;;   :termination-by (+ (sizeOf xs) (sizeOf ys))   or   [(sizeOf xs) (sizeOf ys)]

;; Run it — it's a normal Clojure function
(merge '(1 3 5) '(2 4 6)) ;; => (1 2 3 4 5 6)

;; Structures compile to Clojure defrecord
(a/structure Point [] (x Nat) (y Nat))
(->Point 3 4)  ;; => #user.Point{:x 3, :y 4}
(:x (->Point 3 4))  ;; => 3

Verified data structures — define types, implement with pattern matching, prove properties:

;; Define your own types (like Clojure records, but type-checked)
(a/inductive RBColor [] (red) (black))
(a/inductive RBTree [α Type]
  (leaf)
  (node [color RBColor] [left (RBTree α)] [key α] [right (RBTree α)]))

;; Pattern matching with recursion — the kernel checks termination.
;; The types are inferred: the tree's from `t`, the result's from the signature.
(a/defn rb-size [t :- (RBTree Nat)] Nat
  (match t
    [leaf 0]
    [(node color left key right) (+ 1 (+ (rb-size left) (rb-size right)))]))

;; BST lookup — recursion into a subtree is an ordinary call
(a/defn rb-member [t :- (RBTree Nat), k :- Nat] Bool
  (match t
    [leaf false]
    [(node color left key right)
     (if (< k key)
       (rb-member left k)                 ;; recurse into left subtree
       (if (== k key)
         true                             ;; found it
         (rb-member right k)))]))         ;; recurse into right subtree

;; A verified constant (constructors are ordinary constants in term position)
(a/defn tree [] (RBTree Nat)
  (RBTree.node Nat RBColor.black
    (RBTree.node Nat RBColor.red (RBTree.leaf Nat) 2 (RBTree.leaf Nat))
    4
    (RBTree.node Nat RBColor.red (RBTree.leaf Nat) 6 (RBTree.leaf Nat))))

;; All verified functions compile to ordinary Clojure and run on the JVM
(rb-size tree)           ;; => 3
(rb-member tree 4)       ;; => true
(rb-member tree 42)      ;; => false

Prove properties — from simple definitional equality to automated reasoning:

;; Simplest proof: rb-size(leaf) computes to 0 by definition.
;; (rfl) = "reflexivity" — both sides reduce to the same thing.
(a/theorem leaf-size-zero []
  (= (rb-size (RBTree.leaf Nat)) 0)
  (rfl))

;; (omega) solves linear arithmetic over natural numbers automatically.
;; It sees: goal is (rb-size l) ≤ 1 + (rb-size l) + (rb-size r)
;; and closes it because x ≤ 1 + x + y for all naturals.
(a/theorem left-le-size [c :- RBColor, l :- (RBTree Nat), k :- Nat, r :- (RBTree Nat)]
  (<= (rb-size l) (+ 1 (+ (rb-size l) (rb-size r))))
  (omega))

;; The following proofs use definitions from examples/ (llen, lmap, Sorted,
;; insertSorted, balance1, ValidRB — see verified_list.clj, sorting.clj, rbtree.clj).

;; Induction + grind: the standard pattern for list properties.
;; (induction l) splits into two goals:
;;   1. Base case:  llen (lmap f []) = llen []        — both sides are 0
;;   2. Inductive:  llen (lmap f (x::xs)) = llen (x::xs)
;;      with IH:    llen (lmap f xs) = llen xs
;; (grind "lmap" "llen") tells grind to use the equation theorems
;; for lmap and llen (e.g. llen.eq_2: llen(x::xs) = 1 + llen xs).
;; It unfolds one step, sees 1 + llen(lmap f xs) = 1 + llen xs,
;; and closes via congruence from the IH.
(a/theorem map-preserves-len [f :- (arrow Nat Nat), l :- (List Nat)]
  (= (llen (lmap f l)) (llen l))
  (induction l) (all_goals (grind "lmap" "llen")))

;; Sorted is an indexed inductive: Sorted [] | Sorted [a] | Sorted (a::b::tl) when a≤b.
;; (induction h) on h : Sorted l gives 3 goals (one per constructor).
;; (grind "insertSorted") uses insertSorted's equation theorems to unfold it,
;; case-splits on ≤ comparisons, applies constructors, uses omega
;; for arithmetic, and the IH for the recursive case.
(a/theorem insert-preserves
  [x :- Nat, l :- (List Nat), h :- (Sorted l)]
  (Sorted (insertSorted x l))
  (induction h) (grind "insertSorted"))

;; balance1 has 7 branches (from nested pattern matching on color + subtree shape).
;; (cases hl) splits ValidRB(l) into leaf/node.
;; (simp [balance1]) uses balance1's equation theorems to unfold it for each branch.
;; (grind) then applies ValidRB constructors and matches sub-proofs from context.
;; The middle lines split further on color, subtree shape, and inner color
;; to expose the left-left rotation case (the only one that restructures the tree).
(a/theorem balance1-preserves-valid
  [l :- (RBTree Nat), v :- Nat, r :- (RBTree Nat),
   hl :- (ValidRB l), hr :- (ValidRB r)]
  (ValidRB (balance1 l v r))
  (cases hl)                           ;; leaf or node?
  (all_goals (try (simp [balance1])))  ;; unfold via equation theorems
  (all_goals (try (grind)))            ;; close the easy cases
  (all_goals (try (cases c)))          ;; red or black?
  (all_goals (try (cases l)))          ;; left subtree shape
  (all_goals (try (cases color)))      ;; inner node color (detects LL rotation)
  (all_goals (try (cases hl)))         ;; decompose inner ValidRB proof
  (all_goals (try (simp [balance1])))  ;; unfold the rotation case
  (all_goals (try (grind))))           ;; close all remaining goals

See examples/ for complete working examples:

• verified_list.clj — verified list library (map, filter, append, length) with 10+ proved properties + insertion sort correctness
• sorting.clj — verified merge sort, structures, factorial (CSLib-inspired)
• rbtree.clj — verified red-black tree with balance invariant proof (grind + manual versions)
• gradient_descent.clj — verified GD convergence rate proofs
• metaprogramming.clj — custom tactics, elaborators, simprocs

New to verified programming? Start with the Tutorial — a hands-on guide that teaches you to define functions, write proofs, and use grind, with no prior theorem proving experience needed.

Already know Lean 4? See Lean 4 for Clojurians for the syntax translation guide.

How it works (for Clojure developers)

Ansatz adds these primitives to Clojure:

1. a/defn — like defn, but type-checked. The kernel verifies that your function matches its type signature. Supports well-founded recursion via :termination-by for non-structural patterns (merge sort, factorial). The compiled output is a normal Clojure fn.

2. a/theorem — states a property and proves it using tactics. Tactics are commands that build a proof step by step. The (grind "defn-name") tactic automates most proofs via E-graph congruence closure and case splitting. For manual control: (apply lemma), (induction x), (cases h), (omega), (simp [lemma]). The kernel verifies the final proof term.

3. a/inductive — defines algebraic data types with exhaustive pattern matching. The kernel generates a recursor that ensures termination.

4. a/structure — defines record types that compile to Clojure defrecord. Fields are accessible via keywords: (:x point). Kernel-verified projections are auto-generated.

The key idea: Lean 4's Mathlib library has 210,000+ proved theorems about math (algebra, analysis, topology). Ansatz lets you USE those theorems in your Clojure proofs. When you write (apply mul_le_of_le_one_left), you're applying a theorem that was proved in Mathlib and verified by the kernel. Proofs are portable — Ansatz can export to Lean 4 syntax and Lean 4 proofs can be imported into Ansatz.

Features

• Verified functions — define functions with CIC types, prove properties, run at JVM speed
• Malli schemas as signatures (optional) — the gradual-typing on-ramp: keep your (m/=> f [:=> [:cat :int :int] :int]) declarations and change defn to a/defn; the schema becomes the kernel signature. Collections→List; [:map [:x :int] …]→a synthesized named-field record (keyword access (:x p) elaborates to kernel projections, runtime values stay plain Clojure maps); [:int {:min k}]→Subtype refinements whose params are still usable directly as numbers (references auto-coerce to .val, the refinement stays in the binder for proofs). ansatz.malli/check-verified! adds a generative differential check — schema-generated inputs run through both the compiled runtime and the kernel evaluator and must agree, guarding the well-typed-but-unfaithful elaboration bug class the kernel can't see. malli loads lazily; core has no hard dependency
• Grind tactic — automated reasoning via persistent E-graph with congruence closure, propositional propagators (And/Or/Not/Eq/ite), E-matching for lemma instantiation, constructor injection/discrimination, and theory solver integration
• Kernel-enforced termination — every recursive definition carries its termination proof in the kernel term: structural recursion, :termination-by measures (scalar, lexicographic [m n] — Ackermann verifies, (sizeOf xs) over data structures), automatic measure guessing, and loop/recur; non-terminating definitions are rejected with actionable errors (^:partial is the explicit trusted escape)
• One lean4-shaped elaborator — fvar/metavar elaboration with implicit + universe inference for bodies, signatures, measures, theorem statements, and tactic arguments; Clojure macros (->, when, and/or, yours) expand by default and compose
• Structures — a/structure compiles to defrecord with keyword access and pretty-printing
• Generic types — implicit type parameter inference via auto-elaborate (polymorphic constructors work without explicit type annotations)
• Lean 4 Mathlib + CSLib — 707k Mathlib declarations (all kernel-verified) + CSLib verified algorithms
• Tactic proofs — apply, simp, omega, ring, grind, assumption, induction, cases, and more
• Instance synthesis — automatic typeclass resolution with tabled backtracking
• Compiled output — verified defn compiles to ordinary Clojure fn with arity-aware flat calls
• Extensible — register-elaborator! is lean4 macro_rules-shaped (your fn maps argument forms to a replacement surface form, the elaborator does the rest); plus custom tactics and simprocs with full kernel access
• Immutable proof state — free backtracking via Clojure persistent data structures

Quick Start

Prerequisites

• Java 21+ (for Foreign Function API / memory mapping)
• Clojure CLI 1.12+

That is all: the Mathlib store is downloaded on first use. Lean 4 (elan) is needed only to build a store yourself — a version we have not published, or a library of your own.

Installation

Add to deps.edn:

{:deps {org.replikativ/ansatz {:mvn/version "0.2.112"}}}  ; latest release: see the Clojars badge

Startup time

Ansatz's own namespaces are AOT-compiled into the published jar (filtered to ansatz.*, so no dependency classes ship), which is why (require 'ansatz.core) is ~1 s rather than ~8 s. The zero-config tier is then ready in about 3 s from a cold JVM.

A store-backed session costs more, and almost all of it is konserve and datahike compiling from source at every start — not ansatz, and not the store. If that matters, build an application uberjar, which AOT-compiles the whole stack:

clj -T:build uber          # target/ansatz-standalone.jar

Measured on one machine, warm page cache, full Mathlib store:

	library jar	uberjar (50 MB)
(require 'ansatz.core)	1.2–1.4 s	0.8 s
(init! "mathlib")	14.0–15.1 s	3.8–3.9 s
first catalogue recall (loads datahike)	28.9–29.6 s	5.1–6.2 s
total first session	47.4–49.1 s	12.5–13.5 s

Compiling dependencies is safe in an application — it pins its own versions, so nothing can shadow what another project resolved — and is deliberately not done in the library jar. Everything after startup is warm: a repeat theorem lookup is ~3 µs, simp 50–100 ms, a recall query ~1 ms.

Mathlib, without building it

Ansatz needs a store of Lean 4 Mathlib declarations. You do not have to build one:

(require '[ansatz.core :as a])
(a/init! "mathlib")   ;; downloads the published store once (~1.3 GiB), then starts

The store a build can read is published per import — mathlib-v4.33.1-f1, the library tag and the store format — as a release of replikativ/ansatz-stores. init! looks the name up in that repository's index, downloads the parts (resuming if interrupted), checks each against its SHA-256 and installs the store under the durable store root ($ANSATZ_STORE_DIR → $XDG_DATA_HOME/ansatz/stores → ~/.local/share/ansatz/stores). It unpacks to about 5 GB and is used from then on; nothing is downloaded again. Because the index is read at fetch time, a new import reaches you without a new ansatz release.

variable	effect
ANSATZ_STORE_DIR	where stores live
ANSATZ_OFFLINE=1	never download; a missing store is an error
ANSATZ_STORE_INDEX	another index (a path or a URL)
ANSATZ_STORE_BASE	another artifact host (a mirror)

Or build the store yourself — for a Mathlib version that is not published, a private library, or to be independent of us:

Automated setup

# Requires: Lean 4 (elan), Java 21+, Clojure CLI
./scripts/setup-mathlib.sh

This clones lean4export and mathlib4 (if not present), exports Mathlib to NDJSON with mdata preserved, dumps the instance registry and the @[simp]/@[csimp]/@[extern] attributes from the same toolchain, and runs the importer (ansatz.import), which produces a complete store in one pass — the declaration trees, the attributes, the instance index, the matcher corpus, the recall keys, the @[simp] index and the catalogue — under the durable store root ($ANSATZ_STORE_DIR → $XDG_DATA_HOME/ansatz/stores → ~/.local/share/ansatz/stores; pass an explicit directory as the first argument to override). The export takes ~5 minutes, the import about half an hour on 8 cores (the keying passes use every core). Avoid /tmp//var/tmp for stores — systemd-tmpfiles erodes them.

A store is versioned by its manifest.edn (:store/format, provenance — Lean toolchain, library and lean4export revisions — and an inventory of what it holds). init! refuses a store of another format and says so; there is no migration step, ever: re-run the setup script. Node blobs are content-addressed, so re-importing the same export yields the same store.

To re-check an imported store through the kernel:

clj -M -e '
(require (quote [ansatz.export.storage :as s]))
(let [store (s/open-store ((requiring-resolve (quote ansatz.store/resolve-existing)) "mathlib"))]
  (try
    (prn (s/verify-from-store! store "mathlib"
                               :verbose? true
                               :timeout-ms 300000))
    (finally
      (s/close-store store))))
'

The authoritative full-corpus check uses the PSS-backed store. The imported-store verifier uses a higher fuel default than interactive tactic calls because full Mathlib contains legitimate declarations above 20M kernel steps. For trace-level comparison against a patched Lean 4 build, see doc/kernel-validation.md.

Manual setup

If you prefer step-by-step:

# 1. Clone and build lean4export (https://github.com/leanprover/lean4export)
git clone https://github.com/leanprover/lean4export.git ../lean4export
cd ../lean4export && lake build

# 2. Export Mathlib to NDJSON (~5 min, ~5GB)
# Preserve mdata so imported declarations stay closer to Lean kernel trace space.
cd ../mathlib4
lake env ../lean4export/.lake/build/bin/lean4export --export-mdata Mathlib > ../ansatz/test-data/mathlib.ndjson

# 3. Dump Lean's @[instance] registry (~2 min) — module order and real priorities, both
#    load-bearing for synthesis (see scripts/dump_instances.lean)
lake env lean --run ../ansatz/scripts/dump_instances.lean Mathlib > ../ansatz/test-data/mathlib-instances.tsv

# 4. Dump the attributes (co-generated with the export)
lake env lean --run ../ansatz/scripts/dump_attrs.lean Mathlib | gzip -c > ../ansatz/test-data/mathlib-attrs.ndjson.gz

# 5. Import — one command, complete store (~30 min on 8 cores; keying runs on every core)
cd ../ansatz
clj -J-Xmx8g -M:datahike -m ansatz.import "$(clj -M -e '(print ((requiring-resolve (quote ansatz.store/store-dir)) "mathlib"))')" \
    test-data/mathlib.ndjson mathlib test-data/mathlib-attrs.ndjson.gz test-data/mathlib-instances.tsv \
    "lean/toolchain=$(cat ../mathlib4/lean-toolchain)" "library/rev=$(git -C ../mathlib4 rev-parse HEAD)"

Setup CSLib Store (Verified Algorithms)

CSLib is the official Computer Science library for Lean 4 — verified sorting, automata, lambda calculus, and more.

./scripts/setup-cslib.sh

This imports CSLib (including its Mathlib dependency) into a store named cslib under the durable store root (see above).

Using init-medium for quick testing (no Lean needed)

The test data test-data/init-medium.ndjson (10MB, 2997 declarations) is included in the repo and sufficient for basic proofs on Nat. No Mathlib setup required:

;; Works out of the box for Nat proofs (no Real/analysis)
(require '[ansatz.export.storage :as s] '[ansatz.export.replay :as r]
         '[ansatz.export.parser :as p])
(def env (:env (r/replay (:decls (p/parse-ndjson-file "test-data/init-medium.ndjson")))))

Initialize and Prove

(require '[ansatz.core :as a])

;; Load the Mathlib environment by store name — resolved from the durable store root,
;; downloaded once when it is not there (see "Mathlib, without building it").
;; (An explicit path still works: (a/init! "/path/to/store" "mathlib").)
(a/init! "mathlib")

;; Define and prove
(a/defn ^Nat double [^Nat n] (+ n n))

(a/theorem add-zero [n :- Nat]
  (= (+ n 0) n)
  (simp [Nat.add_zero]))

(double 21) ;; => 42

Syntax Reference

Types

Nat                          ;; natural numbers
Int                          ;; integers
Real                         ;; real numbers
Bool                         ;; booleans
Prop                         ;; propositions
Type                         ;; types
(List Nat)                   ;; lists

Operators

Arithmetic is type-directed, the way Lean's binop%/OfNat elaboration is: the operator takes the type of its operands and a bare numeral takes the type its position expects. You do not spell the carrier out, and Nat, Int and Real all work the same way.

(+ a b) (- a b) (* a b)      ;; at the operands' type — Nat, Int, Real, any carrier
(+ x 1)                      ;; the numeral takes x's type (Lean's OfNat)
(pow x n)                    ;; x^n at x's type; the exponent is a Nat (Lean's x ^ n)
(quot a b) (rem a b)         ;; integer division and remainder (NOT `/` — see below)

Comparisons follow Lean's binrel%. In a theorem statement, a hypothesis type, or any other place where a proposition is expected, (<= a b) is the proposition a ≤ b at the operands' type; in code it is the decidable Bool comparison:

(a/theorem kappa-nonneg [η :- Real, L :- Real, hη :- (<= 0 η), hb :- (<= (* η L) 1)]
  (<= 0 (- 1 (* η L)))                          ;; propositions over Real, no type written
  (apply sub_nonneg_of_le) (assumption))

(a/defn small? [n :- Nat] Bool (< n 3))         ;; a Bool comparison in code
(= a b) (< a b) (<= a b) (> a b) (>= a b)       ;; Prop in statements, Bool in code

Give the type explicitly only when no operand carries it — all numerals, as Lean's (0 : ℝ) ≤ 1 does:

(<= Real 0 1)                ;; ≤ at Real (Prop); also (le Real a b), (= Real a b)
(add Real a b) (mul Real a b) (sub Real a b) (pow Real k n)
(div Real a b)               ;; division (there is no `/` operator: Clojure's `/` on integers
                             ;;   is Ratio division, which is not what `Nat.div` means)

Definitions

;; Binder syntax: ONE grammar, three spellings. parse-params reads the vector as
;; name/type pairs; `:-` separators are optional sugar over the pairs; metadata
;; types are the third skin and keep the vector a plain Clojure binding vector
;; (this is what the malli on-ramp generates). Pick one and stay consistent —
;; this README uses the `:-` spelling with the return type after the vector.
(a/defn add [x :- Nat, y :- Nat] Nat body)   ;; recommended (matches a/theorem binders)
(a/defn add [x Nat, y Nat] Nat body)         ;; bare pairs — same grammar, no separators
(a/defn ^Nat add [^Nat x ^Nat y] body)       ;; metadata types, return type on the name

;; Well-founded recursion — the decrease proof is kernel-checked, not trusted
(a/defn ^Nat fact [^Nat n]
  :termination-by n
  (if (== n 0) 1 (* n (fact (- n 1)))))

;; Lexicographic measures (vector) — Ackermann verifies; the measure is also auto-guessed
(a/defn ^Nat ack [^Nat m ^Nat n]
  :termination-by [m n]
  (match m
    [zero (+ n 1)]
    [(succ k) (match n [zero (ack k 1)] [(succ j) (ack k (ack (Nat.succ k) j))])]))

;; Recursion over data structures — sizeOf measures (auto-guessed for List/custom inductives)
(a/defn ^Nat pairs [^{:- (List Nat)} xs]                ; recurses on rest-of-rest
  (match xs [nil 0] [(cons h t) (match t [nil 0] [(cons h2 t2) (+ 1 (pairs t2))])]))

;; Malli schemas as signatures (optional dep): defn → a/defn, schema unchanged
(m/=> add2 [:=> [:cat :int :int] :int])
(a/defn add2 [x y]
  (match x [zero y] [(succ k) (+ 1 (add2 k y))]))
;; [:map …] schemas become named-field records: keyword access verifies, runtime = plain maps
(m/=> dot [:=> [:cat [:map [:x :int] [:y :int]]] :int])
(a/defn dot [p] (+ (:x p) (:y p)))                       ; (dot {:x 2 :y 3}) => 5
;; refined params are used directly as their carrier ([:int {:min 1}] → Subtype, auto-.val)
;; differential check: compiled runtime ≡ kernel evaluation on generated inputs
(ansatz.malli/check-verified! 'my.ns 'add2 :runs 25)     ; => {:runs 25 :ok 25}

;; loop/recur — hoisted to a verified helper, termination auto-proved
(a/defn ^Nat sum-to [^Nat n]
  (loop [acc 0 i n] (if (== i 0) acc (recur (+ acc i) (- i 1)))))

;; Typeclass params
(a/defn ^{:- (List α)} sort [^{:- Type} α ^:inst ^{:- (Ord α)} inst ^{:- (List α)} xs] ...)

;; Theorem
(a/theorem name [param :- Type, hyp :- (<= 0 x), ...]
  proposition
  (tactic1 arg1 arg2)
  (tactic2)
  ...)

;; Structure (compiles to defrecord)
(a/structure Point [] (x Nat) (y Nat))
;; Creates: (->Point 3 4) => #user.Point{:x 3, :y 4}
;; Access: (:x p), (:y p)

;; Inductive type
(a/inductive Color [] (red) (green) (blue))
(a/inductive MyList [α Type] (nil) (cons [head α] [tail (MyList α)]))

;; Indexed inductive family (length-indexed vector)
(a/inductive Vec [α Type] :indices [n Nat]
  (nil :where [0])
  (cons [a α] [m Nat] [tail (Vec α m)] :where [(+ m 1)]))

Pattern Matching

;; Match on inductive types — uses CIC recursor under the hood. As in Lean, the
;; inductive type comes from the scrutinee and the result type from the context.
(match expr
  [ctor1 body1]                          ;; constructor without fields
  [(ctor2 field1 field2 ...) body2])     ;; constructor with field bindings

;; Recursion is an ordinary call on a field; the kernel checks it is structural
;; (or finds a terminating measure)
(a/defn size [t :- (MyList Nat)] Nat
  (match t
    [nil 0]
    [(cons head tail) (+ 1 (size tail))]))

;; The explicit form, with both types spelled out and induction hypotheses
;; named after the recursive fields (ih_tail), is still accepted:
;;   (match t (MyList Nat) Nat (nil 0) (cons [head tail] (+ 1 ih_tail)))

Tactics

Tactic	Description
(apply lemma_name)	Apply a lemma, generating subgoals for arguments
(assumption)	Close goal from local context
(simp [lemma1 lemma2])	Simplify using rewrite lemmas
(rfl)	Close a = a goals
(intro) / (intros x y)	Introduce forall binders
(induction n)	Structural induction
(cases h)	Case analysis
(omega)	Linear arithmetic on Nat/Int
(ring)	Polynomial identity
(linarith)	Linear arithmetic over ordered fields
(norm_num)	Numeric normalization
(positivity)	Prove 0 ≤ expr goals
(gcongr)	Generalized congruence
(solve_by_elim)	Backward chaining from context
(constructor)	Apply the goal's constructor
(exfalso)	Prove by contradiction (change goal to False)
(left) / (right)	Choose disjunction branch
(have name type)	Introduce intermediate lemma
(rewrite h)	Rewrite goal using hypothesis
(try (tactic))	Try tactic, ignore failure
(all_goals (tactic))	Apply to all open goals
(first (tac1) (tac2))	Try tactics in order

Configuration

All limits are configurable via dynamic vars in ansatz.config:

(require '[ansatz.config :as config])

;; Increase fuel for complex proofs
(binding [config/*high-fuel* 100000000]
  (a/theorem ...))

;; Enable grind debugging
(binding [config/*grind-debug* true]
  (a/theorem ... (grind)))

;; Register custom simplification procedure
(binding [config/*simprocs* [(fn [st expr] ...)]]
  (a/theorem ... (simp)))

Var	Default	Description
*default-fuel*	20M	Interactive tactic/typechecker fuel per operation
*high-fuel*	50M	Fuel for deep instance chains
*max-whnf-depth*	512	Maximum WHNF reduction depth
*max-synth-depth*	16	Instance synthesis recursion depth
*max-candidates*	32	Instance candidates tried per class
*max-simp-steps*	100k	Maximum simp rewrite steps
*verbose*	true	Print proof/definition results
*grind-debug*	false	Log grind tactic exceptions
*simprocs*	[]	User-registered simplification procedures

Extending Ansatz

Ansatz provides three extension points, following Lean 4's metaprogramming model. Extensions have full access to the CIC kernel (tc/infer-type, tc/cached-whnf, tc/is-def-eq) and proof state.

Custom Tactics (Lean 4's @[tactic])

;; Register a tactic that tries rfl, then assumption, then omega
(a/register-tactic! 'auto
  (fn [ps args]
    (or (try (basic/rfl ps) (catch Exception _ nil))
        (try (basic/assumption ps) (catch Exception _ nil))
        (try (omega/omega ps) (catch Exception _ nil)))))

;; Use it in proofs:
(a/theorem foo [n :- Nat] (<= 0 n) (auto))

Custom Elaboration Forms (Lean 4's elab_rules)

;; lean4 macro_rules-shaped: the registered fn maps the argument FORMS to a
;; replacement surface form; the elaborator then elaborates the result — so
;; extensions compose with every other surface feature (types, matches, macros).
(a/register-elaborator! 'double
  (fn [args] (list '+ (first args) (first args))))

;; Use in definitions:
(a/defn ^Nat f [^Nat n] (double n))   ;; (f 5) => 10

Custom Simprocs (Lean 4's @[simproc])

;; Register a simplification procedure (always active during simp)
(a/register-simproc! 'my-domain/simplify
  (fn [st expr]
    ;; Return {:expr simplified :proof eq-proof} or nil
    nil))

See examples/metaprogramming.clj for working examples.

Development

# Compile Java kernel (required after changing .java files)
clj -T:build javac

# Run tests
clj -M:test

# Check formatting
clj -M:format

# Fix formatting
clj -M:ffix

# Lint
clj -M:lint

# Start REPL
clj -M:repl

See CLAUDE.md for detailed developer workflow, REPL navigation, tracing, and verification commands.

Architecture

Lean 4 Mathlib + CSLib  →  lean4export  →  Ansatz PSS store
                                                  ↓
                                          ansatz.core/init!
                                                  ↓
                                          Env (immutable, on-demand loading)
                                                  ↓
                    ┌────────────┬────────────────┴────────────────┐
                    ↓            ↓                                 ↓
             a/defn        a/structure                      a/theorem
             (+ :termination-by)  (→ defrecord)            (prove with tactics)
                    ↓            ↓                                 ↓
             Native JVM fn  Clojure record             Java TypeChecker verifies

Kernel (Java)

The CIC kernel is implemented in Java for performance:

• TypeChecker — type inference and definitional equality
• Reducer — WHNF reduction (beta, delta, iota, zeta, projection)
• InductiveBundleChecker — Lean-shaped bundled inductive admission, including nested-inductive lowering/restoration
• RecursorGenerator — Lean-shaped recursor type and iota-rule generation for imported and frontend-authored inductive bundles
• Env — immutable declaration environment with staged external lookup for imported-store verification

For a deeper architectural walkthrough of the kernel, see doc/kernel.md.

Tactic Layer (Clojure)

Tactics are pure functions (proof-state → proof-state) on immutable Clojure maps. Backtracking is free via persistent data structures (no save/restore needed).

• basic.clj — apply, intro, assumption, cases, induction, rewrite
• simp.clj — simplification by rewriting (Lean 4's simp architecture)
• omega.clj — linear arithmetic for Nat/Int (ground + non-ground goals)
• instance.clj — typeclass synthesis with tabled resolution
• extract.clj — proof term extraction and verification

Surface Layer (Clojure)

• core.clj — public API (defn, theorem, inductive, init!)
• config.clj — centralized configuration (fuel, depth, limits)
• S-expression compiler translates Clojure forms to CIC kernel expressions

Building from Source

git clone https://github.com/replikativ/ansatz.git
cd ansatz

# Compile Java kernel
clj -T:build javac

# Run tests (requires test-data/init-medium.ndjson)
clj -M:test

# Start REPL
clj -M:repl

Lean 4 Attribution

Ansatz implements the Calculus of Inductive Constructions following Lean 4 (Apache 2.0). The kernel type checker, reducer, and tactic infrastructure are independent implementations in Java/Clojure, informed by Lean 4's algorithms but without copying source code. Mathlib and CSLib declarations are imported via lean4export. CSLib (Apache 2.0) provides the verified algorithms library.

License

Apache License 2.0 — same as Lean 4. See LICENSE.

Copyright 2026 Christian Weilbach