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

61–70 of 275 posts

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

#61

Post by shoo »

sorokod wrote: post #29
neuronexmachina wrote: post #18

Earlier quoted context omitted.

I think it might be more akin to a programmer complaining about a monolithic/black-box chunk of code that can't easily be split into understandable and/or unit-testable functions.

For the analogy, I'd replace 'unit-testable' with reusable

I'd argue for something stronger: both reusable and useful (outside of the initial application) and novel.

It's possible to write structurally reusable components that are useless, i.e. they do a thing that no one wants or needs.

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

#62

Post by mehrdadn »

nabla9 wrote: post #54
mehrdadn wrote: post #48

Earlier quoted context omitted.

Edit: never mind, it seems I confused deriving a proof with verifying it!

vbezhenar is talking about verifying proofs not finding proofs. Computers can easily verify that proof is correct once the proof is written down using formal semantics. Proof checkers already exist.

Great point, thank you!

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

#63

Post by p1esk »

guelo wrote: post #37
sajid wrote: post #5

https://galoisrepresentations.wordpress.com/2017/12/17/the-a... Terence Tao and Peter Scholze (and others) join the discussion in the comments section.

That discussion is from before Scholze & Stix wrote their criticism.

Scholze wrote it right there: https://galoisrepresentations.wordpress.com/2017/12/17/the-a...

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

#64

Post by barbecue_sauce »

Moodles wrote: post #12

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…

You have an MSc in mathematics but don't consider yourself an expert?

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

#65

Post by dagw »

barbecue_sauce wrote: post #64
Moodles wrote: post #12

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…

You have an MSc in mathematics but don't consider yourself an expert?

I've also got an MSc in mathematics, I and feel that that was barely enough time to just start scratching the surface.

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

#66

Post by man-and-laptop »

Moodles wrote: post #12

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…

Lamport suggests hierarchical proofs as a possible remedy. They're somewhere in between computer verification and the current prevalent style.

Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.

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

#67

Post by zbobet2012 »

danharaj wrote: post #50
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…

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

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint.

The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is then to develop languages which encompass these modern methods.

This is really the goal of the homotopy type theory project, to provide a language which is both machine checkable and easy to use informal reasoning with.

[1]https://www.microsoft.com/en-us/research/publication/write-2...

https://www.youtube.com/watch?v=kOY-XE29_d8

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

#68

Post by jetrink »

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…

> Does that not feel arbitrary, to drop the repetitions?

If the conjecture turns out to be true, then that apparently arbitrary step turns out to be meaningful, because it uncovers a hidden relationship between the numbers A, B and C and their factors.

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

#69

Post by lacker »

I remember an instructor explaining during the math olympiad training program: "A proof doesn't have to be in any particular format. A proof is an argument that can convince other mathematicians."

At this point, it seems clear that we do not have a proof of the ABC conjecture. Perhaps someone will be able to improve this to make a real proof - after all, there were some errors in the first Wiles proof of Fermat's Last Theorem, but they ended up being minor errors that were fixed up once they were found. But what we have is not a proof.

Post reply on HN