Formal proof systems and LLMs are a match made in heaven
= <Formal proof systems> and <LLMs> are a match made in heaven
On one hand, <formal proof systems> prevent <hallucinations>.
On the other hand, <LLMs> can handle the mega verbosity and learning curve of <formal proof systems> which few humans are willing to undertake.
The human only needs to understand the bare minium of the formal proof system to know that statements are what they say they are. LLMs can then take care of the proof entirely.
It's really a killer combo.