I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language:

https://link.springer.com/chapter/10.1007/978-3-030-79876-5_...

Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers.

[1] https://leanprover.github.io/functional_programming_in_lean/