Comment by kevinventullo

I contend it is the only way to move forward on the goal of “automating” mathematics. Although we’ve seen natural language approaches do well at IMO, the human effort required to verify higher level proofs is too great with hallucinations being what they are. With something like Lean, you don’t need a human verifier.