12 ms·
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematic
by salty_biscuits 8y ago
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
- vbezhenar 8y agoI don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that proof.
- _Microft 8y agoSome mathematicians are concerned that the possibility of an error in a computer program or a run-time error in its calculations calls the validity of such computer-assisted proofs into question. (This might be one reason, from https://en.wikipedia.org/wiki/Mathematical_proof#Computer-assisted_proofs https://en.wikipedia.org/wiki/Mathematical_proof#Computer-as... )
- fjsolwmv 8y agoThat's silly, because humans have been repeatedly proven to be full of errors.
- salty_biscuits 8y agoIt is actually surprisingly fussy to set up a formal proof for anything complex enough to be interesting to a mathematician (for computer assisted verification). People take big leaps that are often quite awful to actually prove. I think you are right though, this area will definitely be very important and make big strides.
- deleted 8y ago[deleted]
- mehrdadn 8y agoEdit: never mind, it seems I confused deriving a proof with verifying it!
- danharaj 8y ago> Mathematics is very strict science with axioms and following theorems. 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.
- mrob 8y agoWhy can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.
- wtallis 8y agoI participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to typeset proofs that embed metadata about which lines are the key steps and which could be folded. This is probably influenced by the fact that LaTeX doesn't support this kind of semantic markup and it would be awkward to add.
- yesenadam 8y agopeople with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?
- wtallis 8y agoNah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.
- bollu 8y agoIf you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson theorem), you'll realise just how painful it is --- I speak as someone who's done this for fun (and now for research. [my report is available here](https://github.com/bollu/dependence-analysis-coq/blob/master/report-independent-study/independent-study.pdf) https://github.com/bollu/dependence-analysis-coq/blob/master...)
- noisem4ker 8y agohttps://github.com/bollu/dependence-analysis-coq/blob/master/report-independent-study/independent-study.pdf https://github.com/bollu/dependence-analysis-coq/blob/master... Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.
- WalterGR 8y agoIf you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is 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?
- patrickthebold 8y agoImagine convincing someone that a web service could be written, vs getting it written and deployed to production. And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...
- darkmighty 8y ago> What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful? 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.
- nabla9 8y agoFormal proof assistants and interactive theorem prover for mathematics already exist. So do proof libraries. See: http://metamath.org/ http://metamath.org/ 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.
- kiriakasis 8y agoAlso I want to add syntax, mathematical syntax is incredibly rich, complex, ambiguous and effective; so much that in some paper it is the hardest part to understand, not always because of bad writing. At least we are better off than theoretical physicists :-)
- andrepd 8y agoYou don't understand because you haven't looked into it very much :) You'll find that automated theorem proving and proof verification is far from trivial. State of the art tools are still very cumbersome and verbose to use and are infeasible to use in those problems where you need them the most.
- naasking 8y agoBecause most mathematics is not constructive, and most automated theorem proving tools are based on constructive logic.
- dwheeler 8y agoThere are number of proof verification systems that do not require constructive logic. So if you require classical logic, just use a tool that supports it.
- fjsolwmv 8y agoThat doesn't sound right at all. Law of excluded middle is very easily computed with, It's a college homework exercise.
- kiriakasis 8y agoWell, yes because you can embed classical logic in constructive logic in many ways but then you lose a lot of convenience. The if you had exensionality things get really weird
- Kutta 8y agoThat's irrelevant, all mainstream proof assistants are compatible with classical logic.
- Angostura 8y agoWouldn;t it bump into the same kind of problems that Bertrand Russell's attempts bumped into with the Principia Mathematica? Namely it crashed into Gödel's incomplete theorem? Disclaimer: What I don't know bout maths would fill volumes, in both senses of the word Edit: From the down-votes, apparently not.
- mrob 8y agoHuman mathematicians are bound by Gödel's theorem in exactly the same way computer software is. If an informal human-based "proof" does something that would be impossible with a formal software-based proof, then it's incorrect. There is no theoretical advantage to running the calculations on a human brain.
- Angostura 8y agoSorry, I didn’t intend to suggest that running a proof on wetware had advantages. Simply that running complete, from first principal proofs were doomed to failure
- dan-robertson 8y agoThere’s this curious thing in mathematics where most things are either obviously true or obviously false and those that aren’t are mostly inconsequential. Those that remain are certainly more interesting but also typically their proofs are a few obvious steps. 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.
- Moodles 8y agoSome fun large counterexamples to conjectures: https://math.stackexchange.com/questions/514/conjectures-that-have-been-disproved-with-extremely-large-counterexamples https://math.stackexchange.com/questions/514/conjectures-tha... So maybe Fermat's Last Theorem etc isn't always obviously true. But I do get your point.
- deleted 8y ago[deleted]
- ChrisRackauckas 8y agoA lot of areas like real/stochastic analysis are really difficult to map to any formal proving mechanism. Really there are only some areas in abstract algebra where it can be done, and in there you still need some proofs that link a set of real problems to a computable problem and finish with the computation (Groebner basis proofs are one example). But that's rare.
- nixpulvis 8y agoWho proves that the automated proof is correct. Who proves that... etc. All this is tied up in Gödel's incompleteness theorem.
- dwheeler 8y agoVerifying proofs is a much simpler job than creating a proof. Also, you can have multiple independently implemented verifiers, which act in many ways like multiple human reviewers. That is what the metamath community does, they have 4 independently implemented verifiers that check every proof. That is very strong evidence that a proof is correct, far stronger evidence than is typically accepted now.
- nixpulvis 8y agoYes but these will only accept proofs from within the mathematical framework of the multiple verifiers. I'm not saying that having 4 automatic independent verifications of a proof is useless, far from it! Just that, the notion you can "prove" all of mathematics is almost meaningless, or demonstrable false.
- dwheeler 8y agoI'm not sure what your point is here. If the point is that the provers require a particular format, and not just English sentences, then that is true but not really a problem. Writing programs also requires that you use a particular format, AKA programming language, and that happens all the time. 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.
- nixpulvis 8y ago
- stepvhen 8y agoWell, first, use a logic programming language and report back. Then understand that math is almost wholly non-empirical. The things discovered or made up in math are not reflective of the real world, most of the time, regardless of how closely it resembles. 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.
- throwawaymath 8y ago> Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. 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."
- karmakaze 8y agoAs dweller says below, I'll rephrase it here. Godel's incompleteness theorem proves that with any axiomatic system there are statements which are true but are absolutely not provable within the system. Godel, Escher, Bach is a beautiful read for this.
- lacker 8y agoI don't really understand why the entire known mathematics is not automatically proven yet. 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.
- mrob 8y agoFormal proofs increase trust in mathematics. E.g. Fermat's Last Theorem is supposedly true, but I can't understand the proof. I have to trust the mathematicians who say the proof is correct, and I know that in other fields (most notably with the replication crisis in psychology) people accepted things as true when they weren't. If I had a formal proof I could run it through a theorem checker and see that it was correct, and I could use multiple independent implementations of the theorem checker for more confidence. If I'm using human mathematicians as black-box theorem checkers, I don't have the option of using multiple independent implementations, because all mathematicians work with other mathematicians, so it's possible that they're just agreeing with each other's mistakes. With the software I also have the option of examining how it works, all the way down to transistor level if I want to.
- lacker 8y agoBut who is demanding this sort of increased trust in abstract mathematics? Mathematicians don't seem to be demanding it, as this sort of work/research is not in high demand for publications. Non-mathematicians don't seem to be demanding it, because this sort of mathematics doesn't yet have much application outside of mathematics.
- paulddraper 8y agoI don't understand why the entire known software corpus is not automatically proven yet. Computation is a very strict process. I'm not talking about a computer writing code itself, but a programmer should write programs using some formal language and the computer should be able to follow the proof. I.e. no bugs. /s