Nice, but what is the motivation for this? That the syntax is perceived to be nicer than SMT-LIB format? Or that Lean can get involved? Differential testing? Just for fun?