> But is this foolproof? Is a proof a proof just because Lean agrees it’s one? In some ways, it’s as good as the people who convert the proof into inputs for Lean.<p>Having studied CS in school I'm sort of triggered by this. Might be the editorialization, but this is a statement I have a problem with.<p>I am not one of those who think that computers will save us all. My point of view is that computers are meaningless machines that do meaningless operations on meaningless symbols unless proven otherwise. This is what gets drilled in your head in any semi-decent CS program and it's a point of view I came to agree with completely.<p>But we have proven otherwise.<p>Proof checkers like Lean, Coq, Matita, Isabelle and the like are not like normal code, they are more similar to type-systems and code expressed in their formalisms is directly connected to a valid mathematical proof (see the Curry-Howard isomorphism).<p>They are usually constructed as a tiny, hand-proven core, and then built on their own formalism, ensuring that what is exposed to the end user is perfectly grounded.<p>If a program is accepted by the proof checker, then <i>by construction</i> it must be a valid mathematical proof.<p>Of course, computers are physical machines that can potentially make all sorts of mistakes. Hardware failures, cosmic rays, whatever.
But the probability of that happening on a large scale is the same probability that seven billion people collectively hallucinated elementary theory and it's in fact not true that there are infinitely many prime numbers.<p>edit: Just a clarification: it's only this particular statement I have a problem with. The article is very much worth your time. Do not get derailed by the title, it's not some sort of "math is racist" nonsense.
I will always remember when I first got into serious proof-based math in the first semester of college, and I had to work hard to develop my sense of what counts as a sufficient proof. I would read the proofs in the textbook and hit the QED at the end and not understand why it was enough. Eventually I came to understand something like the framing here, which is that a proof is about persuasion, persuasion is about judgment, and judgment (by definition, maybe) can't be pinned down to clear rules.<p>The University of Chicago has a special math class format called Inquiry-Based Learning designed around this idea, where you work <i>together</i> in class to put proofs together and work out a shared understanding of what is sufficient. I didn't take it but I wish I had. You can read some people's experiences with it here[0].<p>[0]: <a href="https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_your_experience_like_in_honors_calc_ibl/" rel="nofollow noreferrer">https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_y...</a>
By late-undergrad, it was intuitive to me that "proof" means "all mathematicians who reads this agrees with it". Mathematics is unique in that, mostly, the field can achieve consensus on results, which we then call "proofs".<p>But similarly, it makes sense that, even if a result is is "true" in a universal, objective sense, if the mathematician cannot communicate this in a convincing fashion to the rest of the mathematics world, I don't think we can call that result "proved".
I find his scepticism about proof assistants like Lean a bit weird. Of course, there is never absolute certainty, but there are degrees. A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong, which is possible but less likely than a flaw in a proof that hasn't seen much scrutiny because it's rather unimportant (of course, "big" results get so much scrutiny that it's also very unlikely that they were wrong).
Whenever I want to think about "what does it mean to prove something?" I dig into my copy of Imre Lakatos's "Proofs and Refutations", a Socratic dialogue-style story where a bunch of aspiring theorem-provers try to prove a particular theorem about the Euler characteristic of polyhedra and discuss what they are actually doing and why it works or doesn't.<p>I originally picked up the book because I was trying to understand Euler's polyhedral formula better -- which in retrospect is kind of like reading Zen and the Art of Motorcycle Maintenance because you wanted to fix a motorcycle.<p>I'm not wired for pure math -- I loved real analysis then quit while I was ahead. Still it's fun to pretend sometimes, and Lakatos does a great job of making you feel like you're learning inside knowledge about what mathematicians do. He introduces fun concepts like "monster-barring" (the way people sometimes carve out special cases in a proof when they encounter counterexamples).<p>I've never made it the whole way through, but I like to go back every few months and absorb a little more.<p>edit to add: I just now skimmed the author's Wikipedia entry and the Stanford Encyclopedia of Philosophy's story about the author's interaction with someone named Éva Izsák and I have a ton of questions.
> Moreover, one could play word games with the mathematical language, creating problematic statements like “this statement is false” (if it’s true, then it’s false; if it’s false, then it’s true) that indicated there were problems with the axiomatic system.<p>I hope this isn't too far off topic, but can someone clarify exactly how this problem indicts axioms? As an uninformed and naive musing, it occurs to me that an issue with the statement "this statement is false" is <i>this</i>. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components.
There are weaker formal systems like Presburger arithmetic (peano without multiplication) and Skolem arithmetic (peano without addition) that have been proven to be complete and consistent. Tarski also showed that there are formal systems for real numbers (hence also geometry) which have the same properties. (although the real numbers include integers, the integers alone have a lot more structure and so Tarski's result does not imply Peano)<p>There are also extensions to these (eg. presburger extended to multiplication by constants) that are also known to be complete and consistent.<p>These systems do not require any social compact. Any theorems proven through them are absolute truth, although the the range of statements that these systems can express is limited.<p>One may require a social compact for Peano, ZFC, and such other powerful formal systems.<p>That the software implementations like Coq and Lean are bug free may also require a social compact, if the nature of being bug free cannot be formally proved, although it seems determining this should be an easier problem.
Whether a task is meaningful or meaningless depends on how we think about meaning. I tend to think about it in terms of correspondences between structures. Such structures are usually what we think of as information, so this comment has meaning when interpreted using the corresponding knowledge of English in your brain. A computer simulation of the weather has meaning to the extent that it corresponds to actual weather, and its behaviour. The environmental mapping data structures in a Roomba’s memory has meaning to the extent it corresponds to the environment it is navigating.<p>So meaning is about correspondences, but also about achieving goals. We communicate for many reasons, maybe in this case to help us understand problems better. The weather simulation helps us plan activities. The Roomba’s map helps it clean the room. So there’s also an element of intentionality.<p>What is the intention behind these mathematical proofs? What are their correspondences to other information and goals?
I mean... you can abuse language and math notation in ways that you can't do for computer code. Math notation is actually terribly and surprisingly informal compared to code. I'd just argue that many[*] of these "social disagreements" would go away within a computational framework. I think the future of mathematics is in computer proofs.<p>[*] Note that the claim is "many" (ie.: a subset), not "all".
>What AI can do that’s new is to verify what we believe to be true<p>This is not AI.<p>Combining Theorem Provers with AI is promising:<p><a href="https://leandojo.org/" rel="nofollow noreferrer">https://leandojo.org/</a>
Nice interview / thoughts. There was a great article almost exactly 10 years ago, revolving around the same example (Mochizuki's claimed proof of the abc conjecture) that this article starts with: <a href="http://projectwordsworth.com/the-paradox-of-the-proof/" rel="nofollow noreferrer">http://projectwordsworth.com/the-paradox-of-the-proof/</a> (It's still worth reading, even as background to the posted article.)
Good teacher, his Number Theory book felt really good though I have no comparable in Number Theory. I must say Number Theory and Combinatorics are the most difficult topics I got acquainted with in undergrad.
Catarina Dutilh Novaes has been arguing much the same thing. She has a 2021 book out, <i>The Dialogical Roots of Deduction,</i> which is on my list but I haven't gotten there yet.<p>I also haven't watched this video, but I'm linking it because I can't find an earlier one where she points out that the basis of logic is in rhetoric.<p><a href="https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO" rel="nofollow noreferrer">https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO</a>
> Initially, Newton and Leibniz came up with objects called infinitesimals. It made their equations work, but by today’s standards it wasn’t sensible or rigorous.<p>It would be great if mathematics was widely presented and taught in this messy, practical, human, truthful way rather than the purist, mystical, mythical manner.<p>Calculus wasn't "discovered", it was painstakingly <i>developed</i> by some blokes that were trying to solve physical problems.
Semantics of "Proof" are complicated.<p>Is incorrect proof still a "proof", just
one which is incorrect?<p>If Curry-Howard holds then programs are
"proofs". To write a proof is to write
a program.<p>But what about a program that
has a bug in it? We say it is an incorrect
program. But we still call it a program.
By the same logic an incorrect proof is
still a "proof" as well.<p>And typically it is a proof - of something.
Every formally valid proof proves SOMETHING,
right?<p>Instead of asking "Is this proof correct?"
we should ask: "Does this proof prove what
we claim it proves, or something else"?
I'm not a mathematician but I enjoy maths both as an anchor to an objective reality and as an art of expression (or rather compression of axiomatic ideas into tight and elegant
equations). A shift in the framework of thinking can radically change viewpoints we have adopted so far (if it's not the otherwise) however often to come off as controversial.<p>It reminds me of my old days in high-school when I was intrigued by unconventional ways of doing maths, I often had the habit of mixing many different domains into one derivation (which often led to people interpreting it as nonsense). I realize that even if I were "right", whether it is or not is dependent on a subjective, mutual, and shared convention.
My brain does not like the phrase "social compact" probably because I've heard "social contract" so often, and rarely if ever hear "compact" used in this way. On the other hand I hear "pact" much more often.
The best reference for proofs as social constructions is:<p>DeMillo, Lipton, Perlis<p><i>Social Processes and Proofs of Theorems and Programs</i><p><a href="https://gwern.net/doc/math/1979-demillo.pdf" rel="nofollow noreferrer">https://gwern.net/doc/math/1979-demillo.pdf</a>
I personally view maths as just another language. It’s just a medium to transmit ideas from one person to another with the most efficient symbol set possible. It can’t be anything else - it doesn’t exist without some kind of intelligent life form to decode it.
A couple of observations.<p>It's odd that the article doesn't spell out Zermelo–Fraenkel, and instead uses the shorthand ZFC axioms. At a fundamental level, axioms are simultaneously solid and slippery. The entire purpose of a set of axioms is to serve as a backstop. Without axioms there are no proofs, and instead you wind up riding infinite regress; turtles all the way down. In short, proofs without axioms are impossible.<p>But once you have a set of axioms, proofs are precisely that, proofs. The notion that mathematics is a social compact is aggrandizing the role of the axiom, and minimizing the rest of mathematics. It is certainly the case that axioms are in fact a "social compact" in the sense that if we cannot agree that a set of given axioms are true without proof, then we can prove nothing. But the goal of axioms is to make that compact as narrow and clear as possible.<p>The brief discussion of Godel's incompleteness theorem elides the fundamental nuance that incompleteness has only been demonstrated in the context of self reference. There is a longer and better discussion of how this relates to logic, science, and consciousness in Hofstadter's seminal work "Godel, Escher, Bach"