You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.

Not saying your niche doesn't have value, but you can get interesting ideas from there.

> In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully.

Why is Windows not open source then, where we can trust Microsoft based on the experience with previous Windows versions?

The trust in open source software is founded on the process which involves people being able to understand the code given they have the right expertise. I don't see how this process works with open weights.