Clojurians Log v2

Announcing Ansatz https://github.com/replikativ/ansatz is a new Clojure library for verified programming based on the Calculus of Inductive Constructions, with a Lean 4-compatible kernel and similar syntactic abstractions. The idea is: write programs and proofs in Clojure s-expressions, type-check them against a CIC kernel implemented in Java, and then run verified functions as ordinary JVM/Clojure code. Ansatz can also work against imported Lean 4 libraries, including Mathlib and CSLib, so in principle you can use a large body of existing formalized mathematics and verified algorithms from Clojure. It uses the same persistent memory model as #datahike which makes the proof state git-like, something that Lean4 cannot do. Current focus: • verified functions, theorems, inductives, structures • tactic-based proofs in Clojure syntax • import/export around Lean 4 / Mathlib • a JVM-native path for building larger systems on top This is the first release, but not a weekend hack. A lot of work already went into getting Mathlib checking/import paths and the core machinery working. I’m exploring this direction seriously because I want to build AI infrastructure on top of it (e.g. #simmis). That said, this is still an early starting point, not stable software. I expect dragons: - tactic implementations still have rough edges - there are probably still gaps in the kernel - the overall workflow and ergonomics need iteration So this is both a release and an invitation: if verified programming from Clojure, Lean interop, or proof-aware AI infrastructure sounds interesting, I’d be glad if people kick the tires, look at the design, and explore where this could go.