# lean-clj: call Lean 4 functions from Clojure, and prove Clojure functions in Lean Date: 2026-11-05 URL: https://s.conao3.com/blog/2026/311be4 Author: conao3 (Naoya Yamashita) I wrote lean-clj, a library that lets you call functions written and proved in Lean 4 from Clojure, and prove properties of Clojure functions in Lean. The repository is [conao3/lean-clj](https://github.com/conao3/lean-clj), under Apache-2.0. You can get it from Clojars as `io.github.conao3/lean-clj`, and this post uses version 0.3.0. lean-clj compiles the intermediate representation (IR) of the Lean compiler to Clojure source. The JVM runs the same program that Lean's C backend builds, with types and proofs erased. [conao3/lean-clj](https://github.com/conao3/lean-clj): Lean 4 IR to Clojure backend and Lean embedded in Clojure via S-expressions # Three ways to use it lean-clj supports three uses. ![img](https://s.conao3.com/img/311be4-uses.svg) 1. Write functions and theorems in Lean inside a Clojure file, and call the functions from Clojure (`deflean`). 2. Compile an existing Lean project (a lake project) to a set of Clojure namespaces (the CLI). 3. Translate a function written in Clojure into a Lean model, and prove its properties in Lean (`lean-clj.typed`). The first two go from Lean to Clojure, and the third goes from Clojure to Lean. Each section below gives an example, in the same order. # Write in Lean, call from Clojure Add lean-clj to `deps.edn`: ```clojure {:deps {io.github.conao3/lean-clj {:mvn/version "0.3.0"}}} ``` To expand a `deflean` block for the first time, you need Lean 4.35.0 (`lean` and `lake`) and the `lean-clj` CLI on your `PATH`. Install the CLI with nix: ```console $ nix profile install github:conao3/lean-clj/v0.3.0 ``` Inside `deflean`, you write Lean syntax as S-expressions: ```clojure (ns demo.core (:refer-clojure :exclude [double]) (:require [lean-clj.core :refer [deflean]])) (deflean arith (def double [n Nat] Nat (+ n n)) (theorem double_eq [n Nat] (= (double n) (* 2 n)) (by (unfold double) omega)) (structure Account [owner String balance Nat]) (def deposit [a Account n Nat] Account (with a {:balance (+ (.balance a) n)}))) ``` `def` defines a function, `theorem` states a theorem, and `(by ...)` holds its proof. The proof of `double_eq` unfolds `double` and then closes the goal with `omega`, the tactic for linear arithmetic over natural numbers and integers. When the namespace loads, lean-clj turns the block into Lean source, runs `lake build`, and checks the proofs. If the check passes, lean-clj defines the functions of the block as Clojure functions in the namespace. You pass and receive a structure as a map with keyword keys. ```clojure (double 21) ;=> 42 (deposit {:owner "ann" :balance 10} 5) ;=> {:owner "ann", :balance 15} ``` If a proof fails, the namespace does not compile. Change the theorem to `(* 3 n)`, and you get this error: ```text Syntax error macroexpanding deflean at (demo/wrong.clj:5:1). lean-clj: Lean rejected deflean arith error: demo/wrong.clj:9: deflean arith:3:75: omega could not prove the goal: a possible counterexample may satisfy the constraints a ≥ 1 where a := ↑n Lean source of the block: 1 | def double (n : Nat) : Nat := (n + n) 2 | 3 | theorem double_eq (n : Nat) : ((double n) = (3 * n)) := (by unfold double; omega) ``` The error gives the Clojure file and line (`demo/wrong.clj:9`) and shows the Lean source that lean-clj generated from the block. For syntax that the S-expressions do not cover, you can pass Lean source as a string with `(lean "...")`. The [word-count](https://github.com/conao3/lean-clj/tree/master/samples/word-count) sample uses it to write a function in `do` notation. lean-clj stores the generated Clojure code in `.lean-clj/cache/`. As long as the block does not change, later expansions read the cache and skip Lean. If you commit the cache, the code runs on machines without Lean. # Compile a Lean project to Clojure namespaces The CLI compiles the Lean code of a lake project to Clojure namespaces. The [roman-numerals](https://github.com/conao3/lean-clj/tree/master/samples/roman-numerals) sample converts numbers to and from Roman numerals in Lean, and proves that converting a number from 1 to 999 and back returns the same number. ```lean def toRoman (n : Nat) : String := toRomanAux (n + 13) numerals n def fromRoman (s : String) : Option Nat := if s.isEmpty then none else fromRomanAux s.toList theorem roundtrip : ∀ n, n < 1000 → fromRoman (toRoman n) = if n = 0 then none else some n := by decide +kernel ``` After `lake build` checks the proofs, the CLI compiles the module to a namespace: ```console $ lean-clj module generate-namespace --module-name Roman --namespace roman.core \ --search-path lean/.lake/build/lib/lean --output-file src/roman/core.clj ``` The CLI turns each public function into a Clojure function with a kebab-case name. An `Option` turns into the wrapped value or `nil`. ```clojure (require '[roman.core :as roman]) (roman/to-roman 1994) ;=> "MCMXCIV" (roman/from-roman "MMXXVI") ;=> 2026 (roman/from-roman "hello") ;=> nil ``` The generated `src/roman/core.clj` is an ordinary Clojure file. If you commit it, the code that uses it runs without Lean. `lean-clj project generate` compiles all the modules of a project at once. # Write in Clojure, prove in Lean In the third use, you write the implementation in Clojure. The next example takes a Clojure function that computes the sum from 0 to n in closed form, and proves that it equals a Lean specification that follows the recursive definition of the sum. ```clojure (ns demo.sum (:require [lean-clj.core :refer [deflean]] [lean-clj.typed :as lt])) (lt/defn sum-to-fast [n Nat] Nat (quot (* n (inc n)) 2)) (deflean sums (clojure sum-to-fast) (def sum-to [n Nat] Nat (match n 0 0 (+ k 1) (+ (sum-to k) (+ k 1)))) (theorem two-sum-to [n Nat] (= (* 2 (sum-to n)) (* n (+ n 1))) (by (on-all (induction n) (simp only [sum-to Nat.mul_add Nat.add_mul] at *) omega))) (theorem sum-to-fast-eq [n Nat] (= (sum-to-fast n) (sum-to n)) (by (simp only [sum-to-fast Clj.quot_nat Clj.mul_nat Clj.inc_nat]) "have := twoSumTo n" omega)) (theorem ^{:attrs [csimp]} sum-to-eq [] (= (the (-> Nat Nat) sum-to) sum-to-fast) (by (funext n) (exact (.symm (sum-to-fast-eq n)))))) ``` `lt/defn` defines an ordinary Clojure function and records the Lean types of its parameters and result on the var. Inside the block, `(clojure sum-to-fast)` translates the function into a Lean definition, which this post calls the function's model. `Clj`, a Lean library that ships with lean-clj, provides models of `clojure.core` functions such as `quot` and `inc`. The `@[csimp]` attribute on `sum-to-eq` lets Lean replace `sum-to` with `sum-to-fast` when it compiles a call. Lean permits the replacement because you proved that the two are equal. As a result, a call of `sum-to` from Clojure runs the Clojure `sum-to-fast` instead of the recursion. ```clojure (sum-to 1000000) ;=> 500000500000 ``` lean-ritsuryo, which I introduced in [a post in Japanese](https://s.conao3.com/blog/2026/5499a8), relates implementations to specifications in several ways, and lean-clj applies the same ways to implementations in Clojure. Each relation has a sample:
How the implementation relates to the specification How to write it in lean-clj Sample
The specification runs as it is Call the deflean definition todo-cli
A faster implementation equals the specification on every input Prove the equality, and replace with @[csimp] verified-clojure (sum-to)
A faster implementation equals it under an assumption Prove it under the assumption; callers that meet it call the implementation sorted-search
The implementation satisfies a property of its result State the property as a theorem and prove it verified-clojure (insertion sort), inventory
## Compare the function with its model on generated inputs Lean proves theorems about the model. If the model departs from what Clojure does, you can still prove a theorem that the real function breaks. `lt/check` calls the real function and its model on the same inputs and compares the results: ```clojure (lt/check #'sum-to-fast {:seed 1}) ;=> {:result true, :pass? true, :num-tests 100, :time-elapsed-ms 7, :seed 1} ``` `lt/check` builds test.check generators from the types of the signature. If the results differ, it returns the arguments and both values in `:counterexample`. `lt/defcheck` defines the same check as a `clojure.test` test. lean-clj's own tests compare the `Clj` models with the `clojure.core` functions the same way, in a table of 156 rows. A theorem holds for the calls where the Clojure function returns a value. Calls that throw, such as a `Long` overflow, a division by zero, or an index out of range, fall outside what the models describe. # Model errors that generated tests found The comparison tests found several errors in the models. Some of them let Lean prove theorems that do not hold. ## Truthiness in polymorphic functions This `member?` checks whether `x` is in a list of elements of any type `α`: ```clojure (lt/defn member? [(implicit α Type) (inst (BEq α)) x α xs (List α)] Bool (if-let [y (first xs)] (or (= x y) (member? x (rest xs))) false)) ``` Clojure's `if-let` takes the else branch when the bound value is `false` or `nil`. So on a list of `false`, the function returns `false`: ```clojure (member? 1 [1]) ;=> true (member? false [false]) ;=> false ``` The models treated every value of a type variable `α` as truthy. Values of `Nat` and `String` are always truthy in Clojure, so this is right for most types. At `α = Bool`, though, `false` is falsy, so the model and the Clojure function give different results. With that model, you could prove the next theorem, "if `x` is the head, `member?` returns `true`", for every `α`: ```clojure (theorem member-head [(implicit α Type) (inst (BEq α)) (inst (LawfulBEq α)) (inst (Clj.Truthy α)) x α xs (List α)] (= (member? x (cons x xs)) true) (by (rw [member?]) simp)) ``` At `x = false`, the Clojure function returns `false`, so the theorem does not hold for the real function. Each type variable of a polymorphic model now comes with a `[Clj.Truthy α]` instance argument, so a test of an `α` value behaves as it does at the caller's type. The same proof now stops, because it has to show that `x` is truthy: ```text error: demo/member.clj:15: deflean proofs:3:128: unsolved goals ... x : α xs : List α ⊢ Clj.truthy x = true ``` The [generic-search](https://github.com/conao3/lean-clj/tree/master/samples/generic-search) sample writes `member?` with `if-some`, which treats only `nil` as false, and proves the same theorem. ## Other errors The generated tests also found models that disagreed with these three behaviors of Clojure: ```clojure (:k {:k nil} 0) ;=> nil (str [12345678901234567890N]) ;=> "[12345678901234567890N]" (get [0 1] 4294967297) ;=> 1 ``` - `(:k m default)` returns `nil` when the key is there with the value `nil`. The default applies only when the key is missing. The model returned the default for `nil` too. - `str` adds an `N` to a `BigInt` inside a vector. The model did not. The tests found this because the generators also produce integers beyond `Long`. - `get` on a vector truncates the index to the low 32 bits of an `int`. `4294967297` is `2^32 + 1`, so the call returns the element at index 1. Each model now follows what Clojure does. # What lean-clj does not do lean-clj has no mode (`^:total`) that also proves that a function never throws, including on `Long` overflow. Such a mode would have to rewrite every expression as a computation in a type that represents failure, such as `Option`. If you write that with Lean's `do` notation, the order of evaluation differs from Clojure's: ```lean def half (n : Nat) : Option Nat := if n % 2 == 0 then some (n / 2) else none def g (n : Nat) : Option Bool := do pure (n == 1 || (← half n) == 0) #eval g 1 -- none ``` Clojure's `(or (= n 1) ...)` returns `true` without evaluating the right side when `n` is 1. Lean lifts `(← half n)` out of the expression and runs it first, so `half 1` fails and `g 1` is `none`. The translation would have to rewrite each expression that skips evaluation, like `and` and `or`, to keep Clojure's order, and I decided it was not worth that cost. To avoid overflow, use the arbitrary-precision `+'` family. To find it, pass `:throws :fail` to `lt/check`, which then counts an input that throws as a failure. # How it works lean-clj emits Clojure source, not Java source or JVM bytecode. lean-clj maps Lean's `Array` to Clojure's persistent vector, where updating an element takes O(log n). `Nat` arithmetic moves to `BigInt` through `+'`, and Lean closures become Clojure values that implement `IFn`. The JIT optimizes the bytecode anyway, so emitting bytecode directly would gain little speed. At run time, only the JVM runs. Lean runs only when a `deflean` block expands or when the CLI compiles a module, and a Clojure reimplementation of Lean's runtime functions replaces the C runtime. No Lean process, FFI, or second heap takes part, so there is no state for two runtimes to share. The values that cross between Clojure and the generated code are immutable, and Lean's mutable state runs on Clojure's own: `IO.Ref` is an atom, `Task` a future, `Thunk` a delay, and the standard output `*out*`, which `binding` redirects. A differential test against Lean's C backend checks the generated Clojure. The test runs the same functions as an executable that the C backend builds and as generated Clojure, and compares 182 lines of output. This test found that C prints an infinite float as `inf` and Java as `Infinity`. The backend also ran into the JVM limit of 64 KB per method. It expanded each join point of Lean's IR (a merge point inside a function) at every jump to it. The generated code grew to 36,000 lines, and loading the functions of `Std.Format` failed with "Method code too large!". Now it expands only the join points with one jump, and turns the others into `letfn`. Self tail calls become `loop` and `recur`, and mutual recursion runs through `trampoline`, so neither grows the stack. # Clojure's type and schema libraries Clojure has schema libraries that check values at run time, such as clojure.spec, malli, and Plumatic Schema. They describe values with predicates: they have no type variables, their maps are open by default, and their integers do not tell fixed precision from arbitrary precision. Typed Clojure and clj-kondo's type checking each have their own type language and their own annotations of `clojure.core`. In lean-clj, you write types in Lean, and lean-clj derives malli schemas, test.check generators, and clj-kondo types from them. For the structure `Account` in the `deflean` block above, it derives this schema: ```clojure (require '[lean-clj.types :as t]) (t/malli-schema 'Account) ;=> [:map {:closed true} [:owner :string] [:balance [:and integer? [:>= 0]]]] ``` `Nat` becomes a non-negative integer, and a structure becomes a closed map with the same keys. You get these from the signatures alone, without writing proofs (the [typed-schemas](https://github.com/conao3/lean-clj/tree/master/samples/typed-schemas) sample). A related project is whilo's [ansatz](https://github.com/replikativ/ansatz). ansatz implements Lean's kernel in Java and completes type checking on the JVM. lean-clj checks with the real Lean, and uses Lean's syntax, its standard library, and existing lake projects as they are. In exchange, you need the Lean toolchain the first time you expand a `deflean` block. # Wrapping up lean-clj is on Clojars as `io.github.conao3/lean-clj`. The [samples](https://github.com/conao3/lean-clj/tree/master/samples) directory holds a small program for each use. Start with todo-cli for `deflean`, and with verified-clojure for verifying Clojure functions. I welcome issues and pull requests.