alt Hacker News> would be an issue even if it were humans writing
I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.
From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.
I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect.
For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that works for most realistic cases, e.g. integers -> Int64. Other types become considerably more irritating; you might prove something with regards to all real numbers, but when exporting to a "real" programming language, there really isn't such thing as "real" numbers, since computers can really only do the rationals. You could export to float64, but then you're dealing with IEEE rounding, which may or may not be fine for what you're working on. You could use something like GMP (which is what I ended up doing when I had this issue) but of course you pay a performance penalty by doing that, and of course you're then trusting the correctness of GMP (though there is a verified subset, to be fair).
I feel like with TLA+, I am typically working on higher-level problems. Usually I'm modeling distributed systems, which sort of inherently requires an "opinion" for deployment.
How would I deploy this code? Erlang? Kubernetes? Docker Swarm?
How am I doing service discovery? DNS? YOLOing with raw IP addresses?
Suppose my model has a global function [1] that I'm writing to as a global shared store? Where does this live? Is this a local cache? Is this Redis? Memcached?
I could go on. The whole point of TLA+ is to write and test the algorithms, and very purposefully allows and encourages you to ignore details that aren't necessary to show correctness of your algorithm.
I'm not saying you couldn't do this, to be clear. You could absolutely create an exporter for TLA+, but my point is that it would require a good chunk of opinions and decisions to do it. You'd also need to ensure that the semantics of these things properly map to your model, else the exporter is only of debatable utility.
I think this is why there isn't really a serious exporter for TLA+. You just work at a different level with it, and I think there are just too many (kind of arbitrary) decisions that would have to be made in order to do anything useful.
[1] In TLA+, "function" basically means key-value map.