AlphaProof's Greatest Hits

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking.

For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language? What about "The theoretical basis of the October Revolution lay in a development of Marxism, but this development occurred through three successive rounds of theoretical debate"?

Or have I totally misunderstood what people mean when they say that developments in automatic theorem proving will solve LLM's hallucination problem?