Comment by monkeyelite

My claim is not that nobody ever makes mistakes, it’s formalizing in a computer is extremely high cost for very little reward and doesn’t help the core process of finding proof ideas