Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

vice.com

Post reply on HN
Print view View original

91–100 of 107 posts

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

#91

Post by knzhou »

Silhouette wrote: post #87
knzhou wrote: post #69

Earlier quoted context omitted.

People will complain about that too. The introduction is "redundant" or "trivial". The book is a long, bloated slog. (Since what you're proposing will unavoidably increase the page count.) The author intentionally confuses students by alluding to some "main theorem" but waiting a hundred pages to say what it is, instead of putting it in front where it belongs. For every complaint about a textbook, there is an equal a…

People will complain about that too. The introduction is "redundant" or "trivial". The book is a long, bloated slog. Some people will, but they probably aren't the target audience for the book, and most people won't. You don't teach kids who are learning to count about 0 by explaining group theory and identity elements.

I promise you that explaining a technical advanced math subject is less obvious than this, and that even students that come in with the same background will strongly disagree over which books are easiest to read.

Maybe it's obvious that sketching only a little formalism is the best. But then some of your statements end up vague, and students stumble on practice problems where they really need to understand the details of the formalism.

Maybe it's obvious that stating things as simply as possible is the best, even at the cost of generality. But then your statements won't be powerful enough when people try to go beyond the few simple examples you give, and people will feel betrayed.

Maybe it's obvious that a historical approach is the best, for motivation. But historical papers are extremely confusing to read. They're full of redundant checks of things we know are obviously true today, and archaic notation and jargon. People will get annoyed at slogging through ten pages of text to confirm something that is obvious in a modern formalism.

Maybe it's obvious that a modern, clean formulation is best. But then the definitions are unmotivated, seem to come out of nowhere, there's not enough connection to the historical development, and your book won't be compatible with older books.

Maybe it's obvious that no formalism at all is best; you just show how to solve problems concretely. But this turns what could have been a few simple principles into an enormous bag of ad hoc tricks people need to memorize. Textbooks that do this are derisively referred to as "cookbooks".

It is not obvious how to write a book.

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

#92

Post by hyperbovine »

Stasis5001 wrote: post #52
hyperbovine wrote: post #37

Earlier quoted context omitted.

Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.

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 h…

Right, speaking as a lapsed mathematician, I definitely see errors or gaps in published work. Wiles’ original FLT proof had one. And yes these can generally be patched up. I’m not quite as alarmed as the author is, because generally a major false result would have all sorts of alarming ripple effects and implications which would be pretty easy to spot. FLT is an extreme example where literally anyone with a calculator could in theory disprove it. The fact that no one has suggests to me that it’s likely true.

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

#93

Post by Silhouette »

knzhou wrote: post #91
Silhouette wrote: post #87

Earlier quoted context omitted.

People will complain about that too. The introduction is "redundant" or "trivial". The book is a long, bloated slog. Some people will, but they probably aren't the target audience for the book, and most people won't. You don't teach kids who are learning to count about 0 by explaining group theory and identity elements.

I promise you that explaining a technical advanced math subject is less obvious than this, and that even students that come in with the same background will strongly disagree over which books are easiest to read. Maybe it's obvious that sketching only a little formalism is the best. But then some of your statements end up vague, and students stumble on practice problems where they really need to understand the detail…

It is not obvious how to write a book.

I agree, and I also agree that readers will differ in which books they find easiest to read. Different people learn in different ways.

However, in some respects, it is obvious how not to write a book. Mathematics is not magically exempt from effective technical writing skills, nor all we have discovered about cognitive psychology and how people learn, nor anything else that goes into creating a generally good presentation.

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

#94

Post by madez »

joker3 wrote: post #84
madez wrote: post #30

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.

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.

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.

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

#95

Post by YeGoblynQueenne »

robinhouston wrote: post #40
Ceezy wrote: post #28

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

There’s a great discussion of this on Buzzard’s blog. https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Read the comments too.

One of the commenters wonders why we can trust a proof assistant more than a human:

>> if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.?

To which Buzzard's reply is that, well, computer scientists have done a thorough job proving the correctness of proof assistants:

>> To check that Lean has correctly verified a proof, we don’t need to check that Lean has no bugs, we just need to check that it did its job correctly on that one occasion, and this is what the typecheckers can do. This is a technical issue and you’d be better off talking to a computer scientist about this, but they have thought about this extremely carefully.

Reading this as a computer scientist whose field of study is buiilt on automated theorm proving and logic programming (not what proof assistants do, exactly, but close, and some proof assistants even use resolution theorem proving, I understand) this is placing way too much trust on computer scientists. Every bit of theory on automated theorem proving that has ever been published is like maths: theorems are proved by hand, on paper, by humans. And some proofs can be quite convoluted. There's nothing approaching the complexity of the mathematical proofs that make Kevin Buzzard worry, but still, the proofs are not trivial and there is plenty of scope for error.

So I'm afraid that even with computer-aided proofs, we 're still building castles on sand.

Which is quite shocking if you think about it. We think that, maybe we can't trust our minds to know anything with any certainty, but we can trust computers to be flawless in their computations. But how do we know that with any certainty, if we can't know anything with any certainty?

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

#96

Post by digama0 »

YeGoblynQueenne wrote: post #95
robinhouston wrote: post #40

Earlier quoted context omitted.

There’s a great discussion of this on Buzzard’s blog. https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Read the comments too.

One of the commenters wonders why we can trust a proof assistant more than a human: >> if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.? To which Buzzard's reply is that, well, computer scientists have done a thorough job proving the correctness of proof assistants: >> To check that Lean has correctl…

Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a bootstrapping theorem prover (Metamath Zero) to do this in a few hundred lines of code. So it's not as hopeless as it seems. You just have to have a really efficient and simple checking algorithm and run it over a big computer generated proof of correctness, and it all scales very well. Then you can take that verified theorem prover and apply it to all the regular math we care about.

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

#97

Post by digama0 »

higherkinded wrote: post #31

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

Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching). No one in ITP is seriously using modern neural net based AI in real theorem provers yet, although there are several research teams working on it.

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

#98

Post by digama0 »

lidHanteyk wrote: post #54
drchewbacca wrote: post #51

Earlier quoted context omitted.

Metamath is awesome if you're willing to slum it :) https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...

How long does it take your preferred proof assistant to prove things? Metamath's standard set.mm takes only about 10s to prove everything .

Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn't matter, or at least is secondary to ease of use, mathematical cleanliness etc, from the functional programming community. It turns out that once you make this decision it's difficult to get that raw speed back, even if you start worrying about performance later, and the HOL family provers make it worse by defining correctness in terms of the running of an ML program, which bakes the runtime of the ML system into the proof checking time.

When you combine this with the fact that these ML programs are not proofs but proof scripts, that perform a lot of "unnecessary" work like searching for a proof rather than just going straight for the answer, it suddenly begins to make sense why these systems take on the order of hours to days to check their whole libraries.

Coq and Lean are somewhere in the middle, because they have proof terms, but the logic itself still requires some unbounded computations. Checking a proof here is often fast, unless you make too much use of computation in the logic. But people often don't care about proof terms, and still store the proof scripts, which are as slow as ever.

Metamath is in this setting somewhat unique in eschewing proof scripts altogether, or more accurately, inlining proof scripts immediately on the author's machine. The resulting proofs are often comparatively long and verbose, but I would argue this is only a display matter, since all the other provers are doing the same thing, they just aren't showing it.

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

#99

Post by [deleted] »

echelon wrote: post #34
hgtr wrote: post #21

Earlier quoted context omitted.

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…

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…

[deleted]

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

#100

Post by higherkinded »

not2b wrote: post #63
higherkinded wrote: post #31

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

You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.

Okay but they are formal systems and don't have anything to do with AI either, do they?
Post reply on HN