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

51–60 of 107 posts

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

#51

Post by drchewbacca »

lidHanteyk wrote: post #24
breck wrote: post #12

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

Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf

Metamath is awesome if you're willing to slum it :)

https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...

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

#52

Post by Stasis5001 »

hyperbovine wrote: post #37
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.

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

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

#53

Post by nilkn »

knzhou wrote: post #25
Hasz wrote: post #9

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

That doesn’t mean that it’s wrong, it means that you need to read more. In a lot of fields, undergraduate material doesn’t qualify you to read papers, a PhD does. If all papers actually were written to undergraduate level, many would be 500 pages long. Who has time to write a book-length exposition of the basics of their field every time they publish? I mean, have you ever published a technical work? If so, did you g…

The problem is really that a PhD doesn't get you to reading level either. It might get you there in only one specialized subfield. And there might only be a few dozen other people who are also at reading level for that area. How much do you trust that small group to catch every single subtle, abstract error in papers published in the area?

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

#54

Post by lidHanteyk »

drchewbacca wrote: post #51
lidHanteyk wrote: post #24

Earlier quoted context omitted.

Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf

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.

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

#55

Post by imglorp »

Hasz wrote: post #9

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

Software is very much in crisis because of this exact problem.

Most of us build on top of a mountain of existing work; sometimes just setting a pebble on top and we have a new thing. But no human alive has seen, could remember, or could understand, each and every behavior down in that mountain, from pixels on the screen to pulses on the phy all the way to gates inside their processors.

So you read about the APIs you need; you set your pebble down with a little glue or duct tape; you hope you've connected it correctly; you hope the rest of the mountain works how you want; you hope you didn't miss any use cases for interfacing to the mountain; and you hope it doesn't have any undocumented surprises. Abelson and Sussman called this engineering by poking (1).

Of course, if you want to make something work fast with minimal work, this is great, it's the component future we dreamed about. But it also means we are clueless.

1. http://lambda-the-ultimate.org/node/5335

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

#56

Post by repolfx »

To mathematicians,

Welcome to our world!

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.

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

#57

Post by mathgenius »

hannob wrote: post #38
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…

So I find this interesting, because it seems to confirm a suspicion I held. I "only" did some undergrad math during my computer science (but due to a lack of specialization at my university back then it was "real math", i.e. we took the same courses as the math students). My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it…

Absolutely.

It's a problem with academia in general. Academics don't get rewarded for explaining things in an easy to understand way. Moreover, it is often a huge amount of work to distill results down like this. And if you succeed the response you may get is "well that is obvious".

Anyway, this is my counter argument to the "formalization of mathematics": why don't we incentivize people to bring some clarity to the exposition? If mathematics is suffering from faulty proofs, then I have little sympathy. Make it simpler, organize the concepts. Muscular calculations only go so far.

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

#58

Post by I_AM_A_SMURF »

hannob wrote: post #38
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…

So I find this interesting, because it seems to confirm a suspicion I held. I "only" did some undergrad math during my computer science (but due to a lack of specialization at my university back then it was "real math", i.e. we took the same courses as the math students). My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it…

> My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it sound harder than it really is. I never dared to postulate that this is a more general problem of math, but your words sound like that's exactly what is happening.

I "only" have a masters degree in Math, but this sounds really wrong to me. Most advanced math concepts are complex and can take months to understand for someone with an unrelated math background (e.g., say, Lebesgue measure theory or Galois theory). I wouldn't even know how to start teaching something like that to someone who doesn't have a formal mathematical background.

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

#59

Post by chongli »

hannob wrote: post #38
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…

So I find this interesting, because it seems to confirm a suspicion I held. I "only" did some undergrad math during my computer science (but due to a lack of specialization at my university back then it was "real math", i.e. we took the same courses as the math students). My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it…

The problem with math is that the only strategy we’ve discovered (with any success) for making a concept easier to learn is to connect it with a concrete, real-world analogy. This works because people find it easier to learn something if they can connect it to something else they already know. The Achilles heel of this approach is that it discards the abstract form of the concept such that the full generality is lost on the student.

One example I see frequently around here is the much-maligned monad tutorial. Writers keep trying to connect it by analogy to concepts with which imperative programmers are already familiar. As a math student, I would much prefer to be given a basic statement of the definition of a monad, a list of properties, and maybe a theorem to prove that some structure is a monad instead of having to fall back to the definition. From there, I would just work through a few exercises and start to understand what it is and how it works. Most people don’t work this way, however. People seem to be extremely resistant to learning by experimentation. Instead, they prefer to be given all the answers.

I suppose this isn’t really a problem that’s unique to math. We’ve also discussed how a lot of computer users fail to truly understand how the software works and instead prefer to follow steps by rote in order to carry out one particular task.

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

#60

Post by [deleted] »

imglorp wrote: post #55
Hasz wrote: post #9

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

Software is very much in crisis because of this exact problem. Most of us build on top of a mountain of existing work; sometimes just setting a pebble on top and we have a new thing. But no human alive has seen, could remember, or could understand, each and every behavior down in that mountain, from pixels on the screen to pulses on the phy all the way to gates inside their processors. So you read about the APIs you…

[deleted]
Post reply on HN