17 ms·

Number theorist fears many proofs widely considered to be true are wrong

87 points by lelf 7y ago

MrBuddyCasino 7y ago
Soo... Unit testing / CI for math proofs? If it can be done in software, great.
- std_throwaway 7y ago
  To my knowledge the hard part is writing the input for the software. While in text you have a bit of leeway to glance over some details, with the computer program you must, indeed, write every last relevant detail down and you must get it right. This is very heavy work.
  - ukj 7y ago
    But it's once-off work. Thereafter the computers can take over.
- jeff_friesen 7y ago
  I was thinking it's a lot like property-based testing
- jetzzz 7y ago
  It's actually type checking. Per the Curry–Howard correspondence, proof checking is equivalent to type checking, just for much more sophisticated type system than in an ordinary programming language.
adamnemecek 7y ago
Vice really does a disservice to the author. "All" math is not wrong, but I sure wish theorem provers were the preferred method of formalizing mathematics. But theorem provers really aren't quite ready for prime time either. But it sure feels like a lot of verification of mathematics is somewhat repetitive. I think that programming/CS is to mathematics what neolithic revolution was to human culture. It allows for specialization in the stack. People can obsessively optimize different parts of the stack to everyones benefit.
gowld 7y ago
Headline is of course absurd hyperbole that does not belong here. > "I think there is a non-zero chance that some of our great castles are built on sand," Buzzard wrote in a slide presentation. "But I think it's small."
- mirimir 7y ago
  Yes, the title ought to be changed. At least, "all" to "some". But he does note: > This overreliance on the elders leads to a brittleness in the understanding of truth. A proof of Fermat's Last Theorem, proposed in 1637 and once considered by the Guinness Book of World Records to be the world's "most difficult math problem," was published in the 1990s. Buzzard posits that no one actually completely understands it, or knows whether it's true.
- kurlberg 7y ago
  Well, they also quote him as saying: "I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,”
  - kevinzz 7y ago
    https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...
std_throwaway 7y ago
There is a big grey area between "not 100% correct" and "wrong and harmful". Like a faulty computer program that produces correct results in 99.999% of the cases a wrong mathematical statement can still yield useful results in practice. You just don't want to run into those pesky edge cases where it indeed is wrong. Having a database of all mathematical proofs where all of them are checked for validity, however, is a very useful tool to actually find those edge cases where a proof is wrong and give future mathematicians a solid foundation. Using AI as an extension of human capabilities is a given to me. Like with heavy machinery, we don't want to do the heavy lifting. We want to steer it properly to gain most benefit.
- cyphar 7y ago
  > a wrong mathematical statement can still yield useful results in practice Yes and no. For some basic conjectures this might be the case, but one of the greatest utilities of certain theorems is how they can be applied to completely new fields. If a theorem used in this manner is not actually true, then the proof is invalid -- and it might be the case that (several proofs down the line) the conjecture you've ended up proving is almost entirely invalid. There's also the slippery slope of "Principle of Explosion"-type problems with accepting "mostly right" proofs -- it means you will be able to prove any given statement (even ones which are outright false).
ukj 7y ago
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project. [1] https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq [2] https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath
- krapht 7y ago
  Well, having used both, Lean really is a lot more ergonomic. Unimath is mostly category theory; other parts of mathematics are woefully underdeveloped.
  - ukj 7y ago
    That's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never written human-computer interfaces before. When it comes to adapting humans to Mathematics, or adapting Mathematics to humans - I prefer the latter.
Hasz 7y ago
Headline is waaaay overblown, but not all of it is total hyperbole -- checkout out arxiv and try to read the abstract from just about any paper. It's basically totally impermeable. I'm almost done with an undergraduate degree in math and basically have no idea what ~90% of the research is about at anything other than a topical level. This is fine, it's written for specialists in the field (hopefully), but damn, for most fields, it's not a whole lot of people. Compared to physics or chemistry, math gets very specialized, very quickly. Depending on the field, there's no easy real world isomorphisms either, making it even more difficult.
- hgtr 7y ago
  I did some undergraduate research and ended up getting published. My initial drafts were written with prose so that I (and hopefully any novice) could understand. However, my professor wasn’t happy with it so I got some help from one of his grad students to re-write it. By the end of it I could barely understand my own paper. IMO the final paper had too much technical jargon which was convoluting some simple concepts. Kinda made me disenchanted with the academic world. Still have to give credit to my prof and the grad student, without their edits it probably wouldn’t have been published.
  - echelon 7y ago
    This is one of the reasons why I pursued engineering instead of a hard science. Mathematics in particular feels like an ivory tower with a bunch of gatekeeping. Better language and grammar around core concepts could improve accessibility, but few in the field that I've encountered seem to care about that. Biology and chemistry are a bit better, but there are still improvements that could be made. You can't easily go from zero to biochem or ochem, and I don't think that has to be the case. Gen chem and gen bio just suck at presenting themes and concepts and instead focus on being a smorgasbord of facts (that you later have to amend or unlearn). Computer science and electrical engineering are a walk in the park by comparison. We have all sorts of interactive tools and visualizations of algorithms and analysis. We keep refining and making the onboarding process easier and more accessible.
breck 7y ago
Anyone interested in this topic, I have a prediction that the time is right for a new math, that starts from just 1 and 0, and builds every symbol up in a rigorous way. We're working on the infrastructure to make such a thing easier, but the project does not currently have a leader: https://github.com/treenotation/jtree/issues/83 https://github.com/treenotation/jtree/issues/83
- devicetray0 7y ago
  Forgive me, but why is the TreeNotation/jtree library the right place to craft a new "rigorous" mathematics language?
  - breck 7y ago
    It’s a good question. This paper hints at the reason: https://github.com/treenotation/jtree/blob/master/papers/paper3/countingComplexity.pdf https://github.com/treenotation/jtree/blob/master/papers/pap... First, jtree is a bit orthogonal as that’s just an implementation. The github issue is there for convenience, it’s arbitrary. The reason for tree notation is that it’s a level up from binary. Binary notation does not give you the ability to define new symbols. Tree notation is a 2d binary. You can define new abstractions. It is a bridge between human and machine languages. Take any concept in mathematics, such as “derivative”. How would you define such a concept, starting only from 1s and 0s? Tree notation gives you a method to do that, in a way that’s not only efficient (noiseless), but also gives you practical tools, like complexity counting.
- lidHanteyk 7y ago
  Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf
  - breck 7y ago
    Very interesting, thanks! This is definitely along the lines of what I’m thinking. It uses EBNF, i think if we switched it to tree notation it would be much, simpler, tighter, and more self contained.
lysium 7y ago
I’m sure this will help proofing papers. There will still be the problem of proofing that the software proofs what it is intended to proof.
ummonk 7y ago
Extreme clickbait headline. The subheading is '"I think there is a non-zero chance that some of our great castles are built on sand," he said, arguing that we must begin to rely on AI to verify proofs.'
- asaph 7y ago
  But, more consistent with the alarmist headline: > “I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk.
  - parsimo2010 7y ago
    Someone who says that is, ironically, not concerned with the details. All of published math is wrong? No, a lot of is is understandable and verifiable by advanced undergraduates. Most of the fundamental theorems in each field are understandable by humans. As you get more and more abstract, and get into more and more obscure areas, you start to see non-understandable proofs built on top of non-understandable proofs. There's a danger that those are wrong, but when they collapse it just means that one professor has wasted their life, not that all of mathematics will suddenly collapse.
    - kevinzz 7y ago
      The headline is clickbait. A more measured debate about the issues is here https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...
- dang 7y ago
  We've replaced that with a more measured sentence from the article, in accordance with the HN guidelines ("Please use the original title, unless it is misleading or linkbait") https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
colorincorrect 7y ago
This short pdf which the article cites is more useful than anything the article itself contains: http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf
- enjoyyourlife 7y ago
  Discussion: https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404
iamaelephant 7y ago
This just seems like a native advertisement for Lean...
- DoctorOetker 7y ago
  I am not that perturbed by whatever framework they use, tools to translate the bulk of the majority of proofs from Lean to MetaMath to [...] and back will be made, the more important thing is that the number of humans aware of the existence of this tech and the more actually use it the better society will be off in the long run the following may seem totally impossible today but seems a lot less impossible to people who have been thinking about this for a long time: once sufficient mathematics has been translated, people can start adding physics postulates, one most physics has been inserted we can start formally verifying (up to validity of postulates on top of axioms) not just proper operation of digital circuits etc but also power plants and so on, and once interacting with proof systems becomes as widespread as alphabetic literacy, people might one day be able to formalize and vote on their requirements of society and policy, see predicted perverse incentives, or decide that policy can only be enacted when facets of their consequences can be proven. We might one day not vote on promises of strategy, also not vote on strategy, but rather on outcomes! I know it sounds absurd.
Ceezy 7y ago
"I believe that no human, alive or dead, knows all the details of the proof of Fermat’s Last Theorem. But the community accept the proof nonetheless," Buzzard wrote in a slide presentation[...] That s 100% clickbait. People knows the demonstration and the demonstration helped to create entire new fields. By the way there are new and shorter proof of the theorem.
- hyperbovine 7y ago
  Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.
  - foooobar 7y ago
    Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".
  - repolfx 7y ago
    I think the intended implication is that Wiles has not read or understood all of the proofs he built on. If someone said, "nobody dead or alive understands all the details of Windows" I doubt anyone here would find it controversial. It's too big to fit in one person's head.
  - Stasis5001 7y ago
    Sure, Wiles obviously understands the main thrust of his proof. But one could argue that Wiles' result depends on lots of other results, which in turn depend on other results, and so on through decades and decades of work, ultimately going back to the foundations of mathematics. Neither Wiles nor anybody else can claim to rigorously understand all of it. You can imagine this as a tree, with Wiles' work as root, and his dependencies as ancestors, and so on. An error at a lower level of the tree could, in theory, invalidate the root node. I do agree with Buzzard that it's hard to be sure. I've definitely read papers where a critical argument isn't well written or what is written seems wrong. However, if there are low-level errors, I suspect that with some work things could be patched up.
madez 7y ago
I'm currently working on the formalization of Catalan's conjecture (or Mihăilescu's theorem) in Isabelle/HOL/Isar. My personal impression is that more formal verification is necessary in math, and it should be tought to every student of Mathematics in introductionary courses because it gives an unforgiving but also rewarding learning experience with formal proofs. Feel free to ask questions.
- joker3 7y ago
  How much research is being done on making these tools more user friendly? I spent a little bit of time using Coq about a decade ago, and while I agree that it's very important to make things like that widely used, there was a pretty steep learning curve.
  - madez 7y ago
    I can't answer how much research or work is done to make the tools more user-friendly as I'm rather exclusively on the user-side. There exists extensive documentation in form of multiple PDFs, but they are only of little help to me as they lack useful examples. Sadly Google thinks every possible answer about Isabelle/HOL is answered by these PDFs as they are often the only relevant search result. However, Isabelle/HOL/Isar allows proofs to be written in a very human readable way, so the "documentation" I use is the existing library and how things are done there. There is a convenient Ctrl+left click action on terms to jump to their definition. That is very helpful to navigate unknown libraries. In comparison, I couldn't read and make sense the proofs I've seen in Coq. There is a learning curve with Isabelle/HOL/Isar. It can be extremely frustrating to not know how to express "simple" arguments or definition. But for someone familiar with manual "formal" proofs in mathematics, most can be learned in some hours under guidance, like in a seminar on a weekend with a couple of hours on each day. I'm learning rather autodidactly by trial and error. I think there would be value in a series of blog posts about "This is how you define a group" or "This is how you reason in nonclassical logic" or "This is how to proof the fundamental theorem of Algebra" all applied to Isabelle/HOL/Isar. There are often multiple ways to define things, and to be honest, I don't know the specific advantages and disadvantages. For example, I think you can introduce rings as type classes or as locales or using axiomatizations, and possibly more. This is one example of stuff I don't know how to manage in the system, but there is already a lot of structure defined, and I can reuse that.
higherkinded 7y ago
Suggestion to rely on AI for proof verification is just laughable. Neuron weights instead of formal definitions. So reliable.
- drchewbacca 7y ago
  It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail. Here is an example. https://arxiv.org/pdf/1608.02644.pdf https://arxiv.org/pdf/1608.02644.pdf
- 6gvONxR4sf7o 7y ago
  That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier. Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.
- not2b 7y ago
  You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.
  - higherkinded 7y ago
    Okay but they are formal systems and don't have anything to do with AI either, do they?
- YeGoblynQueenne 7y ago
  Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation. https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant This is Good Old-Fashioned AI, through and through.
bryanrasmussen 7y ago
I just can't help feeling that either the true should be correct, or the wrong should be false. But I guess English is not a strongly typed language.
raymondh 7y ago
Summary: Motherboard interviewed an attendee at the Interactive Theorem Proving conference who says that he thinks Interactive Theorem Proving is important. Also, professors specializing in proof theory think their tooling may become important but "the technology still needs improvement".
dls2016 7y ago
I had these fears about my dissertation work, but then realized that the “elder’s” papers were highly cited because they contained important machinery which could be modified and refined to prove other results... or the paper contained an important idea which went on to be proved in a variety of ways. Maybe it’s different outside of PDEs, but I doubt it.
repolfx 7y ago
To mathematicians, Welcome to our world! https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Actually working through some of [the details], when formalising them, made me understand that some of these issues were far bigger and more complex than I had realised. In the perfectoid project there is still an issue regarding the topology on an adic space, which I had assumed would be all over within about a page or two of pdf, but whose actual proof goes on for much longer Yeah, that's how software developers feel, all day, every day. That's why we all moan about being asked to give estimates for things. You don't really understand a thing until you've formalised it in code, and often things that look simple and easy turn out to be unexpectedly deep. Mathematics is a field that's been doing the equivalent of writing pseudo-code for thousands of years. There are endless reams of pseudo-code that looks like it might work, but as any programmer who's ever written pseudo-code knows, whether it actually runs when you try it out for real is anyone's guess. So now mathematics is starting to experience the pain of multiple incompatible programming languages/ecosystems. There's Lean, Coq, Isabelle/HOL and some new JetBrains language too. Soon they'll start to discover the value of 'foreign language interop', rigorous code review, comments, style guides, design documents, package management, automatic optimisation etc. Have you ever looked at a proof written in one of these languages? All code in these languages is a hot mess judged by the standards of professional software developers: tons of abbreviations, single letter variables, uncommented, ad-hoc module structure etc. I'm sure we'll eventually see mathematicians having raging flamewars about what clean style is and tabs vs spaces. Luckily for mathematicians though they work at their own pace and are under no deadline pressure. They'll figure it out.
joker3 7y ago
The headline is certainly overblown, but there probably errors out there. The interesting question is where we should be looking for them. All of the major results in an undergraduate or introductory graduate textbook have been studied often and thoroughly enough that we can be reasonably confident there are no errors in their proofs. There are errors in very new or very obscure material, but those tend to get corrected as more people start paying attention to them. It therefore seems like the search should therefore be concentrated in recent results that are becoming more useful but still aren't standard. On the other hand, we do need to build a standard library of results that can be used to prove those newer results. You can't do much in analysis without basic results on metric spaces, for instance.

87 points by lelf 7y ago

MrBuddyCasino 7y ago

Soo... Unit testing / CI for math proofs? If it can be done in software, great.

std_throwaway 7y ago
To my knowledge the hard part is writing the input for the software. While in text you have a bit of leeway to glance over some details, with the computer program you must, indeed, write every last relevant detail down and you must get it right. This is very heavy work.
- ukj 7y ago
  But it's once-off work. Thereafter the computers can take over.
jeff_friesen 7y ago
I was thinking it's a lot like property-based testing
jetzzz 7y ago
It's actually type checking. Per the Curry–Howard correspondence, proof checking is equivalent to type checking, just for much more sophisticated type system than in an ordinary programming language.

adamnemecek 7y ago

Vice really does a disservice to the author. "All" math is not wrong, but I sure wish theorem provers were the preferred method of formalizing mathematics. But theorem provers really aren't quite ready for prime time either. But it sure feels like a lot of verification of mathematics is somewhat repetitive. I think that programming/CS is to mathematics what neolithic revolution was to human culture. It allows for specialization in the stack. People can obsessively optimize different parts of the stack to everyones benefit.

gowld 7y ago

Headline is of course absurd hyperbole that does not belong here. > "I think there is a non-zero chance that some of our great castles are built on sand," Buzzard wrote in a slide presentation. "But I think it's small."

mirimir 7y ago
Yes, the title ought to be changed. At least, "all" to "some". But he does note: > This overreliance on the elders leads to a brittleness in the understanding of truth. A proof of Fermat's Last Theorem, proposed in 1637 and once considered by the Guinness Book of World Records to be the world's "most difficult math problem," was published in the 1990s. Buzzard posits that no one actually completely understands it, or knows whether it's true.
kurlberg 7y ago
Well, they also quote him as saying: "I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,”
- kevinzz 7y ago
  https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...

std_throwaway 7y ago

There is a big grey area between "not 100% correct" and "wrong and harmful". Like a faulty computer program that produces correct results in 99.999% of the cases a wrong mathematical statement can still yield useful results in practice. You just don't want to run into those pesky edge cases where it indeed is wrong. Having a database of all mathematical proofs where all of them are checked for validity, however, is a very useful tool to actually find those edge cases where a proof is wrong and give future mathematicians a solid foundation. Using AI as an extension of human capabilities is a given to me. Like with heavy machinery, we don't want to do the heavy lifting. We want to steer it properly to gain most benefit.

cyphar 7y ago
> a wrong mathematical statement can still yield useful results in practice Yes and no. For some basic conjectures this might be the case, but one of the greatest utilities of certain theorems is how they can be applied to completely new fields. If a theorem used in this manner is not actually true, then the proof is invalid -- and it might be the case that (several proofs down the line) the conjecture you've ended up proving is almost entirely invalid. There's also the slippery slope of "Principle of Explosion"-type problems with accepting "mostly right" proofs -- it means you will be able to prove any given statement (even ones which are outright false).

ukj 7y ago

Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project. [1] https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq [2] https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath

krapht 7y ago
Well, having used both, Lean really is a lot more ergonomic. Unimath is mostly category theory; other parts of mathematics are woefully underdeveloped.
- ukj 7y ago
  That's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never written human-computer interfaces before. When it comes to adapting humans to Mathematics, or adapting Mathematics to humans - I prefer the latter.

Hasz 7y ago

Headline is waaaay overblown, but not all of it is total hyperbole -- checkout out arxiv and try to read the abstract from just about any paper. It's basically totally impermeable. I'm almost done with an undergraduate degree in math and basically have no idea what ~90% of the research is about at anything other than a topical level. This is fine, it's written for specialists in the field (hopefully), but damn, for most fields, it's not a whole lot of people. Compared to physics or chemistry, math gets very specialized, very quickly. Depending on the field, there's no easy real world isomorphisms either, making it even more difficult.

hgtr 7y ago
I did some undergraduate research and ended up getting published. My initial drafts were written with prose so that I (and hopefully any novice) could understand. However, my professor wasn’t happy with it so I got some help from one of his grad students to re-write it. By the end of it I could barely understand my own paper. IMO the final paper had too much technical jargon which was convoluting some simple concepts. Kinda made me disenchanted with the academic world. Still have to give credit to my prof and the grad student, without their edits it probably wouldn’t have been published.
- echelon 7y ago
  This is one of the reasons why I pursued engineering instead of a hard science. Mathematics in particular feels like an ivory tower with a bunch of gatekeeping. Better language and grammar around core concepts could improve accessibility, but few in the field that I've encountered seem to care about that. Biology and chemistry are a bit better, but there are still improvements that could be made. You can't easily go from zero to biochem or ochem, and I don't think that has to be the case. Gen chem and gen bio just suck at presenting themes and concepts and instead focus on being a smorgasbord of facts (that you later have to amend or unlearn). Computer science and electrical engineering are a walk in the park by comparison. We have all sorts of interactive tools and visualizations of algorithms and analysis. We keep refining and making the onboarding process easier and more accessible.

breck 7y ago

Anyone interested in this topic, I have a prediction that the time is right for a new math, that starts from just 1 and 0, and builds every symbol up in a rigorous way. We're working on the infrastructure to make such a thing easier, but the project does not currently have a leader: https://github.com/treenotation/jtree/issues/83 https://github.com/treenotation/jtree/issues/83

devicetray0 7y ago
Forgive me, but why is the TreeNotation/jtree library the right place to craft a new "rigorous" mathematics language?
- breck 7y ago
  It’s a good question. This paper hints at the reason: https://github.com/treenotation/jtree/blob/master/papers/paper3/countingComplexity.pdf https://github.com/treenotation/jtree/blob/master/papers/pap... First, jtree is a bit orthogonal as that’s just an implementation. The github issue is there for convenience, it’s arbitrary. The reason for tree notation is that it’s a level up from binary. Binary notation does not give you the ability to define new symbols. Tree notation is a 2d binary. You can define new abstractions. It is a bridge between human and machine languages. Take any concept in mathematics, such as “derivative”. How would you define such a concept, starting only from 1s and 0s? Tree notation gives you a method to do that, in a way that’s not only efficient (noiseless), but also gives you practical tools, like complexity counting.
lidHanteyk 7y ago
Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf
- breck 7y ago
  Very interesting, thanks! This is definitely along the lines of what I’m thinking. It uses EBNF, i think if we switched it to tree notation it would be much, simpler, tighter, and more self contained.

lysium 7y ago

I’m sure this will help proofing papers. There will still be the problem of proofing that the software proofs what it is intended to proof.

ummonk 7y ago

Extreme clickbait headline. The subheading is '"I think there is a non-zero chance that some of our great castles are built on sand," he said, arguing that we must begin to rely on AI to verify proofs.'

asaph 7y ago
But, more consistent with the alarmist headline: > “I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk.
- parsimo2010 7y ago
  Someone who says that is, ironically, not concerned with the details. All of published math is wrong? No, a lot of is is understandable and verifiable by advanced undergraduates. Most of the fundamental theorems in each field are understandable by humans. As you get more and more abstract, and get into more and more obscure areas, you start to see non-understandable proofs built on top of non-understandable proofs. There's a danger that those are wrong, but when they collapse it just means that one professor has wasted their life, not that all of mathematics will suddenly collapse.
  - kevinzz 7y ago
    The headline is clickbait. A more measured debate about the issues is here https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...
dang 7y ago
We've replaced that with a more measured sentence from the article, in accordance with the HN guidelines ("Please use the original title, unless it is misleading or linkbait") https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

colorincorrect 7y ago

This short pdf which the article cites is more useful than anything the article itself contains: http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf

enjoyyourlife 7y ago
Discussion: https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404

iamaelephant 7y ago

This just seems like a native advertisement for Lean...

DoctorOetker 7y ago
I am not that perturbed by whatever framework they use, tools to translate the bulk of the majority of proofs from Lean to MetaMath to [...] and back will be made, the more important thing is that the number of humans aware of the existence of this tech and the more actually use it the better society will be off in the long run the following may seem totally impossible today but seems a lot less impossible to people who have been thinking about this for a long time: once sufficient mathematics has been translated, people can start adding physics postulates, one most physics has been inserted we can start formally verifying (up to validity of postulates on top of axioms) not just proper operation of digital circuits etc but also power plants and so on, and once interacting with proof systems becomes as widespread as alphabetic literacy, people might one day be able to formalize and vote on their requirements of society and policy, see predicted perverse incentives, or decide that policy can only be enacted when facets of their consequences can be proven. We might one day not vote on promises of strategy, also not vote on strategy, but rather on outcomes! I know it sounds absurd.

Ceezy 7y ago

"I believe that no human, alive or dead, knows all the details of the proof of Fermat’s Last Theorem. But the community accept the proof nonetheless," Buzzard wrote in a slide presentation[...] That s 100% clickbait. People knows the demonstration and the demonstration helped to create entire new fields. By the way there are new and shorter proof of the theorem.

hyperbovine 7y ago
Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.
- foooobar 7y ago
  Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".
- repolfx 7y ago
  I think the intended implication is that Wiles has not read or understood all of the proofs he built on. If someone said, "nobody dead or alive understands all the details of Windows" I doubt anyone here would find it controversial. It's too big to fit in one person's head.
- Stasis5001 7y ago
  Sure, Wiles obviously understands the main thrust of his proof. But one could argue that Wiles' result depends on lots of other results, which in turn depend on other results, and so on through decades and decades of work, ultimately going back to the foundations of mathematics. Neither Wiles nor anybody else can claim to rigorously understand all of it. You can imagine this as a tree, with Wiles' work as root, and his dependencies as ancestors, and so on. An error at a lower level of the tree could, in theory, invalidate the root node. I do agree with Buzzard that it's hard to be sure. I've definitely read papers where a critical argument isn't well written or what is written seems wrong. However, if there are low-level errors, I suspect that with some work things could be patched up.

madez 7y ago

I'm currently working on the formalization of Catalan's conjecture (or Mihăilescu's theorem) in Isabelle/HOL/Isar. My personal impression is that more formal verification is necessary in math, and it should be tought to every student of Mathematics in introductionary courses because it gives an unforgiving but also rewarding learning experience with formal proofs. Feel free to ask questions.

joker3 7y ago
How much research is being done on making these tools more user friendly? I spent a little bit of time using Coq about a decade ago, and while I agree that it's very important to make things like that widely used, there was a pretty steep learning curve.
- madez 7y ago
  I can't answer how much research or work is done to make the tools more user-friendly as I'm rather exclusively on the user-side. There exists extensive documentation in form of multiple PDFs, but they are only of little help to me as they lack useful examples. Sadly Google thinks every possible answer about Isabelle/HOL is answered by these PDFs as they are often the only relevant search result. However, Isabelle/HOL/Isar allows proofs to be written in a very human readable way, so the "documentation" I use is the existing library and how things are done there. There is a convenient Ctrl+left click action on terms to jump to their definition. That is very helpful to navigate unknown libraries. In comparison, I couldn't read and make sense the proofs I've seen in Coq. There is a learning curve with Isabelle/HOL/Isar. It can be extremely frustrating to not know how to express "simple" arguments or definition. But for someone familiar with manual "formal" proofs in mathematics, most can be learned in some hours under guidance, like in a seminar on a weekend with a couple of hours on each day. I'm learning rather autodidactly by trial and error. I think there would be value in a series of blog posts about "This is how you define a group" or "This is how you reason in nonclassical logic" or "This is how to proof the fundamental theorem of Algebra" all applied to Isabelle/HOL/Isar. There are often multiple ways to define things, and to be honest, I don't know the specific advantages and disadvantages. For example, I think you can introduce rings as type classes or as locales or using axiomatizations, and possibly more. This is one example of stuff I don't know how to manage in the system, but there is already a lot of structure defined, and I can reuse that.

higherkinded 7y ago

Suggestion to rely on AI for proof verification is just laughable. Neuron weights instead of formal definitions. So reliable.

drchewbacca 7y ago
It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail. Here is an example. https://arxiv.org/pdf/1608.02644.pdf https://arxiv.org/pdf/1608.02644.pdf
6gvONxR4sf7o 7y ago
That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier. Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.
not2b 7y ago
You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.
- higherkinded 7y ago
  Okay but they are formal systems and don't have anything to do with AI either, do they?
YeGoblynQueenne 7y ago
Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation. https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant This is Good Old-Fashioned AI, through and through.

bryanrasmussen 7y ago

I just can't help feeling that either the true should be correct, or the wrong should be false. But I guess English is not a strongly typed language.

raymondh 7y ago

Summary: Motherboard interviewed an attendee at the Interactive Theorem Proving conference who says that he thinks Interactive Theorem Proving is important. Also, professors specializing in proof theory think their tooling may become important but "the technology still needs improvement".

dls2016 7y ago

I had these fears about my dissertation work, but then realized that the “elder’s” papers were highly cited because they contained important machinery which could be modified and refined to prove other results... or the paper contained an important idea which went on to be proved in a variety of ways. Maybe it’s different outside of PDEs, but I doubt it.

repolfx 7y ago

To mathematicians, Welcome to our world! https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Actually working through some of [the details], when formalising them, made me understand that some of these issues were far bigger and more complex than I had realised. In the perfectoid project there is still an issue regarding the topology on an adic space, which I had assumed would be all over within about a page or two of pdf, but whose actual proof goes on for much longer Yeah, that's how software developers feel, all day, every day. That's why we all moan about being asked to give estimates for things. You don't really understand a thing until you've formalised it in code, and often things that look simple and easy turn out to be unexpectedly deep. Mathematics is a field that's been doing the equivalent of writing pseudo-code for thousands of years. There are endless reams of pseudo-code that looks like it might work, but as any programmer who's ever written pseudo-code knows, whether it actually runs when you try it out for real is anyone's guess. So now mathematics is starting to experience the pain of multiple incompatible programming languages/ecosystems. There's Lean, Coq, Isabelle/HOL and some new JetBrains language too. Soon they'll start to discover the value of 'foreign language interop', rigorous code review, comments, style guides, design documents, package management, automatic optimisation etc. Have you ever looked at a proof written in one of these languages? All code in these languages is a hot mess judged by the standards of professional software developers: tons of abbreviations, single letter variables, uncommented, ad-hoc module structure etc. I'm sure we'll eventually see mathematicians having raging flamewars about what clean style is and tabs vs spaces. Luckily for mathematicians though they work at their own pace and are under no deadline pressure. They'll figure it out.

joker3 7y ago

The headline is certainly overblown, but there probably errors out there. The interesting question is where we should be looking for them. All of the major results in an undergraduate or introductory graduate textbook have been studied often and thoroughly enough that we can be reasonably confident there are no errors in their proofs. There are errors in very new or very obscure material, but those tend to get corrected as more people start paying attention to them. It therefore seems like the search should therefore be concentrated in recent results that are becoming more useful but still aren't standard. On the other hand, we do need to build a standard library of results that can be used to prove those newer results. You can't do much in analysis without basic results on metric spaces, for instance.