> 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.
Once upon a time, the professor of a class on logic I was taking pointed out that, if you proved some famous open conjecture (I think Fermat's was the example) using some simple proof that everyone had just missed so far, mathematicians would pat you on the head, maybe give you an award or something, and you (and the conjecture) would become another forgotten footnote.
Major mathematical advances come from difficult problems when a new branch of mathematics is invented to solve them. Think of calculus, non-Euclidean geometry, and Turing machines (and their equivalents).
The problem I see with Coq, the proof checker I've worked with the most, and the others I've seen is that the proofs they result in are neither good, understandable programs nor good, understandable proofs. They are as complicated as complex programs, but written in something that isn't a half-way clean programming language, but they're also not written as a traditional proof. That goes back up to the article's point that the purpose of a proof is to convince and enlighten others.
Sure, I'd have to say a proposition proven in Coq is true, but how do you get from that to the ideas in the proof letting you go on to other problems?
I don't think the point is to either have good math or good code.
When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq.
When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.
I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked.
Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).
There is something similar Nima Arkani-Hamed talks about Feynman equations during his amplituhedron lecture, pages and pages of equations being reduced to simple representation.
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.
1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do).
2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.
It's an important problem and people in formal verification are aware of it. One example of tackling this is that the Lean LTE team accompanies the proof with "several files corresponding to the main players in the statement" and "[they] should be (approximately) readable by mathematicians who have minimal experience with Lean [...] to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished".
I'm with you almost everywhere, but it's worth pondering this:
> If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.
I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct.
To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)
But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.
For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.
But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.
I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale.
Eg.
- Are you sure the compiler is correct?
- Are you sure the OS is behaving correctly?
- Are you sure the CPU isn't randomly glitching out?
There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all.
How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.
This is a great point. In a computer proof system, you produce judgements like "the term x has type is T", where the type "T" encodes the statement of a theorem and "x" is the proof. We must be certain that whenever the type checker verifies that "x has type T", it means that the theorem "T" is actually true. Such a meta-proof must be done on pen and paper, before any code is written at all. Any bug in this meta-proof would destroy our ability to rely on the computer proof system.
> the same probability that seven billion people collectively hallucinated elementary theory
Just for fun, it's not unprecedented that the entire human race is disposed to mislearn basic truths about the universe which have to be unlearned when you get to the point where it matters. See quantum mechanics.
One hopes that conscientious mathematicians are careful to select axiomatizations (such as ZF set theory or the type system of Lean) which faithfully reflect reality. And, within such a system, we can be extremely confident in what we're doing. But the distinct possibility remains that the axiomatization doesn't actually match our universe and, say, admits a proof of false or implies something not physically realizable, such as that a certain computation should terminate, when no real life physical machine obeying the laws of physics can ever do so.
Be careful with things like "faithfully reflect reality". :-)
Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.
I think his argument is exactly that, those formal systems can suffer from errors (even though they've been checked), because the compiler could have errors, the processor could have errors, etc
So in the end, it's always a question of "community" and "belief that things seen by sufficiently many people are right", eg that after 10 years of using a CPU, we've identified and fixed most bugs, and so the program is even more likely to be valid
You're still performing meaningless operations on meaningless symbols. All you've done is picked a subset that looks - to you - as if it's a little less meaningless.
It's a problem of epistemology, not logic.
Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.
We label a certain set of psychological experiences "true", a certain related set "logical", and a different related set "experimentally valid."
But all we really have is a set of experiences that are subjectively consistent (more or less) and shared.
IMO it's quite likely we're missing a lot. Far from having god-like insight into the ultimate nature of truth and reality our minds are actually quite small and limited.
Many relationships, operations, and elements of objective reality are literally invisible to us because they're far too complex for us to imagine, never mind experience and understand.
This matters because potentially AI may not have the same limitations. We're just getting started with associative cognitive modelling based on ML data compression as opposed to mechanical machine building - which is what traditional code is.
That's a fundamental difference of approach, with the potential to work with a much larger conceptual and symbolic space than we're capable of.
I suspect we'll see some quite interesting outcomes.
> Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.
I agree that it is this way, but does it have to be? Is it physically necessary to perceive defection from this dilemma as "pedantic" (see below, how surprising!), or might it only be culturally necessary?
Take your claim for example: you are not distinguishing between logic itself and our experience of logic. You are objectively correct that there is in fact no distinction on one level (experience), but that is not the only level that exists.
How are questions of this nature (essentially: existence) answered in the physical realm, where we have high levels of skill and experience?
The thing that these systems offer is "having to check less code". In some situations, that's huge. In others, it's not worth the effort it takes to get there and maybe doesn't actually reduce the complexity of checking that it all makes sense.
In other words, maybe you proved something beyond reasonable doubt, but that's completely useless if you misunderstand what it was that you proved.
For me, the entire article can be summarised in the following quote from it:
>> So there’s a big mess. We are limited in what we can do.
We are limited in what can do. All our formal systems are flawed. That's including arithmetic and Gödel proved that any system powerful enough to represent arithmetic will always be flawed. The machines we have that compute our formal systems with us -and it never stops doing my head in that it's possible to create physical machines to calculate what exists only in our thoughts- our computers, they are flawed, too, because they are based on the same flawed formal systems, the same limitations as ours. We cannot use such machines to escape their own, our own, limitations.
It's not wrong that we are limited in what we can do, but we are limited in the same sense a Turing machine is limited by the halting problem. We are limited in a very specific and precise sense.
> All our formal systems are flawed.
This threads dangerously close to the pop-culture take that math is flawed. I can accept this statement only if we take 'flawed' to mean 'incomplete' in the Godel sense. We don't say that integers are flawed because they aren't a field, that's how integers work. We should avoid needlessly loaded words.
> Have we now. To whom?
We don't prove things to someone. Proofs just are.
There's a sleight of hand at play here. A proof in the technical sense (let's call them Tproofs), as a series of deductions, is a mathematical object, not unlike the number five. A proof in the common sense (let's call them Cproofs) is an informal argument to convince other human beings that there exists a Tproof with certain characteristics. In this sense it's easy to see how Cproofs are social phenomena. They are basically ways to communicate with other human beings. Not unlike how banks create money when they issue loans, backed by nothing by the community's trust, a mathematician can write a Cproof standing for a Tproof, backed by the trust of his colleagues. Mathematics could not meaningfully function without this socially constructed web of trust, exactly like the economy could not function if our only mean of exchange were physical coins.
I have no problems in accepting that, in this sense, mathematics is a community effort and is strictly dependent on such community existing.
But there lies my argument. A proof-checker accepting a proof offers a very strong guarantee that an equivlent Tproof exists, stronger than any number of peer-reviewers could offer.
Therefore, to the extent that we deem epistemologically possible to mathematically prove a statement, a proof being accepted by a proof-checker is a mathematical proof.
The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.
> 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.
That's the fundamental problem. We're building the machines to verify an internally consistent idea that we're all pretty pleased with. For example, type systems don't tell you that your data is true or correct, they just provide a framework of assumptions to work from that turn out to be really useful. Each type system will provide a different view on your data/process/etc.
Most senior, non-applied mathematicians in academia (including those with fancy titles at prestigious universities) outright refuse to adapt even simplest technological advances, like version control, let alone think about possible large scale transformation of mathematics. I wouldn't take take anything that they say about technology too seriously.
That's not how it works. If you input garbage in Lean or other proof checker they will just tell you it's wrong. You would have to input garbage in the statement you want to prove for them to accept a wrong proof (which must still be correct for that garbage statement!). To rule this out you just have to manually check the translation of the statement, which is most often much much smaller than the proof itself.
You have a point, but to be fair the person you replied to didn't use the word "truth". They said "valid mathematical proof". An in the context of type theory or formal logic "valid proof" is indeed something that has been "defined into existence" (in type theory "valid proof" ≈ "well-typed term"). Whether it represents "truth" is a different matter. Though such systems can (ideally) be proven sound in and with respect to "normal" mathematics. At that point I guess the "truth"ness depends on you overall belief in math :)
All mathematical "truths" are defined into existence as you call it. All mathematical proofs are essentially of the form If A Then B. B is only a "truth" since we defined A a certain way and accept it as True. Due to its very nature, there are no empirical facts in mathematics.
You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.
They aren't assumed to be bug-free. It's simply known that the vast majority of bugs that occur in practice and that you have to care about aren't compiler or hardware bugs. So formal systems have a lot less bugs.
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].
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.
It definitely takes a second to develop that intuition, I remember being quite confused as well. As I got more into CS, I began to think of proofs similar to how I do unit tests: you externalize or “fix” as many as the inputs as you possibly can, and then abuse the remaining degrees of freedom as much as possible to show that your solution is complete.
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.
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".
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.
> There are objective facts about the nature of reality
This is a pretty bold claim and you would have to do a bit of work to make it more convincing. Besides, it's not really how science works. Different theories wax and wane over time all the time. What we're really doing with science is coming up with ever better models that give us greater predictive power.
You could argue that at the macro scale we're asymptotically approaching some kind of objective truth with the whole endeavor of science, but you can't simply tunnel across that gap and make the leap to say that we know there is an objective truth.
The best that we can do is probably say something along the lines of "these are the best methods of getting closer to the truth that we have available - if anyone claims to have better methods, they are very likely wrong", but you still need to have the humility to accept that even the best models that we have to date are not infallible. They do not give us the objective truth, nor do they promise to, but they are the most effective tools that we have available to us at the current time. This is critically not the same as claiming that they give us the objective truth.
You could say that for all intents and purposes/everyday usage, "sure, these are objective facts about reality" - but I don't actually think that helps anyone and it serves to foment mistrust towards science and scientists. I think the best chance we have at preserving the status of science and scientists in our society starts by being honest about what it actually is giving us - which is quite a lot, but let's not oversell it for the sake of convience or whatever.
This fact is interesting because many people grew up with an idea of mathematics as having discovered fundamental truth, and some of us, when we get deep into the field, realize that Math is made up of human ideas, exactly the same as a very complex boardgame we play in our heads, and that the belief that these boardgames represent something fundamental about reality is it's own leap of faith.
> 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"
...
> 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.
I think the intersection of these two groups is the null set.
> Foundational fields like mathematics and physics are as objective as we can get.
Objective? Yes. But objective does not equate to "true"[1]. One requires data, and the other lives only in the mind. It is not at all problematic to ponder over whether mathematics is "true" - most mathematicians have an opinion one way or another, and they are not unanimous in their opinions.
[1] True w.r.t reality, not true in the logic sense.
> There are objective facts about the nature of reality
Such as?
> "but how do you actually know" argument of a college freshman
Epistemology has been studied by some of the greatest thinkers since the ancient greeks ( probably even before ) and not just college freshmen.
> no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them.
If you have to intuitively understand them, it isn't very objective is it?
> Foundational fields like mathematics and physics are as objective as we can get.
What in math are objective facts about the nature of reality? Where in nature is the number 1? Also do you realize that many mathematicians don't even accept the 'reality' of real numbers.
I think as you think more deeply about these topics, you will change your tune.
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.
After the article, my opinion is going to be that people do this because they are politically privileged by a social relativistic argument. The professor in the interview is advantaged by the narrative that proofs are socially constructed.
Indeed, mathematics and any other STEM field is deeply political. People are politics. But to confuse that--that STEM as practiced is socially constructed and political--and to make a sloppy ontological conclusion about what STEM/math is, is a deeply neoliberalizing argument. So I'm inclined to make the argument that it is actually the neoliberal intellectuals who try to spin this as fundamentally only a human enterprise, because it privileges their social standing as the "correct" practitioners of this compact: capitalism requires that mathematicians be able to "sell" each other the truth of their proofs.
Indeed, the article mentions the Mochizuki controversy but I don't think they understood the social problem. See, it doesn't matter if Mochizuki is right or wrong, or if people understood his 500 pages or not. It is that in principle it could be shown that he is right or wrong. And that's unlike, say, the Bible, which is also a social compact. Reduction of STEM to social construct throws the baby out with the bathwater.
No, no, I think you're missing the point. Mathematics is such that all mathematicians, in particular Brouwer and Hilbert, will read a proof and say "yes, this follows" or "no, it doesn't follow". The agreement is on the argumentation, i.e. what can be said given a set of assumptions. This doesn't mean there are no disagreements in the Philosophy of Mathematics. The place Brouwer and Hilbert disagrees is about what can be assumed at all times. The disagreement is on the foundation that mathematics lies on. This is also not the only disagreement, there are various models of what mathematics really is. You can ask N philosophers of mathematics (who are also trained in math) about a proof and they'll all agree that the mechanism of the proof follows. What they may disagree on is whether the assumptions are sound, and what "mathematics" really is. Some will focus on the social aspect and point out that "proof" ultimately means "convinces all mathematicians". Some will focus on the psychological aspect. Some will push mathematics outside of material realm etc etc.
That's like claiming all historians agree that Hitler was born in 1889 ergo historians achieve consensus on results.
If you study a broad range of subjects, you'd realize in mathematics the level of convergence is quite high relative to the other subjects, even the "hard" sciences. I wouldn't say it's 100% though.
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).
I wouldn't characterize him as being sceptical about Lean; this is what he says:
> Some terrific developments have happened with proof verification. Like [the proof assistant] Lean, which has allowed mathematicians to verify many proofs, while also helping the authors better understand their own work, because they have to break down some of their ideas into simpler steps to feed into Lean for verification. […] I’m not saying that I believe something like Lean is going to make a lot of errors. […] They can be a very valuable tool for getting things right — particularly for verifying mathematics that rests heavily on new definitions that are not easy to analyze at first sight. There’s no debate that it’s helpful to have new perspectives, new tools and new technology in our armory.
In between (the "[…]"s above), he says:
> 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. Which sounds very much like how we do traditional mathematics. […] I’m just not sure it’s any more secure than most things done by humans. […] I’m afraid I have a lot of skepticism about the role of computers. […] what I shy away from is the concept that we’re now going to have perfect logical machines that produce correct theorems. You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on.
The latter part is less about the correctness and more about community: the main goal of mathematics is not merely a "true" theorems, but (human) mathematical understanding. I wrote an answer about this on math.SE in 2014 (mostly quoting Thurston and Rota): https://math.stackexchange.com/questions/632705/why-are-math...
I agree that a big part of proving thing is understanding intuitively "why" they are true. That's part of the reasons why I don't think we'll just write proofs in Lean in 50 years and leave it at that (the other reason is that, at least for now, those systems are very "stupid" and need a lot of handholding to prove facts that any maths undergraduate would understand to be true).
But when he says that he doesn't believe that a proof in Lean is "more secure than most things done by humans" I fundamentally disagree.
I agree very much with you... but it seems to me like theorem provers / computers can be a really helpful tool in building trust and understanding between people or between groups of people, in ways that printed paper can't quite match.
I read it more as him saying that at the end of the day a human is inputting symbols into Lean, and a human is interpreting the meaning of the proof that Lean has verified. Not that the mechanics of the proof checking are in doubt, but that that meaning of it all is still a social consensus.
I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's kernel, it will almost never invalidate a Lean proof, because bugs in the Lean kernel (or the kernels of other proof assistants) are, just like with normal programs, almost always bugs dealing with edge cases testing the boundaries of mathematics or syntax, not things that show up in everyday proofs. Coq has fixed numerous proofs of False and, to my knowledge, these fixes have never ended up invalidating a "real" proof that wasn't specifically designed to test these kinds of edge cases. Proofs are far more often broken by changes to the surface syntax (e.g. inference algorithms or the tactic language) than by changes to the kernel.
Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics.
(I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).
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.
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.
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) to a MathOverflow question.
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.
> 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.
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.
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.
Is the fact that these systems cannot prove their own consistency actually a feature of the incompleteness theorem? I thought it effectively boiled down to "you can keep either consistency or completeness, not both". It's been a while since my metamathematics course ...
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.
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".
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.
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.
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 :).
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
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.
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.
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?
Readit News
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.
Major mathematical advances come from difficult problems when a new branch of mathematics is invented to solve them. Think of calculus, non-Euclidean geometry, and Turing machines (and their equivalents).
The problem I see with Coq, the proof checker I've worked with the most, and the others I've seen is that the proofs they result in are neither good, understandable programs nor good, understandable proofs. They are as complicated as complex programs, but written in something that isn't a half-way clean programming language, but they're also not written as a traditional proof. That goes back up to the article's point that the purpose of a proof is to convince and enlighten others.
Sure, I'd have to say a proposition proven in Coq is true, but how do you get from that to the ideas in the proof letting you go on to other problems?
When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq.
When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.
Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).
@56:26 in https://youtu.be/sv7Tvpbx3lc
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.
2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.
Details in this blog post: https://leanprover-community.github.io/blog/posts/lte-exampl...
> If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.
I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct.
Edit: this is not entirely academic. from what I understand, the unsoundness of Hindley-Milner in the presence of polymorphic references was not immediately known (https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).
But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.
For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.
But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.
But we've definitely gotten it right this time...
[0] https://github.com/coq/coq/issues/4294
Eg.
- Are you sure the compiler is correct?
- Are you sure the OS is behaving correctly?
- Are you sure the CPU isn't randomly glitching out?
There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all.
How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.
Just for fun, it's not unprecedented that the entire human race is disposed to mislearn basic truths about the universe which have to be unlearned when you get to the point where it matters. See quantum mechanics.
One hopes that conscientious mathematicians are careful to select axiomatizations (such as ZF set theory or the type system of Lean) which faithfully reflect reality. And, within such a system, we can be extremely confident in what we're doing. But the distinct possibility remains that the axiomatization doesn't actually match our universe and, say, admits a proof of false or implies something not physically realizable, such as that a certain computation should terminate, when no real life physical machine obeying the laws of physics can ever do so.
Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.
So in the end, it's always a question of "community" and "belief that things seen by sufficiently many people are right", eg that after 10 years of using a CPU, we've identified and fixed most bugs, and so the program is even more likely to be valid
It's a problem of epistemology, not logic.
Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.
We label a certain set of psychological experiences "true", a certain related set "logical", and a different related set "experimentally valid."
But all we really have is a set of experiences that are subjectively consistent (more or less) and shared.
IMO it's quite likely we're missing a lot. Far from having god-like insight into the ultimate nature of truth and reality our minds are actually quite small and limited.
Many relationships, operations, and elements of objective reality are literally invisible to us because they're far too complex for us to imagine, never mind experience and understand.
This matters because potentially AI may not have the same limitations. We're just getting started with associative cognitive modelling based on ML data compression as opposed to mechanical machine building - which is what traditional code is.
That's a fundamental difference of approach, with the potential to work with a much larger conceptual and symbolic space than we're capable of.
I suspect we'll see some quite interesting outcomes.
I agree that it is this way, but does it have to be? Is it physically necessary to perceive defection from this dilemma as "pedantic" (see below, how surprising!), or might it only be culturally necessary?
Take your claim for example: you are not distinguishing between logic itself and our experience of logic. You are objectively correct that there is in fact no distinction on one level (experience), but that is not the only level that exists.
How are questions of this nature (essentially: existence) answered in the physical realm, where we have high levels of skill and experience?
Not really, by your logic (heh) everything is subjective: including your own argument about logic being subjective (which in turn uses logic).
In other words, maybe you proved something beyond reasonable doubt, but that's completely useless if you misunderstand what it was that you proved.
Math generally has a higher bar (for better or worse..)
>> So there’s a big mess. We are limited in what we can do.
We are limited in what can do. All our formal systems are flawed. That's including arithmetic and Gödel proved that any system powerful enough to represent arithmetic will always be flawed. The machines we have that compute our formal systems with us -and it never stops doing my head in that it's possible to create physical machines to calculate what exists only in our thoughts- our computers, they are flawed, too, because they are based on the same flawed formal systems, the same limitations as ours. We cannot use such machines to escape their own, our own, limitations.
>> But we have proven otherwise.
Have we now. To whom?
It's not wrong that we are limited in what we can do, but we are limited in the same sense a Turing machine is limited by the halting problem. We are limited in a very specific and precise sense.
> All our formal systems are flawed.
This threads dangerously close to the pop-culture take that math is flawed. I can accept this statement only if we take 'flawed' to mean 'incomplete' in the Godel sense. We don't say that integers are flawed because they aren't a field, that's how integers work. We should avoid needlessly loaded words.
> Have we now. To whom?
We don't prove things to someone. Proofs just are.
There's a sleight of hand at play here. A proof in the technical sense (let's call them Tproofs), as a series of deductions, is a mathematical object, not unlike the number five. A proof in the common sense (let's call them Cproofs) is an informal argument to convince other human beings that there exists a Tproof with certain characteristics. In this sense it's easy to see how Cproofs are social phenomena. They are basically ways to communicate with other human beings. Not unlike how banks create money when they issue loans, backed by nothing by the community's trust, a mathematician can write a Cproof standing for a Tproof, backed by the trust of his colleagues. Mathematics could not meaningfully function without this socially constructed web of trust, exactly like the economy could not function if our only mean of exchange were physical coins.
I have no problems in accepting that, in this sense, mathematics is a community effort and is strictly dependent on such community existing.
But there lies my argument. A proof-checker accepting a proof offers a very strong guarantee that an equivlent Tproof exists, stronger than any number of peer-reviewers could offer.
Therefore, to the extent that we deem epistemologically possible to mathematically prove a statement, a proof being accepted by a proof-checker is a mathematical proof.
The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.
That's the fundamental problem. We're building the machines to verify an internally consistent idea that we're all pretty pleased with. For example, type systems don't tell you that your data is true or correct, they just provide a framework of assumptions to work from that turn out to be really useful. Each type system will provide a different view on your data/process/etc.
Deleted Comment
Huh? How? Truth is an empirical fact, you can't possibly define it into existence.
You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.
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_y...
I thought it was an interesting perspective.
[0] https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-t...
https://plato.stanford.edu/entries/logic-if/
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".
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.
This is a pretty bold claim and you would have to do a bit of work to make it more convincing. Besides, it's not really how science works. Different theories wax and wane over time all the time. What we're really doing with science is coming up with ever better models that give us greater predictive power.
You could argue that at the macro scale we're asymptotically approaching some kind of objective truth with the whole endeavor of science, but you can't simply tunnel across that gap and make the leap to say that we know there is an objective truth.
The best that we can do is probably say something along the lines of "these are the best methods of getting closer to the truth that we have available - if anyone claims to have better methods, they are very likely wrong", but you still need to have the humility to accept that even the best models that we have to date are not infallible. They do not give us the objective truth, nor do they promise to, but they are the most effective tools that we have available to us at the current time. This is critically not the same as claiming that they give us the objective truth.
You could say that for all intents and purposes/everyday usage, "sure, these are objective facts about reality" - but I don't actually think that helps anyone and it serves to foment mistrust towards science and scientists. I think the best chance we have at preserving the status of science and scientists in our society starts by being honest about what it actually is giving us - which is quite a lot, but let's not oversell it for the sake of convience or whatever.
...
> 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.
I think the intersection of these two groups is the null set.
> Foundational fields like mathematics and physics are as objective as we can get.
Objective? Yes. But objective does not equate to "true"[1]. One requires data, and the other lives only in the mind. It is not at all problematic to ponder over whether mathematics is "true" - most mathematicians have an opinion one way or another, and they are not unanimous in their opinions.
[1] True w.r.t reality, not true in the logic sense.
Such as?
> "but how do you actually know" argument of a college freshman
Epistemology has been studied by some of the greatest thinkers since the ancient greeks ( probably even before ) and not just college freshmen.
> no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them.
If you have to intuitively understand them, it isn't very objective is it?
> Foundational fields like mathematics and physics are as objective as we can get.
What in math are objective facts about the nature of reality? Where in nature is the number 1? Also do you realize that many mathematicians don't even accept the 'reality' of real numbers.
I think as you think more deeply about these topics, you will change your tune.
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.
Indeed, mathematics and any other STEM field is deeply political. People are politics. But to confuse that--that STEM as practiced is socially constructed and political--and to make a sloppy ontological conclusion about what STEM/math is, is a deeply neoliberalizing argument. So I'm inclined to make the argument that it is actually the neoliberal intellectuals who try to spin this as fundamentally only a human enterprise, because it privileges their social standing as the "correct" practitioners of this compact: capitalism requires that mathematicians be able to "sell" each other the truth of their proofs.
Indeed, the article mentions the Mochizuki controversy but I don't think they understood the social problem. See, it doesn't matter if Mochizuki is right or wrong, or if people understood his 500 pages or not. It is that in principle it could be shown that he is right or wrong. And that's unlike, say, the Bible, which is also a social compact. Reduction of STEM to social construct throws the baby out with the bathwater.
Deleted Comment
No. See Brouwer–Hilbert controversy.
They can't even agree on what makes mathematical logics.
Hard sciences are the same, yes?
Water is two parts hydrogen, one part oxygen.
If you study a broad range of subjects, you'd realize in mathematics the level of convergence is quite high relative to the other subjects, even the "hard" sciences. I wouldn't say it's 100% though.
> Some terrific developments have happened with proof verification. Like [the proof assistant] Lean, which has allowed mathematicians to verify many proofs, while also helping the authors better understand their own work, because they have to break down some of their ideas into simpler steps to feed into Lean for verification. […] I’m not saying that I believe something like Lean is going to make a lot of errors. […] They can be a very valuable tool for getting things right — particularly for verifying mathematics that rests heavily on new definitions that are not easy to analyze at first sight. There’s no debate that it’s helpful to have new perspectives, new tools and new technology in our armory.
In between (the "[…]"s above), he says:
> 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. Which sounds very much like how we do traditional mathematics. […] I’m just not sure it’s any more secure than most things done by humans. […] I’m afraid I have a lot of skepticism about the role of computers. […] what I shy away from is the concept that we’re now going to have perfect logical machines that produce correct theorems. You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on.
The latter part is less about the correctness and more about community: the main goal of mathematics is not merely a "true" theorems, but (human) mathematical understanding. I wrote an answer about this on math.SE in 2014 (mostly quoting Thurston and Rota): https://math.stackexchange.com/questions/632705/why-are-math...
But when he says that he doesn't believe that a proof in Lean is "more secure than most things done by humans" I fundamentally disagree.
Deleted Comment
That, or an error in the specification (ie.: not the implementation).
(I very much am with you that his attitude / way of framing it is a bit weird)
Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics.
(I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).
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.
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.
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.
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.
To mathematicians and non-mathematicians.
Being unable to prove or disprove certain statements is a rainy cloud. Like maybe the Riemann hypothesis is just impossible to prove.
It doesn't mean math is "broken" but it is disappointing, no?
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.
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".
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.
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 :).
As for this particular issue I think this wikipedia page is relevant: https://en.wikipedia.org/wiki/Impredicativity
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)
Deleted Comment
Deleted Comment
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.
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?