Lean is now the Language of the Month. Yay!
But... Lean is a theorem proving language. It is also a general purpose, Turing complete1 programming language too but I mean... Lean isn't exactly better than other languages on that front wrt code golf.
On the Lean Zulip chat, sometimes users compete to write the shortest proof possible for a given lemma. Could we also do something similar on this Code Golf website?
The main issue with this is that this wouldn't be language agnostic: how the problem statement is formalized, or specified in the theorem proving language can significantly affect the proof.
1 You can turn off the termination checker. There are functions to interact with the operating system.