Lean4 tactics are related to Clojure/Lisp based macros (https://lean-lang.org/theorem_proving_in_lean4/Tactics/)
Lean4 core is a functional programming lang and Zil it's a DSL implemented ontop, that means it would define a set of abstractions lean4 accepts such as theorems and lemmas, im also learning !
initial implementation uses clojure, I used claude to port it to Lean4 for my projects, it helps AI agents specially well because it allows it to keep context about how concepts are related and define rules and have a query system(datalog) to recover. If you try it pls report back ! if doesnt work, just mention how what what was the context, maybe there's a way to improve it for that case too. cheers and happy hacking.