I am betting though that type theory is not the right logic for this, and that Lean can be leapfrogged.
I am not sure lean in part is the right language, there might be challengers rising (or old incumbents like Agda or Roq can find a boost). But type theory definitely has the most robust formal systems at the moment.
I think it is more important to be close to English than to programming languages, because that is the critical part:
"As close to a programming language as necessary, as close to English as possible"
is the goal, in my opinion, without sacrificing constraints such as simplicity.
The calculus of constructions and other approaches are already available and proven. I'm not sure why we'd need a special logic for LLMs unless said logic somehow accounts for their inherently stochastic tendencies.
