[scscsc]

To those wondering if there will be a successful "marriage" between popular incarnations of AI, like ChatGPT, and FM: no, at least not in the sense you would expect.

Sure, ChatGPT will successfully manage to find formal proofs that have been done before.

But synthesising proofs from scratch is NP-complete for the simplest proofs (or worse for more interesting cases), and LLMs are simply not clever enough to do it (except in cases where the proof has been seen before).

It could be possible to integrate an SMT solver with a LLM to make this work, but the core difficulty of the FM task will then be solved by the SMT solver.

[trenchgun]

There is ongoing work trying to get that marriage to work