[UltraSane]

This is NOT what Lean 4 is designed to do. You seem to be using Lean 4 for what TLA+ is much better suited for.

[wizzwizz4]

If it is not suitable for programming, then it should not be branded as a programming language. Heck, its homepage says:

> Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.