Hacker News Reader

When do you think we’ll have something that can do “verify this proof of the ABC conjecture” and it would check the proof?

If the proof is written in a formal language, we have that now! Even several directly competing efforts (for better and worse).

Some people greatly hope that fully formal proofs become a routine part of math research and communication in the future.