Dependently typed Clojure DSL with a Lean4 compatible kernel
Summary
The article presents Ansatz, a dependently typed Clojure DSL that runs with a Lean4 compatible kernel. It describes how the Lean CIC kernel is implemented in Java, how proofs are checked against Mathlib and CSLib, and how verified functions compile to normal JVM-based Clojure. It also covers on-ramp workflows for Clojure developers, including Malli schemas, kernel signatures, and tactic-based proofs, highlighting verified data structures and termination guarantees.