33 ms·

Mathematical proof is a social compact

179 points by digital55 3y ago

davidgrenier 3y ago
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.
- Tainnor 3y ago
  Number Theory is really weird because the definitions and theorems are so often straightforward and easy to understand (you could explain Fermat's Last Theorem to a bright school kid), but the proofs can be devilishly complicated.
sctb 3y ago
> 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. 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 this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components.
- Tainnor 3y ago
  You're precisely right that it's the self-referentiality that gets us in trouble. Systems which don't have that don't suffer from Gödel-related problems (e.g. propositional logic, or arithmetic without multiplication). Unfortunately, what Gödel showed is that any logical system that is strong enough to capture addition and multiplication over natural numbers - and nothing more - includes self-referentiality. That includes the language of arithmetic - you can write down formulas that refer to themselves - and Turing machines (via the recursion theorem, any Turing Machine is equivalent to a machine that knows its own source code). The constructions are a bit technical, but it's possible.
  - finnh 3y ago
    Yeah I always thought that the construction of Gödel numbers was always the weakest part of the proof / the biggest leap of faith / the part your prof would just hand-wave as being a valid move. Of course once you get into Turing machines it all flows more naturally, what with all of us being accustomed to "code is just data".
    - Tainnor 3y ago
      I agree that Turing Machines feel more natural to programmers than first-order logic (although "natural" doesn't necessarily mean "rigorously proven"), but there are no leaps of faith involved in Gödel's construction. You can write down "P is provable" as a first-order sentence of arithmetic (which involves some number theoretic tricks), and you can also do the diagonalisation trick that gives you self-referentiality. That's really all you need.
- rmzz 3y ago
  I guess the problem is that the axioms are not preventing “this statement is false” to be an invalid statement.
- kmod 3y ago
  IANA mathematician, but I read "axiomatic system" broadly as including not just the axioms but also the logic in which they are based. My understanding is that a common interpretation is that ZFC axioms are a list of 10 strings of symbols, which only have some sort of meaning when you pick a logic that gives meaning to these symbols. But I think also that this particular understanding of what axioms are ("formalism") is just one way of understanding truth in mathematics, and there are others. https://en.wikipedia.org/wiki/Philosophy_of_mathematics https://en.wikipedia.org/wiki/Philosophy_of_mathematics As for this particular issue I think this wikipedia page is relevant: https://en.wikipedia.org/wiki/Impredicativity https://en.wikipedia.org/wiki/Impredicativity
  - thorel 3y ago
    This idea of giving "meaning" to a set of axioms is precisely captured by the notion of "interpretation" in logic [1]. The rough idea is to map the symbols of the formal language to some pre-existing objects. As you say, this gives one way of formalizing truth: a sentence (string of symbols that respect the syntax of your language) is true if it holds for the objects the sentence is referring to (via a chosen interpretation). This notion of truth is sometimes referred to as semantic truth. An alternative approach is purely syntactic and sees a logical system as collection of valid transformation rules that can be applied to the axioms. In this view, a sentence is true if it can be obtained from the axioms by applying a sequence of valid transformation rules. This purely syntactic notion of truth is known as “provability”. Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide. [1] https://en.wikipedia.org/wiki/Interpretation_(logic) https://en.wikipedia.org/wiki/Interpretation_(logic)
    - Tainnor 3y ago
      > Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide It's even more subtle than that. They do coincide in a sense, which is proven by Gödel's completeness theorem (well, at least in First-Order Logic). That one just says that a sentence is provable from some axioms exactly iff it's true in every interpretation that satisfy the axioms. So one thing that Gödel's first incompleteness theorem shows it's that it's impossible to uniquely characterise even a simple structure such as the natural numbers by some "reasonable"[0] axioms - precisely because there will always be sentences that are correct in some interpretations but not in others. Unless you use second-order logic - in which case the whole enterprise breaks down for different reasons (because completeness doesn't hold for second order logic). [0] reasonable basically means that it must be possible to verify whether a sentence is an axiom or not, otherwise you could just say that "every true sentence is an axiom"
- qsort 3y ago
  This is probably the editorialization. He's alluding to the fact that unlike what one might naively intuit, it's impossible to formulate a set of axioms that can formally express all mathematics. Because of Godel's incompleteness theorems, any formal system that's sufficiently powerful to formulate basic arithmetic (see for instance Robinson arithmetic) and consistent (that is, it cannot prove false statements) is both incomplete (meaning that it's possible to formulate a wff within that system that the system itself can neither prove nor disprove) and can't prove it's own consistency. This fact is often portrayed in popular media as being a "bug" or a "missing foundation" of mathematics. That is inaccurate -- it's just a property of how logical systems work -- but it does prove that the search for the holy grail of a grand unified system of axioms for all of mathematics is destined to remain fruitless. Modern mathematics is most often implicitly assumed to be formulated in a formal system called ZFC, but there are alternatives.
  - Tainnor 3y ago
    I think the second theorem is the "worse" result for mathematics. It shows that it's completely impossible to use a weaker system, which is hopefully self-evident, to prove the consistency of a stronger, but weirder system like ZFC. Hilbert wanted to show that, even if you don't "believe" in ZFC, we could at least try to convince you that it doesn't lead to contradictions, but that fundamentally didn't work.
    - qsort 3y ago
      Oh this is interesting, I didn't know about this historical detail. It makes sense, Godel's first could be mostly seen as a version of the halting problem, while the second is "game over" for a Hilbert-like foundation program. p.s. Just wanted to point out that it's funny how we wrote two mostly identical sets of comments. Great minds think alike? :)
      - Tainnor 3y ago
        > Oh this is interesting, I didn't know about this historical detail. That's the characterisation I got from Peter Smith's book about Gödel's theorems. I didn't verify original sources or anything, but it sounds very plausible to me. And it also kind of answers the question about why we should care: if a system can't prove its own consistency, well that's not terribly interesting (even if it could, we would have to believe the system a priori to trust its own consistency proof). But if it also can't prove a stronger system consistent, then that's much more interesting. > Great minds think alike? That would be a bit too self-aggrandizing for me. :D I'm very curious about logic (and maths in general), that's why I know some stuff about it, but I'm no maths genius.
- thorel 3y ago
  The article is a bit oversimplifying in summarizing the axiomatic crisis as being problem with sentences like “this statement is false“. This being said, your intuition is absolutely correct, the crux of the issue is with ‘this‘. What mathematicians realized is that if you are not careful with your choice of axioms, the resulting logical system becomes too “powerful” in the sense that it becomes self-referential: you can construct sentences that refer to themselves in a self-defeating manner. As others have mentioned, this is the idea underlying Gödel's incompleteness theorem but also, to some extent, Russel's paradox that came before and is what the article is referring to. In Russel's paradox, the contradiction comes from constructing the set of all sets that contain themselves.
  - Tainnor 3y ago
    Maybe in analogy to Russell's paradox and how you can "fix" it by distinguishing sets and classes, you can "fix" a Gödel sentence by adding it as an axiom, but then you'll just get a new Gödel sentence... and so on.
- deleted 3y ago
  [deleted]
- lmm 3y ago
  We would hope that the axioms fully characterised the thing they're meant to describe. Can we even talk about "the" natural numbers at all? If you have two copies of the natural numbers, one red and one blue, are they both the same? Well, trivially they're not: one's red and one's blue. But (we'd hope) all the statements in the language of the natural numbers (which doesn't talk about redness or blueness) that are true of the red copy will be true of the blue copy, so it doesn't matter which copy you use, they're both "the" natural numbers. E.g. why did we care about the parallel postulate? Why not just have geometry without a fith axiom? Well, because without it the axioms are, well, incomplete: there are statements in the language of geometry that cannot be proven from the other four axioms. You can have spherical geometry, planar geometry, and projective geometry, and they all conform to the first four axioms, but sometimes one of these geometrical statements will be true in one and false in another. So neither is "the" geometry, it matters which specific version of geometry you work in, and we need that fifth axiom to have a complete theory of (planar) geometry. We'd hope to avoid that kind of situation with the natural numbers - if we need any additional "parallel postulate", we'd like to know about it, and if we don't, we'd like to be able to prove that we don't need one rather than just assuming it because we haven't stumbled across it yet. But Goedel proved that we cannot have a provably complete theory of the natural numbers with addition and multiplication, because he found a way to encode a statement akin to "this statement is false" in the language of the natural numbers. Which indicts any axiomatization of arithmetic - either your axiomatization proves this statement is true (in which case it's inconsistent), it proves this statement is false (in which case it's also inconsistent), or it doesn't prove this statement one way or another (in which case it's incomplete). > As an uninformed and naive musing, it occurs to me that an issue with the statement "this statement is false" is this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components. Well, yes, getting around that is the clever part of Goedel's proof :).
- deleted 3y ago
  [deleted]
- downvotetruth 3y ago
  See section 7.1 and 10 of http://www.imm.dtu.dk/~tobo/essay.pdf http://www.imm.dtu.dk/~tobo/essay.pdf
deleted 3y ago
[deleted]
Tainnor 3y ago
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).
- davidgrenier 3y ago
  I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.
  - Tainnor 3y ago
    Yeah it's likely he hasn't worked much with Lean and may have some misconceptions around it.
  - SkiFire13 3y ago
    The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.
  - robinzfc 3y ago
    Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434 https://mathoverflow.net/a/291351/163434) to a MathOverflow question.
epgui 3y ago
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. [*] Note that the claim is "many" (ie.: a subset), not "all".
catskul2 3y ago
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.
- droptablemain 3y ago
  Construct seems more fitting. I also read the headline and thought it sounded like a mistake.
  - deleted 3y ago
    [deleted]
  - SamBam 3y ago
    I read a "social compact" as more of a "social agreement," which gets at the bottom of consensus that he's talking about. A "social construct" is quite different, that's something entirely constructed by society, like manners or nationalism.
    - epgui 3y ago
      I made the same comment as you in response to parent commenter (now deleted)... But then I looked at some definitions of "social construct" and it seems to have broader semantics than I had thought.
- Tainnor 3y ago
  It's especially weird because "compact" has a very specific meaning in mathematics.
dcre 3y ago
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. The University of Chicago has a special math class format called Inquiry-Based Learning designed around this idea, where you work together 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]. [0]: https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_your_experience_like_in_honors_calc_ibl/ https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_y...
- pjacotg 3y ago
  I recently read this book review [0] where a mathematical proof was described as a dialogue between two semi-adversarial but collaborative actors, the Prover and the Skeptic, who together aim to aquire mathematical insight. I thought it was an interesting perspective. [0] https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-the-dialogical-roots-of-deduction/ https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-t...
  - hgsgm 3y ago
    This also what philosophical discussion/debate is.
  - mikhailfranco 3y ago
    This is Game Theoretic Semantics. See Hintikka's Principles of Mathematics Revisited and his framing of Independence Friendly Logic: https://plato.stanford.edu/entries/logic-if/ https://plato.stanford.edu/entries/logic-if/
- agrounds 3y ago
  I was lucky enough to take two IBL courses from Dr. Michael Starbird at UT Austin. Both were wonderful courses, very engaging and very fun. I never collaborated so much with other math students as I did in those courses. In particular this was my intro to topology and I’ve been hooked on it ever since.
svat 3y ago
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: http://projectwordsworth.com/the-paradox-of-the-proof/ http://projectwordsworth.com/the-paradox-of-the-proof/ (It's still worth reading, even as background to the posted article.)
qsort 3y ago
> 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. 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. 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. But we have proven otherwise. 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). 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. If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof. 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. 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.
- markisus 3y ago
  I think the quote is about the fallibility of the humans who convert theorems into statements of type theory. You could end up with a valid theorem, but not the theorem you meant to prove. This would be a bug in the statement of the theorem, not the proof. For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.
  - Tainnor 3y ago
hackandthink 3y ago
>What AI can do that’s new is to verify what we believe to be true This is not AI. Combining Theorem Provers with AI is promising: https://leandojo.org/ https://leandojo.org/
joe__f 3y ago
What is the meaning of the word 'Compact' in the title here?
- math_dandy 3y ago
  An agreement, basically. https://legal-dictionary.thefreedictionary.com/Compact https://legal-dictionary.thefreedictionary.com/Compact
  - joe__f 3y ago
    Oh huh, I never saw it used like that before
    - passion__desire 3y ago
      Wasn't wittgenstein right? Words gets meaning through their usage and context.
- passion__desire 3y ago
  One metaphor that I have seen ubiquitous in Nature is Consensus Reality. Fiat currency, quantum systems agreeing on each other's value, social contract, etc. It's everywhere and now social concept of proof. Here is Daniel Dennett talking it. https://youtu.be/32u12zjgJww https://youtu.be/32u12zjgJww I like the no miracles argument in favour of science. If our scientific theories don't track reality, how are they successful in prediction the future. Similarly the social aspect of mathematical proofs can be replaced with requirements like being in congruence with established facts (i.e explanatory power), predictive power, and efficient representation (i.e. elegant compression) which means faster programs / less computational steps required.
reso 3y ago
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". 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".
- deleted 3y ago
  [deleted]
- SleekEagle 3y ago
  Not that you were, but I don't quite understand why people get so caught up on this fact. There are objective facts about the nature of reality, and we are all (or at least competent practitioners in the field) are thoroughly convinced that we have identified a subset of these facts. These presumed facts have helped us do things like go to the moon and build skyscrapers, but then someone comes along with the old "but how do you actually know" argument of a college freshman, and then we get into a conversation about the potential social relativism of math. All the while, people will see a half-assed psychology study with a questionable procedure, weak at best, erroneous at worst statistics and therefore tenuous at best conclusions, and this study is taken to be "true" and might legitimately impact notable institutions. Yet when we're talking about extremely complicated topics that exist on the edge of the horizon of human intuition, no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them. Foundational fields like mathematics and physics are as objective as we can get. If you don't accept that, your belief about what is objectively true ends at cogito ergo sum and that's that. This has always been such a pointless conversation in my mind.
  - joelfried 3y ago
    We communicate with words, and people as a whole are used to being lied to and gaslit regularly especially by those in power. It's true that mathematics and the hard sciences have mechanisms for understanding that are on a different scale than, say, ethics and morality. However, it takes time for people -- especially those currently engaged in questioning the nature of their reality[1] -- to accept that in this specific instance lying and gaslighting are a lot harder[2]. The people who eventually accept and internalize the distinction around things that can be objectively shown to be true are those who by in the large have done some of the work to understand these things themselves. Godel's Incompleteness Theorem is beautiful but it takes work to understand and if it didn't, it wouldn't be much of a meaningful breakthrough. Nobody is proving that 3+5=8 and then 4+5=9. So what the average person sees is a high level language they can't speak with people being absolutely positive that this thing is special and true and incontrovertible. That raises red flags when you're dealing with folks talking about normal everyday stuff, doesn't it? It's a lot harder to say "but I don't understand" and a lot easier to say "but what if you're wrong" socially. [1] As all college first years do, right? [2] Let's face it, lying to people is never impossible, it's just harder to be successful when you can be fact checked.
mcguire 3y ago
Catarina Dutilh Novaes has been arguing much the same thing. She has a 2021 book out, The Dialogical Roots of Deduction, which is on my list but I haven't gotten there yet. 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. https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO
- zodzedzi 3y ago
  Off-topic question: I've been seeing this "si" URL parameter pop up a lot in shared youtube links lately. Which app exactly pulled the URL for you?
  - mcguire 3y ago
    The share button under the YouTube video? :-)
    - deleted 3y ago
      [deleted]
pelorat 3y ago
Math is the description of how one number relates to another number. I'm not a math person but this Shinichi Mochizuki sounds like a hack job.
- pphysch 3y ago
  Mochizuki is an extreme case, but the problem of "bullshitting" is omnipresent in academia, and particularly (pure) mathematics which is a) perceived as consequential and b) impossible for laypeople to verify.
  - tacomonstrous 3y ago
    Professional pure mathematician here, so I'm curious if you have many examples of this bullshitting you seem to think is omnipresent. In my experience, the field is reasonably efficient at policing this, as in the case of the one example (Mochizuki) you cite. In fact, the reason he got any attention at all is because of his initial record of nonbullshit and quite non-trivial work on the anabelian program.
    - pphysch 3y ago
      I also have a degree in mathematics and am familiar with how the field operates. > In fact, the reason he got any attention at all is because of his initial record of nonbullshit Sure, if he didn't have a reputation to burn he would be dismissed a priori as a crank. No one should have the time to parse and debunk random 500-page manifestos. My issue with pure math is that, for any given (sub)*field, there are at best a handful of experts, and the probability of that small clique of experts being willing to spend time debunking/criticizing each other is low. Quid-pro-quo back-scratching has far better payout. We have an environment with low accountability, but also low stakes. Basically, my position is that pure math is chock full of arcane nonsense (bullshit is admittedly a strong term that implies bad faith). But, it also doesn't cause harm, so it's not a big deal. Still, it behooves anyone entering or established in mathematics to understand the reality of the game. You will deal with charlatans and it's acceptable if your own work isn't perfect or even remotely correct or applicable.
pphysch 3y ago
> 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. 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. Calculus wasn't "discovered", it was painstakingly developed by some blokes that were trying to solve physical problems.
- tho2i343243244 3y ago
  Actually, in all likelihood it was plagiarized from Indians like Madhava and spun out as 'white European' invention.
  - peanutcrisis 3y ago
    Could you provide evidence for your claim?
  - pphysch 3y ago
    Doesn't matter. All mathematics is derived from other's work.
nuc1e0n 3y ago
Seems that Lean could be considered as a programming language for mathematical proofs.
simonh 3y ago
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. 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. What is the intention behind these mathematical proofs? What are their correspondences to other information and goals?
rcarr 3y ago
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.
andrewprock 3y ago
A couple of observations. 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. 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. 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"
- pfdietz 3y ago
  There have been "natural" theorems which have been shown to be unprovable in Peano Arithmetic. https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...
  - eternityforest 3y ago
    What about with Pinot Arithmetic, where you drink wine until you're sure you're conjecture is a fact?
deleted 3y ago
[deleted]
deleted 3y ago
[deleted]
mherdeg 3y ago
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. 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. 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). I've never made it the whole way through, but I like to go back every few months and absorb a little more. 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.
- theresistor 3y ago
  I had to read that for a first-semester discrete math course in undergrad. It was... challenging.
mikhailfranco 3y ago
The best reference for proofs as social constructions is: DeMillo, Lipton, Perlis Social Processes and Proofs of Theorems and Programs https://gwern.net/doc/math/1979-demillo.pdf https://gwern.net/doc/math/1979-demillo.pdf
- mikhailfranco 3y ago
  Better link... https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf
ironborn123 3y ago
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) There are also extensions to these (eg. presburger extended to multiplication by constants) that are also known to be complete and consistent. 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. One may require a social compact for Peano, ZFC, and such other powerful formal systems. 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.
adunk 3y ago
I like to view mathematical proofs as code for a virtual machine that is executed in the minds of the readers of the proof.
peanutcrisis 3y ago
I wonder what people who are working on foundations think of this.
worthless443 3y ago
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. 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.
deleted 3y ago
[deleted]
galaxyLogic 3y ago
Semantics of "Proof" are complicated. Is incorrect proof still a "proof", just one which is incorrect? If Curry-Howard holds then programs are "proofs". To write a proof is to write a program. 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. And typically it is a proof - of something. Every formally valid proof proves SOMETHING, right? Instead of asking "Is this proof correct?" we should ask: "Does this proof prove what we claim it proves, or something else"?

179 points by digital55 3y ago

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.

Tainnor 3y ago
Number Theory is really weird because the definitions and theorems are so often straightforward and easy to understand (you could explain Fermat's Last Theorem to a bright school kid), but the proofs can be devilishly complicated.

sctb 3y ago

> 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. 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 this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components.

Tainnor 3y ago
You're precisely right that it's the self-referentiality that gets us in trouble. Systems which don't have that don't suffer from Gödel-related problems (e.g. propositional logic, or arithmetic without multiplication). Unfortunately, what Gödel showed is that any logical system that is strong enough to capture addition and multiplication over natural numbers - and nothing more - includes self-referentiality. That includes the language of arithmetic - you can write down formulas that refer to themselves - and Turing machines (via the recursion theorem, any Turing Machine is equivalent to a machine that knows its own source code). The constructions are a bit technical, but it's possible.
- finnh 3y ago
  Yeah I always thought that the construction of Gödel numbers was always the weakest part of the proof / the biggest leap of faith / the part your prof would just hand-wave as being a valid move. Of course once you get into Turing machines it all flows more naturally, what with all of us being accustomed to "code is just data".
  - Tainnor 3y ago
    I agree that Turing Machines feel more natural to programmers than first-order logic (although "natural" doesn't necessarily mean "rigorously proven"), but there are no leaps of faith involved in Gödel's construction. You can write down "P is provable" as a first-order sentence of arithmetic (which involves some number theoretic tricks), and you can also do the diagonalisation trick that gives you self-referentiality. That's really all you need.
rmzz 3y ago
I guess the problem is that the axioms are not preventing “this statement is false” to be an invalid statement.
kmod 3y ago
IANA mathematician, but I read "axiomatic system" broadly as including not just the axioms but also the logic in which they are based. My understanding is that a common interpretation is that ZFC axioms are a list of 10 strings of symbols, which only have some sort of meaning when you pick a logic that gives meaning to these symbols. But I think also that this particular understanding of what axioms are ("formalism") is just one way of understanding truth in mathematics, and there are others. https://en.wikipedia.org/wiki/Philosophy_of_mathematics https://en.wikipedia.org/wiki/Philosophy_of_mathematics As for this particular issue I think this wikipedia page is relevant: https://en.wikipedia.org/wiki/Impredicativity https://en.wikipedia.org/wiki/Impredicativity
- thorel 3y ago
  This idea of giving "meaning" to a set of axioms is precisely captured by the notion of "interpretation" in logic [1]. The rough idea is to map the symbols of the formal language to some pre-existing objects. As you say, this gives one way of formalizing truth: a sentence (string of symbols that respect the syntax of your language) is true if it holds for the objects the sentence is referring to (via a chosen interpretation). This notion of truth is sometimes referred to as semantic truth. An alternative approach is purely syntactic and sees a logical system as collection of valid transformation rules that can be applied to the axioms. In this view, a sentence is true if it can be obtained from the axioms by applying a sequence of valid transformation rules. This purely syntactic notion of truth is known as “provability”. Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide. [1] https://en.wikipedia.org/wiki/Interpretation_(logic) https://en.wikipedia.org/wiki/Interpretation_(logic)
  - Tainnor 3y ago
    > Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide It's even more subtle than that. They do coincide in a sense, which is proven by Gödel's completeness theorem (well, at least in First-Order Logic). That one just says that a sentence is provable from some axioms exactly iff it's true in every interpretation that satisfy the axioms. So one thing that Gödel's first incompleteness theorem shows it's that it's impossible to uniquely characterise even a simple structure such as the natural numbers by some "reasonable"[0] axioms - precisely because there will always be sentences that are correct in some interpretations but not in others. Unless you use second-order logic - in which case the whole enterprise breaks down for different reasons (because completeness doesn't hold for second order logic). [0] reasonable basically means that it must be possible to verify whether a sentence is an axiom or not, otherwise you could just say that "every true sentence is an axiom"
qsort 3y ago
This is probably the editorialization. He's alluding to the fact that unlike what one might naively intuit, it's impossible to formulate a set of axioms that can formally express all mathematics. Because of Godel's incompleteness theorems, any formal system that's sufficiently powerful to formulate basic arithmetic (see for instance Robinson arithmetic) and consistent (that is, it cannot prove false statements) is both incomplete (meaning that it's possible to formulate a wff within that system that the system itself can neither prove nor disprove) and can't prove it's own consistency. This fact is often portrayed in popular media as being a "bug" or a "missing foundation" of mathematics. That is inaccurate -- it's just a property of how logical systems work -- but it does prove that the search for the holy grail of a grand unified system of axioms for all of mathematics is destined to remain fruitless. Modern mathematics is most often implicitly assumed to be formulated in a formal system called ZFC, but there are alternatives.
- Tainnor 3y ago
  I think the second theorem is the "worse" result for mathematics. It shows that it's completely impossible to use a weaker system, which is hopefully self-evident, to prove the consistency of a stronger, but weirder system like ZFC. Hilbert wanted to show that, even if you don't "believe" in ZFC, we could at least try to convince you that it doesn't lead to contradictions, but that fundamentally didn't work.
  - qsort 3y ago
    Oh this is interesting, I didn't know about this historical detail. It makes sense, Godel's first could be mostly seen as a version of the halting problem, while the second is "game over" for a Hilbert-like foundation program. p.s. Just wanted to point out that it's funny how we wrote two mostly identical sets of comments. Great minds think alike? :)
    - Tainnor 3y ago
      > Oh this is interesting, I didn't know about this historical detail. That's the characterisation I got from Peter Smith's book about Gödel's theorems. I didn't verify original sources or anything, but it sounds very plausible to me. And it also kind of answers the question about why we should care: if a system can't prove its own consistency, well that's not terribly interesting (even if it could, we would have to believe the system a priori to trust its own consistency proof). But if it also can't prove a stronger system consistent, then that's much more interesting. > Great minds think alike? That would be a bit too self-aggrandizing for me. :D I'm very curious about logic (and maths in general), that's why I know some stuff about it, but I'm no maths genius.
thorel 3y ago
The article is a bit oversimplifying in summarizing the axiomatic crisis as being problem with sentences like “this statement is false“. This being said, your intuition is absolutely correct, the crux of the issue is with ‘this‘. What mathematicians realized is that if you are not careful with your choice of axioms, the resulting logical system becomes too “powerful” in the sense that it becomes self-referential: you can construct sentences that refer to themselves in a self-defeating manner. As others have mentioned, this is the idea underlying Gödel's incompleteness theorem but also, to some extent, Russel's paradox that came before and is what the article is referring to. In Russel's paradox, the contradiction comes from constructing the set of all sets that contain themselves.
- Tainnor 3y ago
  Maybe in analogy to Russell's paradox and how you can "fix" it by distinguishing sets and classes, you can "fix" a Gödel sentence by adding it as an axiom, but then you'll just get a new Gödel sentence... and so on.
deleted 3y ago
[deleted]
lmm 3y ago
We would hope that the axioms fully characterised the thing they're meant to describe. Can we even talk about "the" natural numbers at all? If you have two copies of the natural numbers, one red and one blue, are they both the same? Well, trivially they're not: one's red and one's blue. But (we'd hope) all the statements in the language of the natural numbers (which doesn't talk about redness or blueness) that are true of the red copy will be true of the blue copy, so it doesn't matter which copy you use, they're both "the" natural numbers. E.g. why did we care about the parallel postulate? Why not just have geometry without a fith axiom? Well, because without it the axioms are, well, incomplete: there are statements in the language of geometry that cannot be proven from the other four axioms. You can have spherical geometry, planar geometry, and projective geometry, and they all conform to the first four axioms, but sometimes one of these geometrical statements will be true in one and false in another. So neither is "the" geometry, it matters which specific version of geometry you work in, and we need that fifth axiom to have a complete theory of (planar) geometry. We'd hope to avoid that kind of situation with the natural numbers - if we need any additional "parallel postulate", we'd like to know about it, and if we don't, we'd like to be able to prove that we don't need one rather than just assuming it because we haven't stumbled across it yet. But Goedel proved that we cannot have a provably complete theory of the natural numbers with addition and multiplication, because he found a way to encode a statement akin to "this statement is false" in the language of the natural numbers. Which indicts any axiomatization of arithmetic - either your axiomatization proves this statement is true (in which case it's inconsistent), it proves this statement is false (in which case it's also inconsistent), or it doesn't prove this statement one way or another (in which case it's incomplete). > As an uninformed and naive musing, it occurs to me that an issue with the statement "this statement is false" is this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components. Well, yes, getting around that is the clever part of Goedel's proof :).
deleted 3y ago
[deleted]
downvotetruth 3y ago
See section 7.1 and 10 of http://www.imm.dtu.dk/~tobo/essay.pdf http://www.imm.dtu.dk/~tobo/essay.pdf

deleted 3y ago

[deleted]

Tainnor 3y ago

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).

davidgrenier 3y ago
I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.
- Tainnor 3y ago
  Yeah it's likely he hasn't worked much with Lean and may have some misconceptions around it.
- SkiFire13 3y ago
  The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.
- robinzfc 3y ago
  Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434 https://mathoverflow.net/a/291351/163434) to a MathOverflow question.

epgui 3y ago

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. [*] Note that the claim is "many" (ie.: a subset), not "all".

catskul2 3y ago

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.

droptablemain 3y ago
Construct seems more fitting. I also read the headline and thought it sounded like a mistake.
- deleted 3y ago
  [deleted]
- SamBam 3y ago
  I read a "social compact" as more of a "social agreement," which gets at the bottom of consensus that he's talking about. A "social construct" is quite different, that's something entirely constructed by society, like manners or nationalism.
  - epgui 3y ago
    I made the same comment as you in response to parent commenter (now deleted)... But then I looked at some definitions of "social construct" and it seems to have broader semantics than I had thought.
Tainnor 3y ago
It's especially weird because "compact" has a very specific meaning in mathematics.

dcre 3y ago

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. The University of Chicago has a special math class format called Inquiry-Based Learning designed around this idea, where you work together 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]. [0]: https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_your_experience_like_in_honors_calc_ibl/ https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_y...

pjacotg 3y ago
I recently read this book review [0] where a mathematical proof was described as a dialogue between two semi-adversarial but collaborative actors, the Prover and the Skeptic, who together aim to aquire mathematical insight. I thought it was an interesting perspective. [0] https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-the-dialogical-roots-of-deduction/ https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-t...
- hgsgm 3y ago
  This also what philosophical discussion/debate is.
- mikhailfranco 3y ago
  This is Game Theoretic Semantics. See Hintikka's Principles of Mathematics Revisited and his framing of Independence Friendly Logic: https://plato.stanford.edu/entries/logic-if/ https://plato.stanford.edu/entries/logic-if/
agrounds 3y ago
I was lucky enough to take two IBL courses from Dr. Michael Starbird at UT Austin. Both were wonderful courses, very engaging and very fun. I never collaborated so much with other math students as I did in those courses. In particular this was my intro to topology and I’ve been hooked on it ever since.

svat 3y ago

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: http://projectwordsworth.com/the-paradox-of-the-proof/ http://projectwordsworth.com/the-paradox-of-the-proof/ (It's still worth reading, even as background to the posted article.)

qsort 3y ago

> 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. 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. 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. But we have proven otherwise. 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). 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. If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof. 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. 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.

markisus 3y ago
I think the quote is about the fallibility of the humans who convert theorems into statements of type theory. You could end up with a valid theorem, but not the theorem you meant to prove. This would be a bug in the statement of the theorem, not the proof. For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.
- Tainnor 3y ago

hackandthink 3y ago

>What AI can do that’s new is to verify what we believe to be true This is not AI. Combining Theorem Provers with AI is promising: https://leandojo.org/ https://leandojo.org/

joe__f 3y ago

What is the meaning of the word 'Compact' in the title here?

math_dandy 3y ago
An agreement, basically. https://legal-dictionary.thefreedictionary.com/Compact https://legal-dictionary.thefreedictionary.com/Compact
- joe__f 3y ago
  Oh huh, I never saw it used like that before
  - passion__desire 3y ago
    Wasn't wittgenstein right? Words gets meaning through their usage and context.
passion__desire 3y ago
One metaphor that I have seen ubiquitous in Nature is Consensus Reality. Fiat currency, quantum systems agreeing on each other's value, social contract, etc. It's everywhere and now social concept of proof. Here is Daniel Dennett talking it. https://youtu.be/32u12zjgJww https://youtu.be/32u12zjgJww I like the no miracles argument in favour of science. If our scientific theories don't track reality, how are they successful in prediction the future. Similarly the social aspect of mathematical proofs can be replaced with requirements like being in congruence with established facts (i.e explanatory power), predictive power, and efficient representation (i.e. elegant compression) which means faster programs / less computational steps required.

reso 3y ago

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". 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".

deleted 3y ago
[deleted]
SleekEagle 3y ago
Not that you were, but I don't quite understand why people get so caught up on this fact. There are objective facts about the nature of reality, and we are all (or at least competent practitioners in the field) are thoroughly convinced that we have identified a subset of these facts. These presumed facts have helped us do things like go to the moon and build skyscrapers, but then someone comes along with the old "but how do you actually know" argument of a college freshman, and then we get into a conversation about the potential social relativism of math. All the while, people will see a half-assed psychology study with a questionable procedure, weak at best, erroneous at worst statistics and therefore tenuous at best conclusions, and this study is taken to be "true" and might legitimately impact notable institutions. Yet when we're talking about extremely complicated topics that exist on the edge of the horizon of human intuition, no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them. Foundational fields like mathematics and physics are as objective as we can get. If you don't accept that, your belief about what is objectively true ends at cogito ergo sum and that's that. This has always been such a pointless conversation in my mind.
- joelfried 3y ago
  We communicate with words, and people as a whole are used to being lied to and gaslit regularly especially by those in power. It's true that mathematics and the hard sciences have mechanisms for understanding that are on a different scale than, say, ethics and morality. However, it takes time for people -- especially those currently engaged in questioning the nature of their reality[1] -- to accept that in this specific instance lying and gaslighting are a lot harder[2]. The people who eventually accept and internalize the distinction around things that can be objectively shown to be true are those who by in the large have done some of the work to understand these things themselves. Godel's Incompleteness Theorem is beautiful but it takes work to understand and if it didn't, it wouldn't be much of a meaningful breakthrough. Nobody is proving that 3+5=8 and then 4+5=9. So what the average person sees is a high level language they can't speak with people being absolutely positive that this thing is special and true and incontrovertible. That raises red flags when you're dealing with folks talking about normal everyday stuff, doesn't it? It's a lot harder to say "but I don't understand" and a lot easier to say "but what if you're wrong" socially. [1] As all college first years do, right? [2] Let's face it, lying to people is never impossible, it's just harder to be successful when you can be fact checked.

mcguire 3y ago

Catarina Dutilh Novaes has been arguing much the same thing. She has a 2021 book out, The Dialogical Roots of Deduction, which is on my list but I haven't gotten there yet. 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. https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO https://youtu.be/0IOhYneseiM?si=vEfJ-JFCPF05zzNO

zodzedzi 3y ago
Off-topic question: I've been seeing this "si" URL parameter pop up a lot in shared youtube links lately. Which app exactly pulled the URL for you?
- mcguire 3y ago
  The share button under the YouTube video? :-)
  - deleted 3y ago
    [deleted]

pelorat 3y ago

Math is the description of how one number relates to another number. I'm not a math person but this Shinichi Mochizuki sounds like a hack job.

pphysch 3y ago
Mochizuki is an extreme case, but the problem of "bullshitting" is omnipresent in academia, and particularly (pure) mathematics which is a) perceived as consequential and b) impossible for laypeople to verify.
- tacomonstrous 3y ago
  Professional pure mathematician here, so I'm curious if you have many examples of this bullshitting you seem to think is omnipresent. In my experience, the field is reasonably efficient at policing this, as in the case of the one example (Mochizuki) you cite. In fact, the reason he got any attention at all is because of his initial record of nonbullshit and quite non-trivial work on the anabelian program.
  - pphysch 3y ago
    I also have a degree in mathematics and am familiar with how the field operates. > In fact, the reason he got any attention at all is because of his initial record of nonbullshit Sure, if he didn't have a reputation to burn he would be dismissed a priori as a crank. No one should have the time to parse and debunk random 500-page manifestos. My issue with pure math is that, for any given (sub)*field, there are at best a handful of experts, and the probability of that small clique of experts being willing to spend time debunking/criticizing each other is low. Quid-pro-quo back-scratching has far better payout. We have an environment with low accountability, but also low stakes. Basically, my position is that pure math is chock full of arcane nonsense (bullshit is admittedly a strong term that implies bad faith). But, it also doesn't cause harm, so it's not a big deal. Still, it behooves anyone entering or established in mathematics to understand the reality of the game. You will deal with charlatans and it's acceptable if your own work isn't perfect or even remotely correct or applicable.

pphysch 3y ago

> 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. 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. Calculus wasn't "discovered", it was painstakingly developed by some blokes that were trying to solve physical problems.

tho2i343243244 3y ago
Actually, in all likelihood it was plagiarized from Indians like Madhava and spun out as 'white European' invention.
- peanutcrisis 3y ago
  Could you provide evidence for your claim?
- pphysch 3y ago
  Doesn't matter. All mathematics is derived from other's work.

nuc1e0n 3y ago

Seems that Lean could be considered as a programming language for mathematical proofs.

simonh 3y ago

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. 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. What is the intention behind these mathematical proofs? What are their correspondences to other information and goals?

rcarr 3y ago

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.

andrewprock 3y ago

A couple of observations. 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. 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. 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"

pfdietz 3y ago
There have been "natural" theorems which have been shown to be unprovable in Peano Arithmetic. https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...
- eternityforest 3y ago
  What about with Pinot Arithmetic, where you drink wine until you're sure you're conjecture is a fact?

deleted 3y ago

[deleted]

deleted 3y ago

[deleted]

mherdeg 3y ago

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. 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. 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). I've never made it the whole way through, but I like to go back every few months and absorb a little more. 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.

theresistor 3y ago
I had to read that for a first-semester discrete math course in undergrad. It was... challenging.

mikhailfranco 3y ago

The best reference for proofs as social constructions is: DeMillo, Lipton, Perlis Social Processes and Proofs of Theorems and Programs https://gwern.net/doc/math/1979-demillo.pdf https://gwern.net/doc/math/1979-demillo.pdf

mikhailfranco 3y ago
Better link... https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf

ironborn123 3y ago

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) There are also extensions to these (eg. presburger extended to multiplication by constants) that are also known to be complete and consistent. 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. One may require a social compact for Peano, ZFC, and such other powerful formal systems. 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.

adunk 3y ago

I like to view mathematical proofs as code for a virtual machine that is executed in the minds of the readers of the proof.

peanutcrisis 3y ago

I wonder what people who are working on foundations think of this.

worthless443 3y ago

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. 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.

deleted 3y ago

[deleted]

galaxyLogic 3y ago

Semantics of "Proof" are complicated. Is incorrect proof still a "proof", just one which is incorrect? If Curry-Howard holds then programs are "proofs". To write a proof is to write a program. 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. And typically it is a proof - of something. Every formally valid proof proves SOMETHING, right? Instead of asking "Is this proof correct?" we should ask: "Does this proof prove what we claim it proves, or something else"?