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

121–130 of 275 posts

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

#121

Post by ssmmww »

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.

My understanding is that the Monty Hall problem was just a cute puzzle published in a pop-sci magazine that confused a few professors who perhaps ought not to have been confused by it. I don't think it says anything at all about the health of the mathematical community.

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

#123

Post by codethief »

zbobet2012 wrote: post #67
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…

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

Speaking of Lamport's "How to write a 21st-century proof" paper, here's a video of a great presentation he gave on this topic last year:

https://www.heidelberg-laureate-forum.org/blog/video/lecture...

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

#124

Post by codethief »

Jach wrote: post #46
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…

How to Write a 21st Century Proof: https://lamport.azurewebsites.net/pubs/proof.pdf From page 6 with figure 1, to page 10 with figure 3, it's clear that even just changing to structured proofs over prose proofs can be helpful in catching errors. Of course the rest of the paper goes into detail about going even further... I don't know if Lamport's ideas have gained any more acceptance in the mathematics communities, b…

Here's a video of an excellent presentation Lamport gave on "21st-century proofs" last year:

https://www.heidelberg-laureate-forum.org/blog/video/lecture...

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

#125

Post by ChrisRackauckas »

vbezhenar wrote: post #42
salty_biscuits wrote: post #27

Earlier quoted context omitted.

The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.

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…

A lot of areas like real/stochastic analysis are really difficult to map to any formal proving mechanism. Really there are only some areas in abstract algebra where it can be done, and in there you still need some proofs that link a set of real problems to a computable problem and finish with the computation (Groebner basis proofs are one example). But that's rare.

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

#126

Post by auntienomen »

wtallis wrote: post #103
yesenadam wrote: post #89

Earlier quoted context omitted.

people with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?

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.

Two points:

1) Mathematicians write all over the papers and books they read. Electronic versions of this exist (e.g., Xournal, written by a well known mathematician), but they tend not to be as convenient as simply scribbling on paper.

2) Mathematicians digest papers nonlinearly. Digital presentations don't usually lend themselves to flipping back and forth between pages. At times, I suspect mathematicians use papers and books as memory mansions, organizing concepts by relating them to their location in the physical copy.

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

#127

Post by zakk »

avip wrote: post #14
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.

Tao's commentary is especially interesting for me as a non-mathematician: >It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever. Likely such is the understatement-ish way of a mathematician to say "This is clearly…

To me it sounds more like: I don't like the idea of this theory working, but I don't have a refutation.

Honestly I am surprised of hearing such an argument from one of the world's best mathematicians.

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

#128

Post by darkmighty »

WalterGR wrote: post #100
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... )

If you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.) What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?

> What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?

I think there are two parts:

1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something.

2) Provide some sort of computational intelligence to fill in natural gaps of proofs. I believe humans tend to leave a large number of more or less trivial gaps even in rigorous mathematical proofs that couldn't be avoided by language syntax. For this probably some kind of AI system would be ideal that tries to derive successive results and complete the proof automatically.

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

#129

Post by timb07 »

Obi_Juan_Kenobi wrote: post #39

Slightly OT: it was very nice to read an article that made such wonderful use of links. Just about every case where material could be directly linked, it was done. I particularly enjoyed the link to Dr. Calegari's blog post, as it was interesting to read the comments in 'real time' and compare that with the author's synthesis. Very good article!

Even further OT: I was good friends with Frank Calegari's older brother (also a mathematician) at school, and used to play bridge with Frank at university. I'm not a mathematician but I do sometimes read articles when they're posted on HN, so it was a surprise to see someone I know mentioned. :p

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

#130

Post by antidesitter »

FabHK wrote: post #86
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…

> 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

Depends on your starting point. You can prove 1+1=2 quite easily from the Peano axioms:

1+1=1+S(0) [definition of 1]

1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)]

1+1=S(1+0) [transitivity of equality]

S(1+0)=S(1) [definition of addition, a+0=a]

1+1=S(1) [transitivity of equality]

S(1)=2 [definition of 2]

1+1=2 [transitivity of equality]

Post reply on HN