I believe this, but it is also a unique case where the pitfalls of LLMs (producing weird errors that a human wouldn't) are zeroed out. Since you have a proof checker that tells you if the LLM did it right.
I'm pretty convinced most serious software will have some kind of proof system inside within the next few years.
I'm pretty convinced most serious software will have some kind of proof system inside within the next few years.