> The goal shouldn't be "does a human fully understand the whole thing" but "is it proven to be true?" > [...] > But no one needs to "understand everything".

> The goal shouldn't be "does a human fully understand the whole thing" but "is it proven to be true?" > [...] > But no one needs to "understand everything". Coming from a pure math background, I have to respectfully disagree. There is a serious debate in the philosophy of mathematics about what, precisely, is a proof. My own, and many others' view is roughly this: > Proofs are stories that convince suitably qualified others that a certain statement is true. > If I present you with a proof, and you have the appropriate background knowledge and ability, you can – usually with some time and effort – as a result of reading my story, become convinced that what I claim is true. > But if you take that as your working definition of proof, you have to acknowledge it is fundamentally about communication, not truth. In particular, whether an argument classifies as a proof depends as much on the intended reader as on its creator. [0] Many mathematicians do not consider a theorem to be "proved" until they understand why it is true. The four color theorem is a prime example of this. By now, literally every graph theorist considers the statement to be logically correct, but there are quite a few who would say that the computer verifications that are out there don't quite constitute "proof" for them. The problem is that these computer-based verifications are simply not conceptually accessible to the majority of working graph theorists who might want to know how the proof works. I haven't personally looked at any of them, but, I, as both a working SWE and someone with several graduate courses in graph theory, including topological graph theory, cannot honestly can't say that they would be accessible to me. The "story," to reference the Keith Devlin quote above, is written in a language that mathematicians simply do not understand. There are other issues, but this is the most fundamental. For instance, mathematicians highly value proofs that themselves offer insight into why the theorem should be true. They value proofs that offer new techniques to solve other problems (i.e. abstraction). While one can get this from a computer proof, it is far, far more difficult to extract these things from code than it is from traditional proofs one would see in a journal. The bottom line is that no, that is not "where we need to go," because that is simply not how mathematics functions. --- [0]: https://www.mathvalues.org/masterblog/what-is-a-mathematical-proof https://www.mathvalues.org/masterblog/what-is-a-mathematical...