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.