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

101–110 of 275 posts

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

#101

Post by konschubert »

MaxBarraclough wrote: post #72
cycrutchfield wrote: post #26

Earlier quoted context omitted.

Per Peter Scholze (from https://galoisrepresentations.wordpress.com/2017/12/17/the-a... ): >One final point: I get very annoyed by all references to computer-verification (that came up not on this blog, but elsewhere on the internet in discussions of Mochizuki’s work). The computer will not be able to make sense of this step either. The comparison to the Kepler conjecture, say, is entirely misguided: In that case, th…

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

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

#102

Post by danharaj »

mrob wrote: post #84
danharaj wrote: post #82

Earlier quoted context omitted.

Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.

If it is impractical now, that simply means the software needs improvement. If mathematicians stop being so accepting of informal proofs then there is a very strong incentive to improve the software.

> that simply means

The point is that it's not simple. It will require significant advances in computer science.

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

#103

Post by wtallis »

yesenadam wrote: post #89
wtallis wrote: post #81

Earlier quoted context omitted.

I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to…

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.

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

#104

Post by konschubert »

lacker wrote: post #69

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

And it's unlikely that there will be anything following from it if the article is right that it's basically "Trivialities to confuse the reader + an esoteric leap of faith"

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

#105

Post by rocqua »

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.

In all of my papers, I have attempted to include an indent-based hierarchy of the argument. Adding code-folding to this would allow for so much more detail here.

I don't think we should have papers being nothing but folds, but there is definite value in presenting proofs in this way.

One potential downside is that there is no longer an order that guides the reader through the paper. Because it isn't quite clear how deep the author expected you to unfold an argument.

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

#106

Post by strikelaserclaw »

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…

Tao has always been a proponent of the fact that proving a theorem establishes powerful tools that might help mathematicians work on other problems, i think his comment is that this does not do that

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

#107

Post by rocqua »

atmanthedog wrote: post #93
ericsoderstrom wrote: post #40

Earlier quoted context omitted.

Math is different in that one feels there should be something close to "absolute truth." That is, given a set of axioms, it is possible to verify with complete certainty whether a proof follows from those axioms or not. Though when proofs become so long and abstruse that only a handful of people can even read them, perhaps that's no longer true. In other fields, it's more clear that nothing is known with 100% certain…

Unfortunately, math doesn't really permit this type of truth: if your axioms are strong enough to prove general statements about arithmetic, there is no effective procedure to determine whether an arbitrary proof follows from those axioms.

Still, given a set of axioms, statements will fall into one of three categories. 1) Provably True, 2) Provably False, 3) Undecideable

Claims that a statement is in category 1 are fully verifiable (by providing the proof). The same goes with claims that a statement is in category 2.

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

#108

Post by dogecoinbase »

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.

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.

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

#109

Post by zbobet2012 »

danharaj wrote: post #79
zbobet2012 wrote: post #67

Earlier quoted context omitted.

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…

I own a copy of the HoTT book :) > Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when…

I agree completely that the tooling is not there today.

However:

"The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. "

Mis-understands why and how we use the linux kernel. Linux isn't that difficult to understand really (both in LOC, and the abstractions it presents). It's simply a base which can be relied on that provides abstraction points we can interface with (both as software, _and_ hardware_).

The important part here is that not only does linux give us a reliable "library" of behavior, but it is one that is common and reuseable.

This "library" of behavior is something we've begun to see present itself in category theory. This is why so many modern papers start with "we show that there exists a isomorphism...".

The biggest thing _modern_ computing and libraries focuses on is composition of behavior. Aka functions that take functions. If a computational interpenetration of uni-valence is found we will have similar capabilities in math (e.g. making it possible to simplify the process of moving between isomorphic structures). I believe this would be a major stride towards broader use of machine verification.

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

#110

Post by patrickthebold »

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?

Imagine convincing someone that a web service could be written, vs getting it written and deployed to production.

And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...

Post reply on HN