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

101–107 of 107 posts

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

#101

Post by casefields »

dorchadas wrote: post #74
imglorp wrote: post #55

Earlier quoted context omitted.

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…

In this case, it likely applies to every aspect of modern day life. Man is no longer a generalist, and we are forced to build upon the foundations others have put, and hope they work.

No one human knows how to make a pencil: https://fee.org/resources/i-pencil/

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

#102

Post by ukj »

krapht wrote: post #81
ukj wrote: post #8

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 [2] https://github.com/UniMath/UniMath

Well, having used both, Lean really is a lot more ergonomic. Unimath is mostly category theory; other parts of mathematics are woefully underdeveloped.

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.

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

#103

Post by YeGoblynQueenne »

digama0 wrote: post #96
YeGoblynQueenne wrote: post #95

Earlier quoted context omitted.

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

But formal methods are also supported by theory where any theorems have proofs done by humans, which may contain mistakes. It's humans all the way down, see.

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

#104

Post by CBVanderhuge »

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 thing is that actually doing mathematics is a process where you take your intuition and find a way to formalize it into definitions and proofs and computations.

A toddler could understand the difference between a smooth curve and a spiky curve, but to actually get a handle on them computationally, the best tool that we have is Calculus -- and even after decades of people iterating on how to teach it, Calculus is still a mystery to most undergrads who muddle through it.

Similarly I could give you some intuition about manifolds by telling you that they're kinda like surfaces that can have higher dimensionality, but until you're able to actually understand and work with the definition of "locally homeomorphic to R^n", you're not going to be able to do anything with them.

I think it's bollocks, this idea that mathematicians are obfuscating easy concepts with complex language. The language doesn't exist to get research grants and gatekeep, it's there because you need some succinct way to describe objects and concepts without running through a full definition every time.

Obviously you can always improve communication, and from my experience most mathematicians try pretty hard to do that, especially in the classroom, but it's not easy.

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

#105

Post by imglorp »

casefields wrote: post #101
dorchadas wrote: post #74

Earlier quoted context omitted.

In this case, it likely applies to every aspect of modern day life. Man is no longer a generalist, and we are forced to build upon the foundations others have put, and hope they work.

No one human knows how to make a pencil: https://fee.org/resources/i-pencil/

Beautifully put, with afterward from Milton Freidman putting it into context.

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

#106

Post by yaccz »

chongli wrote: post #59
hannob wrote: post #38

Earlier quoted context omitted.

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…

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

Have you looked into the original paper?

https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/b...

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

#107

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]
Post reply on HN