Titans of Mathematics Clash Over Epic Proof of ABC Conjecture
quantamagazine.org
quantamagazine.org
I think you are understating the certainty of fundamental proofs like this.
Once such a fundamental proof is considered "true", it almost always has applications beyond what the original proof was used for. It is often used to try to prove things that we already know are "true" in other ways.
So, any "true" proof generally gets tested from multiple directions.
Wile's proof is a good example of this. It doesn't just prove Fermat's Last Theorem. Quoting Wikipedia: "Wiles' path to proving Fermat's Last Theorem, by way of proving the modularity theorem for the special case of semistable elliptic curves, established powerful modularity lifting techniques and opened up entire new approaches to numerous other problems."
I have a PhD in an esoteric field myself. There's literally <50 people worldwide who write/verify proofs in it. I've spotted errors in my own work or other's work that got past peer review. And I don't think I'm particularly special. There's just not enough eyeballs, time and incentives sometimes.
It only takes one to break it. And, for something so fundamental, it's a big deal if you are the one.
This isn't physics, where you have to rule out all manner of confounding data before you can trust your conclusion.
For example, given the axioms of Euclidean geometry, I can prove that the sum of the angles of a triangle add up to 180 degrees.
That statement is true. Full stop.
Now the starting axioms may not be correct (the parallel postulate, for example, is not required to be true). However, given the starting axioms, proofs are true. Period.
In addition, there will be things in mathematics that you cannot prove--Godel's Incompleteness Theorem sits in this section.
And, science has the problem that a hypothesis can only be disproven.
Mathematics does not suffer from the same issue, though.
This same could be said of many other professions, medicine and psychology to start. It seems a related manifestation of the Gells-Mann Amnesia.
Claims that a statement is in category 1 are fully verifiable (by providing the proof). The same goes with claims that a statement is in category 2.
A proof is exactly how we demonstrate that a formula follows from the axioms.
(This might be one reason, from https://en.wikipedia.org/wiki/Mathematical_proof#Computer-as... )
Computers can easily verify that proof is correct once the proof is written down using formal semantics. Proof checkers already exist.
Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication and knowledge. These assumptions make proofs far more implicit than proofs in a formal language, which essentially only assumes that the "reader", i.e. the computer, can push symbols around and compare them.
Maybe there was surprising resistance because you spoke like that?
They're mathematicians, not display interface experts. This is like demanding that someone explain to you why they don't like a particular kind of food -- people are allowed to dislike things without having a complete internal axiomatic system justifying it.
1) computer displays require you to scroll, which interrupts your mental flow
2) paper and pencil or pen is free-form
3) in advanced mathematics, results are rarely calculated in numerical form, so the computer isn't helpful
4) notebooks are permanent. No backups needed.
I imagine the same is true for most cartoon artists.
1) Mathematicians write all over the papers and books they read. Electronic versions of this exist (e.g., Xournal, written by a well known mathematician), but they tend not to be as convenient as simply scribbling on paper.
2) Mathematicians digest papers nonlinearly. Digital presentations don't usually lend themselves to flipping back and forth between pages. At times, I suspect mathematicians use papers and books as memory mansions, organizing concepts by relating them to their location in the physical copy.
That's a fairly weak argument: you can browse an electronic document in a non-linear fashion way easier than a book.
And also: books don't have CTRL-F
How do I make handwritten side notes? How can I create a bookmark for a specific page? How can I view multiple non-contiguous pages next to each other? How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11") and send it to a collaborator?
However, to nevertheless address your points:
>How do I make handwritten side notes
There is a number of applications to do this (e.g. xournal), and when combined with a touchscreen on a decent hirez modern device, we're getting close to what paper can do. I'll grant you: this is still the weak point of computers as compared to pen and paper (especially for scribbling diagrams), but it won't be for long.
>How can I create a bookmark for a specific page
I'm not sure if you're trolling here, all e-book readers I've used have this feature.
>How can I view multiple non-contiguous pages next to each other?
Multiple windows ? CTRL+N ?
>How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11") and send it to a collaborator?
Cut and paste?
Or ... sending him an email with ""3rd paragraph on page 11"" in the body?
If you present a 100 page book as a folder of 100 image files instead, most of these become image manipulation problems:
>How do I make handwritten side notes?
The same way you'd edit an image.
> How can I create a bookmark for a specific page?
Create a subdirectory with the page or a link to the page.
> How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11")
Cut and paste the excerpt into a new image file.
> and send it to a collaborator?
File sharing is a solved problem. Hell, you can even share it on Instagram if you so choose.
love of math and love of technology aren't as closely linked as you believe.
And what Grad student can afford those at [Insert State University]. I was a PhD student in math not long ago, and vastly preferred paper books, and even printed out articles. It is way way easier on your eyes than something actively blasting light. Maybe in 20 years high quality e-ink will be cheap enough, but that has been promised since forever.
See, this is the kind of bad argument that really irks me. There are good arguments about how computers aren't ready to replace pen and paper for actively doing math, and even a few shortcomings for computers replacing paper textbooks. But "actively blasting light" doesn't mean anything. Photons are photons. If you think a backlit display is somehow harder on your eyes than an indirectly-lit piece of paper, then you should be trying to figure out whether you simply have the backlight set too bright for your surroundings, or if your screen's contrast ratio at reasonable brightness levels is inadequate. Your LCD's default settings are probably optimized for movie-watching more than reading, but that's easily fixed and definitely not an inherent limitation of all backlit displays everywhere.
This may be true, but in my experience(not very wealthy, typically sub $400 devices) the presets are set such that 0% backlight in the OS is glaringly bright. I cannot turn it down without rooting the device.
Color temperature can also be a problem, but there's a lot of awareness of that issue nowadays. Most operating systems now support automatic adjustment of color temperature based on time of day, plus manual adjustment. Devices that adjust their color temperature to account for ambient lighting are starting to catch on, and I expect they'll be pretty common in a few years.
Maybe you don't see the problem because you aren't doing any math?
But also..all my favourite books have markings on each page, margin comments, turned-over corners etc. Any pdf book I read more than once or twice, I'll get a paper copy, I think.
Text editor customizations to trigger `make <current-doc>.pdf` on save. (Emacs in my case)
A PDF viewer that reloads the PDF when it changes on disk (Skim in my case, which does auto-reload, but I also have some Applescript in the Makefile to poke Skim so that it notices the file change faster).
A good text editor LaTeX editing mode (Emacs in my case).
Random test editor customizations for working on LaTeX.
My main tips are
1. don't be shy of perfecting your work environment
2. use git to track both your work environment customizations and your LaTeX work.
Yes, e-books have other advantages - but calling it a paper fetish basically means you're making an uninformed call, because you're not even aware of the advantages.
The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position.
And you thought the resistance was surprising?
> The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position.
I didn't propose any specific markup because the specific syntax isn't the problem. The problem is that the predominant markup language for mathematical documents is LaTeX, which is a bit too presentation-oriented rather than semantic/structure-oriented for it to be really easy to use it to produce documents that can be interactively folded (especially when the output file format is almost always PDF). Something that used eg. MathML and an HTML/XML based overall document structure can trivially encode all the information necessary for rich interactive reading, and proposing specific tag or class names to indicate what lines of a proof should be collapsed by default only invites bikeshedding.
I think you're quite unjustified in accusing me of being so thoroughly uninformed.
The real reason people don't do this is simple, it would require an inhumane amount of work and details which will likely be wrong themselves and will for sure be to boring to be checked. Most science is wrong in some aspects, sometime it is better to have a meaningful intuition that can be understood by other expert (and maybe rejected)
I'm not surprised. Virtually all "designers" think low contrast text is better, despite high contrast being preferred on paper. They deliberately reduce contrast by setting the text color to gray. Even Firefox's Reader View, which otherwise fixes most mistakes of designers, sets the text to gray unless you override it in userContent.css. Desktop GUIs often have low contrast text too, which is also difficult to fix. Unless somebody somebody knows how to do this their expensive monitor will be wasted.
The point is that it's not simple. It will require significant advances in computer science.
I don't think we should have papers being nothing but folds, but there is definite value in presenting proofs in this way.
One potential downside is that there is no longer an order that guides the reader through the paper. Because it isn't quite clear how deep the author expected you to unfold an argument.
The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is then to develop languages which encompass these modern methods.
This is really the goal of the homotopy type theory project, to provide a language which is both machine checkable and easy to use informal reasoning with.
[1]https://www.microsoft.com/en-us/research/publication/write-2...
For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.
“The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1]
Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size.
[1]https://www.quantamagazine.org/univalent-foundations-redefin...
> Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).
The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when interpreted as proofs, don't verify properties nearly as strong as a real theorem. The difference between a proof of `Integer -> Integer` and `Integer -> Odd Integer` is already a gulf the vast majority of software does not bridge.
We're just not there yet. Voevodsky's program is a great first step but just that: A first step. No one really knows what the next thousand steps will be. It's not straightforward at all.
However:
"The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. "
Mis-understands why and how we use the linux kernel. Linux isn't that difficult to understand really (both in LOC, and the abstractions it presents). It's simply a base which can be relied on that provides abstraction points we can interface with (both as software, _and_ hardware_).
The important part here is that not only does linux give us a reliable "library" of behavior, but it is one that is common and reuseable.
This "library" of behavior is something we've begun to see present itself in category theory. This is why so many modern papers start with "we show that there exists a isomorphism...".
The biggest thing _modern_ computing and libraries focuses on is composition of behavior. Aka functions that take functions. If a computational interpenetration of uni-valence is found we will have similar capabilities in math (e.g. making it possible to simplify the process of moving between isomorphic structures). I believe this would be a major stride towards broader use of machine verification.
https://www.heidelberg-laureate-forum.org/blog/video/lecture...
If we accept that a software program is isomorphic to a proof, is there anything that isn't isomorphic with a proof?
I can prove Pythogoras' theorem with a diagram, so by extension anything in the physical world is a manifestation of mathematical theory and, since it exists, is isomorphic with a trivial proof for something.
I don't think I agree with this statement. As a matter of fact, I've always had a deep unease with so-called "geometric proofs", where a succession of visual transformations of a diagram are used to prove a theorem.
You can certain explain the intuition behind the proof of Pythagoras theorem with a diagram, and there's huge pedagogic value in doing that.
But to me it isn't a formal proof until it has been codified in a language that a computer can walk from start to end making sure each step is valid.
Basically, although code and proofs are in a sense isomorphic, I think everything and proofs are isomorpic in the same sense. So claiming that proofs should be structured to the same standards as code because code is isomorphic to proof is a bit of a non-sequitur. Why not show the layout of my rock garden is isomorphic to code and hence proving something (my rock garden can be Turing complete) and then claim my rock garden should be structured like a program?
Basically, the idea that the structure mathematicians favour for proofs have fallen behind programmers laying out of code is not well substantiated and the idea that 'proofs are isomorphic to code' is not useful because it is far too broad.
All of the relationships between these are the same too (e.g. a program `p` has type `T`, iff the proof `p` proves the proposition `T`; the proof `w` proves that the existence of `x` implies the proposition `y AND z` iff the program `w` is a function which generates a tuple of `(y, z)` when given an argument implementing the interface `x`; and so on).
Mathematicians and programmers do care about different things. Mathematicians are more concerned with informally proving previously unknown results; which corresponds to something like learning that a type has a value by sketching some pseudocode. Programmers care deeply about how many steps their proofs (programs) take to simplify; how easy it is to modify a proof to prove a slightly different proposition, etc. Yet there are so many good ideas on each side that are immediately applicable (e.g. dependently typed languages take rigorous logical systems and view them as programming languages; proof engineering takes software engineering ideas and applies them to building and maintaining proofs).
I'm struggling to think of an activity involving rock gardens that corresponds precisely to, say, universal quantification.
Of course, that still leaves the same problem of explicit proofs being tedious, i.e. being able to prove pythagoras's theorem "with a diagram" does not mean being able to prove it "within an explicit, formalised diagram language".
Types are propositions, and programs are proofs of their types. Unfortunately most programs are overly-complicated proofs of trivial propositions (when looked at from the mathematical side of curry-howard; of course what's actually the case is that we tend to only use types to specify a tiny part of what our programs are meant to do).
In an untyped language every expression has the same type (which we might call `Thing`, and contains integers, strings, functions, etc.) so in the curry-howard sense every expression is proof of the same trivial proposition.
I'm inclined to think of the laws of physics (whatever they are) as a programming language, and physical systems as programs running in that language. On first impression, it doesn't seem like physics is typed; hence every physical system is a proof of a trivial proposition (essentially: physical things can exist). It would be interesting to hear a counterargument though.
Note that in these cases it's the types/propositions which are trivial, not necessarily the programs/proofs. Consider that we could, if we wanted, prove a pretty trivial proposition like `((A -> B) AND A) -> B` in a roundabout way that involved applications of Fermat's last theorem. I tend to call such things "(over)complicated", rather than "complext", since their complexity isn't inherent or required.
Just as an example, Russell & Whitehead's Principia Mathematica famously requires some 400+ pages to prove that 1+1=2 (well, they prove some other stuff, too, I suppose.)
See the image and caption here to get a flavour: https://en.wikipedia.org/wiki/Principia_Mathematica
The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html
It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory.
It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large.
If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE#
1+1=1+S(0) [definition of 1]
1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)]
1+1=S(1+0) [transitivity of equality]
S(1+0)=S(1) [definition of addition, a+0=a]
1+1=S(1) [transitivity of equality]
S(1)=2 [definition of 2]
1+1=2 [transitivity of equality]
Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.
Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.)
What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?
And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...
I think there are two parts:
1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something.
2) Provide some sort of computational intelligence to fill in natural gaps of proofs. I believe humans tend to leave a large number of more or less trivial gaps even in rigorous mathematical proofs that couldn't be avoided by language syntax. For this probably some kind of AI system would be ideal that tries to derive successive results and complete the proof automatically.
It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).
You can help its heuristics by providing it a set of potential proof facts explicitly.
The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.)
To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on...
It's quite dense, but there are some bits that I, as a programmer, could understand.
[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.
theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare
The reality is that we often overlook issues with the spec until we try to implement it, or try using what we have implemented, even when we are trying to get the spec right first.
If you're referring to the fact that many proof assistants (e.g. Coq) are based on constructive/intuitionistic type theory, whilst most mathematics is formulated in classical set theory, then yes there is some translation involved. However, I would point out that we can use classical logic pretty easily by adding excluded middle, double negation elimination, etc. to an intuitionistic system (this is available in the Coq standard library https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html ). There are also systems which can use set theory (directly or indirectly), like Metamath and Isabelle.
Personally, I much prefer type theory (which I self-learned, before pursuing a related PhD) to set theory (which I was taught as an undergraduate and enjoyed, but not enough to do it as a hobby). However, I'm well aware that my computer scientist background is nothing like that of a trained mathematician.
"Proof assistants" like Coq and Isabelle can generate some of the more "obvious" steps using metaprogramming (known as "tactics").
However, it shoudln't deter us from the goal.
People used to code in assembly and Fortran. It was and still is quite painful.
But programming languages have improved, and resorting to those original languages (which is what Coq is) is rarely necessary these days.
They are not used because it's tedious to type and proof every step in the process. Mathematicians don't write all steps down. You also need build a library from ground up.
We could to the same for computer programs but we don't wan to do that either.
At least we are better off than theoretical physicists :-)
The if you had exensionality things get really weird
Disclaimer: What I don't know bout maths would fill volumes, in both senses of the word
Edit: From the down-votes, apparently not.
Obvious in this case means something like “clear to a mathematician familiar with the field” or “otherwise many things will fall apart”
This leads to the situation where if a mistake is found in a theorem then it is likely still true even if the proof is wrong.
All this is tied up in Gödel's incompleteness theorem.
It's true that some things cannot be proven, due to Goedel's incompleteness theorems... but that is a fundamental limitation of mathematics and has nothing to do with the limitations of computer tools.
You can write proof verifiers that are very generic. The metamath proof verifiers, for example, can work with arbitrary axiom systems. Most people use metamath to prove statements using classical logic with ZFC, but there are a number of other systems that are supported. Quine's New Foundationd set theory axioms and intuitionistic logic are alsk supported.
"I don't really understand why the entire known mathematics is not automatically proven yet."
Which I believe is going to be related to English (or whatever natural language) if we really want to talk about what is meant by "entire known mathematics".
edit: I mean it's a crazy proposal, so you get a crazy response. I think somewhat intuitively we know you can't prove everything.
Take for instance euclidean geometry. In the world of equations, everything works. But a point, or a line, are neither things that exist out in the world, much less their relations which, when drawn on the surface of the earth, are probably not actually euclidean at all.
Number theory in particular is almost never about math, but about the patters mathematicians believe they recognize. Somebody a'ong the lines goes "oh hey check out this flower. I bet this is the only flower of this type in the world" and then spend hundreds of years trying to prove it.
The short answer is that mathematics is not actually a very good application for computation. It's a rather poor application for computation. Herein lies the rub and the reason why it can't be done as easily as you'd suppose. Computationally-oriented questions and theorems are a subset of all available mathematics research in the same way that computer science is only a subset of all available applied mathematics. Stated another way, imagine the massive difference of effort involved between developing an application that works and formally proving that your application works for all possible inputs. It's extremely difficult to take the set of all possible test cases and reduce them to a set of equivalence classes which can be individually proved. This is the difference between constructive and non-constructive proofs.
Most mathematics is not actually constructive, which intrinsically presents a difficulty for computational theorem proving. Furthermore a lot of mathematics (particularly in the various flavors of analysis) is continuous in nature, which is inherently difficult for a computer to correctly model. For example, computers don't actually deal with real numbers, the floating points are just a good enough practical approximation of them.
If you look at the noteworthy cases where computer-assisted theorem proving has done very well, they generally fall into one of two categories:
1. Cases where the program mechanizes a well-established theorem with a vast amount of scaffolding theory already existing around it. In this way it's relatively easier to automatically prove much of undergraduate mathematics, the bulk of which has been reduced to very succinct proofs over the past few centuries (undergraduate mathematics doesn't really make it past the late 19th century in terms of novelty).
2. Cases where a vast problem can be provably reduced to a large but finite number of special cases, each of which can then be individually proven. The four color theorem is an example of this variant of automated theorem.
To give you an idea of how monumental the gap between research mathematics theorems and computation is: in order to make as much progress as we have, we've had to develop an entirely new theory of foundational mathematics (type theory). This allows us to bridge the gap between theorems and automated proofs in a way that set theory doesn't really allow. But that's a huge undertaking and a very quickly growing field of math.
When it comes down to it, mathematicians do not tend to do research in, nor does their intuition naturally map to, a computationally rigid language. Essentially no current mathematician was taught or trained to do their research in a computational manner unless that was explicitly their field of research. Furthermore, while mathematical terminology looks formal to an outsider, there is a significant amount of symbolic overloading and notational interpretation in modern math. That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on."
THIS is the real reason more mathematics isn't computer-checked. You massively buried the lede.
> Most mathematics is not actually constructive, which intrinsically presents a difficulty for computational theorem proving
How so? There are plenty of theorem provers for classical logics.
> Furthermore a lot of mathematics (particularly in the various flavors of analysis) is continuous in nature, which is inherently difficult for a computer to correctly model.
You can do continuous mathematics in a theorem prover. E.g. much of the classical theory of ODEs has been formalized in various theorem provers. Proofs about infinite structures are still a finite sequence of axiom applications.
Furthermore, outside of theorem proving, numerical analysis and simulation of ODEs/PDEs is probably THE killer example of computers revolutionizing a field of mathematics...
> For example, computers don't actually deal with real numbers, the floating points are just a good enough practical approximation of them.
When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true.
Integers aren't decidable: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Reals are deciable: https://en.wikipedia.org/wiki/Real_closed_field#Model_theory...
> To give you an idea of how monumental the gap between research mathematics theorems and computation is: in order to make as much progress as we have, we've had to develop an entirely new theory of foundational mathematics (type theory).
Again, there's nothing stopping us from doing classical mathematics in a theorem prover.
I'm not talking about decidability. I'm talking about computability. Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed. But that has no bearing on the fitness of real numbers for computation. Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.
If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures!
Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions.
> Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed
No.
Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals.
If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand.
If I want to prove something arbitrary about real closed fields, I can press a button and go for a run.
Computers are much better at proving things about real closed fields than they are at proving things about integers!
> I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.
One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms.
This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)
I think the problem is that this would be a significant amount of programming and data entry work, and there's no incentive for anyone to put in this work. There are many important math papers that are written at a level that is enough for a human math professor to understand, but not for a symbolic mathematics program to understand.
Since math research is generally prioritized by other math professors, and the current system of publications is optimized for math professors to read, they have no incentive to convert to a "formal language proofs are what matters" model. And there is no real financial incentive for computer programmers to implement something like this if math professors don't want it.
At the end of the day, what is the benefit of formally proving mathematical theorems via computer? If the only people consuming math proofs are other mathematicians, the only point is to check that you haven't made a mistake, which is useful but perhaps not worth much investment because the current system already does okay at catching mistakes.
If you could actually develop new mathematical research more easily with computer assistance, then I think these formal methods would be quite valuable, but I don't see how that would happen.
/s
From page 6 with figure 1, to page 10 with figure 3, it's clear that even just changing to structured proofs over prose proofs can be helpful in catching errors. Of course the rest of the paper goes into detail about going even further... I don't know if Lamport's ideas have gained any more acceptance in the mathematics communities, but I'm doubtful. At least if memory serves the ABC papers were classic prose-style...
https://www.heidelberg-laureate-forum.org/blog/video/lecture...
By the end of your BSc in the analogy, you can look at a sentence and recognise at least what sort of genre it might be part of, and you can write down many of the most common words as well as a number of rehearsed useful sentences.
An MSc is like reading some examples of long sentences and short paragraphs, and being shown some long paragraphs or even chapters of books (which you have no hope of understanding, but you try, and the experience is salutary). If you're lucky, you did a research project in which you perhaps rewrote a certain very specific short paragraph in your own words.
The job of a research mathematician is analogously then to read and write books.
Well stated. this pretty accurately characterises my experience of undergraduate studies & an honours year in mathematics
Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.
The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books).
Most of the time, the point of proofs isn't to establish something is true, but to communicate something about the internal structure of a piece of mathematics.
The problem with Mochizuki is that he did his work isolated from the rest of the world, so the internal structure of the kind of maths he invented is opaque. Accordingly, what mathematicians are really trying to do is to examine what makes this new maths tick; the books that make this accessible to mathematicians worldwide will not be fully-verifiable proofs of a statement, but webs of separate propositions whose statements are illuminating and whose proofs are easy to understand. If they're really successful, some may even be left as an exercise to the reader.
Automated proofs by contrast really are proofs but as many of these comments show are not arguments.
So maybe the problem to be solved is to appropriately connect mathematical arguments (what mathematicians call proofs) to proofs, while recognizing that they are actually two entirely separate families -- as different as plants and animals.
To extent that mathematics is a science, the whole point is to understand. Of course, people time and again have succumbed to the feeling that (e.g.) numbers are divine, but there's nothing mathematical about that.
---
It's not like it has been established as a mathematical theorem based on simpler ontological facts that capital-T truth exists. And everything in our daily experience points out to the contrary.
That fact that computers and programming languages have evolved from XOR and NAND semiconductors says a lot about the power of a particular branch of mathematics; it says nothing about the nature of mathematics. That idea is like claiming that the existence of probability theory implies that mathematics is about reasoning with uncertainties.
The thing is that mathematic proofs work on different levels of "zoom", ranging from just stating "it follows trivially" to formal proofs. And this is a normal process, that's how Mathematicians boil down long proofs to simple lines of reasoning.
I think what happens here I that the author of the original proof is arguing on a high "it's obvious" level and seems to be unwilling to go into detail.
[1]https://medium.com/@nutanc/the-final-and-exhaustive-proof-of...
[0]: https://empslocal.ex.ac.uk/people/staff/mrwatkin//zeta/RHpro...
That said, I’d be happy to go over this as an analytic number theorist rfurman@alumni.stanford.edu
This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and proofs can be improved. Tools for each can be developed without having to support both.
IMO the only advantage to be gained by introducing physical computers in the picture is lightning-fast book keeping.
Why would you trust an Intel CPU, a Samsung SSD and a linux fs driver running some verifying framework more than the human brains designing, writing and executing said framework?
The question of formally proving Wiles' theorem is [discussed here](http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html). Currently there exists no tool powerful enough to formalize such proof. It's considered a challenging problem in computer science.
They have been the foundation of hundreds of Phd projects and the scientific merit and public fame to be gained by finding a gap in the argument is clear.
Actually I think breakthrough papers are least problematic when it comes to unverified claims in math.
Seemingly "evident" result, extremely difficult to prove in some cases (e.g. continuous, nowhere differentiable function etc.)
At this point, it seems clear that we do not have a proof of the ABC conjecture. Perhaps someone will be able to improve this to make a real proof - after all, there were some errors in the first Wiles proof of Fermat's Last Theorem, but they ended up being minor errors that were fixed up once they were found. But what we have is not a proof.
I was given to understand that his work was more like Grothendieck's, where he's developing this entirely new, super general system. But you can imagine if Grothendieck for example had done all of his work for years and years in isolation and then presented Schemes, Topoi, and Motives to everyone all at once, using them in combination to prove something familiar, and expecting other mathematicians to just learn and understand them all in order to verify a single proof.
I think in that case, folks would not have been immediately so interested in the new constructions Grothendieck had come up, viewing it initially as mountains of unnecessarily alien concepts built up just to give other mathematicians a hard time ;)
(Not to identify the two mathematicians overly—I'm not sure how appropriate that really is—but I remember that being my impression when first digging into Mochizuki's work, and I haven't seen it mentioned here yet.)
It's not sufficient to have a great idea, or even to be right about it. You have to be able to explain it thoroughly enough that other qualified peers can understand your logic enough to weigh in on it. That seems not to have happened yet hear.
This sounds like a variant of the Turing test.
Mochizuki and your pet dog both claim to have proven the ABC conjecture. The ABC conjecture has been proven when you can understand one proof but not the other.
Mochizuki and your pet dog both claim to have proven the ABC conjecture. The ABC conjecture has been proven when you can tell the difference between the two proofs.
Is this normal in advanced Math or is this guy kind of a jerk?
But anyway, mathematics is not any more unhealthy than any other field, but it does have toxicity like all others do as well.
I never went deep enough into mathematical academia to judge, let alone getting into other fields to allow for a comparison.
Terence Tao and Peter Scholze (and others) join the discussion in the comments section.
>It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
Likely such is the understatement-ish way of a mathematician to say "This is clearly wrong, but I have not the time to dig in and find where exactly"
It's possible to write structurally reusable components that are useless, i.e. they do a thing that no one wants or needs.
This is a statement of "If this thing has no other application, it isn't worth my time to dig through what is likely an impenetrable pile of garbage."
Basically, proof of the abc conjecture should have a bunch of follow on consequences. If those aren't materializing, that makes taking the time to understand the proof quite a bit less enticing (ie. the Bayesian prior on "true" goes down a lot).
Important conjecture like ABC expressess some fundamental feature in the field. It's not just a arbitrary brainteaser. How to solve this one problem should give insights to many related problems.
Thought experiment:
Imagine a modern mathematician/time traveller who want's to impress Carl Friedrich Gauss by solving problems CFG can't solve, but at the same time the not wanting to give away any clues to modern mathematics. Traveler would need to devise complex and convoluted ways to proof things. Proofs would probably piss off GFG more than impress him.
Honestly I am surprised of hearing such an argument from one of the world's best mathematicians.
A plausibility argument like Tao’s one is simply not an argument.
To show that Mochizuchi is wrong you need to point out which equation of his work is wrong, which by the way is Peter Scholze’s plan.
Tao by his own admission does not have the background to evaluate Mochizuchi’s theory and still gives this worthless plausibility argument, appealing to his knowledge of other unrelated proofs. I’m astonished.
As a scientist I would never make such a statement, moreso for a theory I admittedly don't understand.
Tangentially, it's not Tao's case, but I have seen a lot of bullying in the academia along these lines... "I am not saying it's wrong, just very bizzarre", "I am not saying it's wrong, but my Ph.D. student worked on it for two years and couldn't solve it", "I am not saying it's wrong, actually I don't even understand the details, but please recheck everything..." etc...
In mathematics there’s absolutely no place for judging the bizarreness of statements, either they are right or wrong, and of course such a judgement cannot be made by someone who admittedly doesn’t have the necessary background.
As I already said, often in the Academia saying that a result is bizarre is a not-so-subtle way of implying something is wrong by appealing to authority.
I can kind of see that, but there's something in it that gives me the feeling of arbitrariness.
It's looking at the relationship between prime factors of A, B, C in A + B = C, where no prime factors may be shared between A, B, or C. The specific relationship in question is between the magnitude of C and the unique prime factors of A, B, and C multiplied together.
To take an example from the article, 5 + 16 = 21 meets the basic requirements since the prime decomposition looks like (5) + (2 * 2 * 2 * 2) = (7 * 3) —no factors are shared. But, the quantity we're supposed to relate to C is (5 * 2 * 7 * 3), since it is the product only of the unique primes.
Does that not feel arbitrary, to drop the repetitions? So it ends up being that the sought out smaller products arise because they had large numbers of repetitions, so we removed more when forming the product.
But I suppose there are probably just some deep number theory mysteries behind it which give justification, so it only feels arbitrary to someone like myself who is basically ignorant on the subject :)
If the conjecture turns out to be true, then that apparently arbitrary step turns out to be meaningful, because it uncovers a hidden relationship between the numbers A, B and C and their factors.
The prime factorization of a number is essentially "random". That makes numbers that are large powers of primes rare; it's like rolling a die and continuously getting the same face. Now if you add two numbers, the prime factorization of the sum does not appear to be related to the prime factorization of the summands, so adding two very rare numbers and getting yet another very rare number seems unlikely. And that seems to be roughly what the abc conjecture says: it is not likely that all of a, b, and c are rare.
So rad(8) = 2, rad(24) = 6, rad(75) = 15
> And that seems to be roughly what the abc conjecture says: it is not likely that all of a, b, and c are rare.
It almost sounds like a tautology. Is your view that it is somewhat vacuous after all? Or maybe the interest comes from the fact that while it seems obviously true, we need a proof in order to use it as a theorem for other things where it would be a useful tool...
The justification I gave depends on an intuition that addition "scrambles" prime factorizations, ie. except for common factors, which obviously pass through to the sum, the prime factorization looks random. Understanding how prime factorizations behave under addition is certainly not an easy problem. And then, even if it is unlikely that a, b, and c are all rare, perhaps it is not unlikely in precisely the quantitative way that the abc conjecture supposes.
On the topic of things where it is a useful tool: I found http://www.ams.org/notices/200210/fea-granville.pdf which discusses its relation to other famous results but which also has a much better argument for why it should be true. They approach it as the integer analogue of this result for polynomials
> If a(t), b(t), c(t) ∈ C[t] do not have any common roots and provide a genuine polynomial solution to a(t) + b(t) = c(t), then the maximum of the degrees of a(t), b(t), c(t) is less than the number of distinct roots of a(t) b(t) c(t) = 0.
I particularly enjoyed the link to Dr. Calegari's blog post, as it was interesting to read the comments in 'real time' and compare that with the author's synthesis. Very good article!
The really hard part (and main part of Wile's contribution to the proof) was proving something called the Taniyama–Shimura–Weil conjecture. However if you skip that bit and just accept that the conjecture is true the rest of the steps of the proof are both elegant and relatively easy to follow (if you gloss over some of the details) for anybody with a decent grasp of basic math.
The book Fermat's Last Theorem by Simon Singh is a pretty great read and does a good job of outlining the basic structure of the proof for anybody with a decent grasp of high school mat.
Apart from that, the article makes me curious about the state of automated mathematical proof. I remember having read an article posted here about a mathematician (I think he was a Field medalist) who was claiming that automated proof were the future of mathematics as they would enable mathematicians to collaborate much more easily, removing problems of trust in others' proof.
Older threads for reference:
https://news.ycombinator.com/item?id=15971802
https://news.ycombinator.com/item?id=4502856
https://mathoverflow.net/questions/106560/philosophy-behind-mochizukis-work-on-the-abc-conjectureThe language of math has always been much more mushy than mathematicians are willing to concede, and the chickens are coming to roost: 21s century math has become so complex and sophisticated that very few people can actually even read the content of proofs, much less understand them.
Shinozuki's case is an extreme example of that: after almost ten years, even he other experts in the field aren't sure of what he's saying.
There is a clear need for formalizing the language of mathematics in a way that allows machine to verify he validity of a proof.
https://en.wikipedia.org/wiki/Shinichi_Mochizuki
About Hoshi, I have seen him in a conference video before, and have an impression that he isn't good at English, which can make a bit difficult in discussion.
I don't know about Scholze and Stix.
We have lots of examples of good writing in math from Bourbaki, W. Rudin, P. Halmos, H. Royden, and more.
Sorry 'bout that: No one wants math to miss out on a great, new result, but the writer has to do their job first, in particular, do good math writing.
> Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.”
This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.
>One final point: I get very annoyed by all references to computer-verification (that came up not on this blog, but elsewhere on the internet in discussions of Mochizuki’s work). The computer will not be able to make sense of this step either. The comparison to the Kepler conjecture, say, is entirely misguided: In that case, the general strategy was clear, but it was unclear whether every single case had been taken care of. Here, there is no case at all, just the claim “And now the result follows”.
What does that mean, then? That a leap is being made that depends on the reader's fuzzy intuitions, rather than the established axioms? If that's the case, it's not a formal proof at all, no?
Or am I way off here?
He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“
But it can. You need to have the computer 'comprehend' the relevant axioms, of course.
If your 'proof' is in fact just arguing the case for new axioms, that isn't a proof at all, it's a misunderstanding of what 'axiom' means. (They're definitions, not profound universal truths.)
> Any proof that can be spelled out at a level of detail sufficient to be analyzed by a computer is necessarily going to consist entirely of steps that are each completely comprehensible to a mathematician.
This means there must either be a lot of steps or a lot of different paths to follow in order for a computer to be of use. Neither is the case here.
Here Scholze is saying that part of the proof simply hasn't been written, so there's nothing to verify. I think he's missing that computer verification proponents are also aware of that and are either
1. trying to motivate the camp that claims to understand Mochizuki's work to formalize and computer-verify it
and/or
2. suggesting that some of the gaps can be filled in by automatic theorem provers
The problem is that these papers are vague. The translation to computerized version would be a very different thing, it'd require a lot of creative writing on behalf of the translator.
For TL;DR see around page 40 in that PDF:
> Indeed, at numerous points in the March discussions, I was often tempted to issue a response of the following form to various assertions of SS (but typically refrained from doing so!): Yes! Yes! Of course, I completely agree that the theory that you are discussing is completely absurd and meaningless, but that theory is com- pletely different from IUTch!
> Nevertheless, the March discussions were productive in the sense that they yielded a valuable first glimpse at the mathematical content of the misunderstandings that underlie criticism of IUTch (cf. the discussion of § 3). In the present report, we considered various possible causes for these misunderstandings , namely:
> (PCM1) lack of sufficient time to reflect deeply on the mathematics under discussion (cf. the discussion in the final portions of § 2, § 10);
> (PCM2) communication issues and related procedural irregularities (cf. (T6), (T7), (T8));
> (PCM3) a deep sense of discomfort ,or unfamiliarity ,with new ways of thinking about familiar mathematical objects (cf. the discussion of § 16; [Rpt2014], (T2); [Fsk], § 3.3).
> On the other hand, the March discussions were, unfortunately, by no means sufficient to yield a complete elucidation of the logical structure of the causes underlying the misunderstandings summarized in § 17.
>It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
so it's not so much that the main result is called into question but there are some useful and workable bits left over. Rather the main result is called into question because there are no other useful and workable bits.