Comment by cubefox
3 days ago
I don't think there is any technical solution for that, apart perhaps from asking an LLM, or multiple different LLMs, whether it thinks the formal definition matches the informal statement.
When mathematicians check normal (informal) proofs they usually verify both things at once: that the proof doesn't contain mistakes or insufficiencies, and that it proves what the author says it proves. Formal proof checkers aren't able to do the latter.
I personally view proof checkers as mathematicians' tools so I assume mathematicians would be involved either way. With some percentage actually preferring to work closely with these tools. See also Terence Tao's comment in https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t... which feels relevant to me
Tao misunderstands the question here: it was about reconciling a traditional (informal) proof and a formal proof which come to opposite conclusions, not about two different formal proofs.
I think he accounts for that in the answer, "in a way that would be faster than if one or both proofs were informal" (which assumes "one formal and one informal" is also a case he's talking about). The way I understand his point is that in either case you would have to go through the two mathematical structures with the same amount of rigour and attention until you find the divergence, and that's easier to do when at least one side is formal (but can be done in either case).
In other words, informal math doesn't make this problem easier because you can still make and miss mistakes in encoding intent into the structure. But at least with formal math, there's whole classes of mistakes that you can't make.