LEAN4 is both an interactive theorem prover and a programming language. It feels natural to have a LEAN driver for TypeDB.