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

Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

quantamagazine.org

Post reply on HN
Print view View original

111–120 of 275 posts

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#111

Post by resters »

bollu wrote: post #51
vbezhenar wrote: post #42

Earlier quoted context omitted.

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

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

What is the painful part? The level of detail required for it to check?

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#112

Post by S4M »

mrob wrote: post #57
danharaj wrote: post #50

Earlier quoted context omitted.

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

Why can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.

Is code-folding necessary? Instead you could put the demonstration in an appendix, and the authors would be free to decide what goes in the core of the article and what goes into the appendix. This could be made automatically where trunks of article would move back and forth from the core to the article and vice-versa, depending of what the reader chose to, and in each case a corresponding pdf could be generated.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#113

Post by westoncb »

edflsafoiewq wrote: post #96
westoncb wrote: post #60

> “The abc conjecture is a very elementary statement about multiplication and addition,” said Minhyong Kim of the University of Oxford. It’s the kind of statement, he said, where “you feel like you’re revealing some kind of very fundamental structure about number systems in general that you hadn’t seen before.” I can kind of see that, but there's something in it that gives me the feeling of arbitrariness. It's lookin…

Another way to think about it is to consider what needs to happen for rad(abc) to be much less than c. This can only happen if the "dropping" you mention drops a whole lot of factors. In other words, it can only happen if a, b, and c all contain mostly large powers of primes. The prime factorization of a number is essentially "random". That makes numbers that are large powers of primes rare; it's like rolling a die a…

Great explanation—thanks. I think I got the upshot, though I am unclear on what function rad() is.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#114

Post by rocqua »

WilliamEdward wrote: post #49
a-nikolaev wrote: post #32

Earlier quoted context omitted.

Math academic community is actually very healthy overall, in my experience.

see: monty hall problem But anyway, mathematics is not any more unhealthy than any other field, but it does have toxicity like all others do as well.

Given the anecdotal correlation between math and autism, and the effects of autism on sociability, one might expect mathematics to have different toxicity.

I never went deep enough into mathematical academia to judge, let alone getting into other fields to allow for a comparison.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#115

Post by edflsafoiewq »

westoncb wrote: post #113
edflsafoiewq wrote: post #96

Earlier quoted context omitted.

Another way to think about it is to consider what needs to happen for rad(abc) to be much less than c. This can only happen if the "dropping" you mention drops a whole lot of factors. In other words, it can only happen if a, b, and c all contain mostly large powers of primes. The prime factorization of a number is essentially "random". That makes numbers that are large powers of primes rare; it's like rolling a die a…

Great explanation—thanks. I think I got the upshot, though I am unclear on what function rad() is.

rad is the arbitrary function you asked about ;) rad(x) is the product of the distinct prime factors of x, ie. it drops repeated prime factors, rad(2^n)=2, etc.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#116

Post by rocqua »

westoncb wrote: post #113
edflsafoiewq wrote: post #96

Earlier quoted context omitted.

Another way to think about it is to consider what needs to happen for rad(abc) to be much less than c. This can only happen if the "dropping" you mention drops a whole lot of factors. In other words, it can only happen if a, b, and c all contain mostly large powers of primes. The prime factorization of a number is essentially "random". That makes numbers that are large powers of primes rare; it's like rolling a die a…

Great explanation—thanks. I think I got the upshot, though I am unclear on what function rad() is.

rad is the radical of a number [1]. In short rad(x) is the product of all unique prime factors of x.

So rad(8) = 2, rad(24) = 6, rad(75) = 15

[1] https://en.wikipedia.org/wiki/Radical_of_an_integer

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#117

Post by wtallis »

dogecoinbase wrote: post #108
wtallis wrote: post #103

Earlier quoted context omitted.

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

It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays They're mathematicians, not display interface experts. This is like demanding that someone explain to you why they don't like a particular kind of food -- people are allowed to dislike things without having a complete internal axiomatic system justifying it.

Dislike, sure. Personal preferences are acceptable. But claiming that it's impossible for a computer/tablet display to be as readable as paper and that all electronic displays cause more eyestrain is unreasonable. Especially when the person making that claim has already demonstrated that they are familiar with terms like resolution, contrast ratio and form factor, but they fail to even propose a hypothesis for what might still be inferior about the best computer display technologies.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#118

Post by dwheeler »

Smaug123 wrote: post #95
FabHK wrote: post #86

Earlier quoted context omitted.

> Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. Just as an example, Russell & Whitehead's Principia Mathematica famously requires some 400+ pages to prove that 1+1=2 (well, they prove some other stuff, too, I suppose.) See the image and caption here to get a flavour: https://en.wikipedia.org/wiki/Principia_Mathematica

It's not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.

Exactly right. Most of those background steps do things like establish the basics of complex numbers, and you can reuse them for anything else involving complex numbers.

The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html

It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory.

It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large.

If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE#

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#119

Post by davemp »

resters wrote: post #111
bollu wrote: post #51

Earlier quoted context omitted.

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

What is the painful part? The level of detail required for it to check?

How current proof assistants work is using the Curry-Howard correspondence, [1] the gist of it is that all of first order logic can be encoded into a type. All one must do is write an expression that type checks to what one is trying to prove. That turns out to be fairly hard for reasonably complex proofs.

[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#120

Post by heinrichhartman »

konschubert wrote: post #101
MaxBarraclough wrote: post #72

Earlier quoted context omitted.

> The computer will not be able to make sense of this step either. What does that mean, then? That a leap is being made that depends on the reader's fuzzy intuitions, rather than the established axioms? If that's the case, it's not a formal proof at all, no? Or am I way off here?

Maybe he says that the computer won't help understand the proof since the proof is missing a step. He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“

Exactly, this is how I read it as well.
Post reply on HN