Titans of Mathematics Clash Over Epic Proof of ABC Conjecture • Hacker News Board

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

#191

Post by kstrauser » Fri, Sep 21, 2018, 5:49 AM UTC

fjsolwmv wrote: post #148

kstrauser wrote: post #88

Earlier quoted context omitted.

I think you're exactly right. Mochizuki's work may or may not turn out to be sound, but in the mean time he's failed to communicate it to other experts, even when they've met with him in person for the specific goal of understanding his reasoning. It's not sufficient to have a great idea, or even to be right about it. You have to be able to explain it thoroughly enough that other qualified peers can understand your l…

It's sufficient for Mochizuki. Everyone else can decide for themselves what is sufficient for them.

Presumably he’d like recognition for having proven it. Unless he can explain and communicate his theorem to others, his work won’t be accepted. That doesn’t seem sufficient.

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

#192

Post by Myrmornis » Fri, Sep 21, 2018, 5:49 AM UTC

Retra wrote: post #170

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.

Trying to do learn math with a computer is frustration. The computer eats up your desk space, you have to constantly move it around as you work on different things, a mouse and keyboard eat up even more space. You have to have power, and you have to drop your pen every other time you need something. Maybe you don't see the problem because you aren't doing any math?

I’ve been studying undergrad maths for the last year or two, and I had a bit of a breakthrough when I realized how much more effective it was for me to do all my work (notes, exercises) in LaTeX rather than with pen and paper. I can refactor at will, improving proofs, and the consistent tidy typesetting makes me think more systematically about the problem I’m working on.

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

#193

Post by forkerenok » Fri, Sep 21, 2018, 5:50 AM UTC

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?

The bottleneck is not the tool itself, but the theory it builds upon: Calculus of Constructs in Coq's case. CoC and other calculi oriented towards proofs have limitations.

To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on...

It's quite dense, but there are some bits that I, as a programmer, could understand.

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

#194

Post by nutanc » Fri, Sep 21, 2018, 5:54 AM UTC

masterjack wrote: post #163

nutanc wrote: post #155

Earlier quoted context omitted.

Agree with this. Don't think there are too many mathematicians who can really argue for or against a really important theorem. My prof has come up with one for Riemann hypothesis[1], but he is not finding anyone willing to engage in a discussion. Most mathematicians seem to believe that the Riemann hypothesis is unsolvable and I don't think it helps that my prof is currently not associated with any reputable universi…

Unfortunately way more often than not attempted proofs of hard problems end up flawed, especially if there are certain warning signs: https://www.scottaaronson.com/blog/?p=304 That said, I’d be happy to go over this as an analytic number theorist rfurman@alumni.stanford.edu

Thanks. Will share the details with my prof.

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

#195

Post by roenxi » Fri, Sep 21, 2018, 6:15 AM UTC

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…

> The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).

If we accept that a software program is isomorphic to a proof, is there anything that isn't isomorphic with a proof?

I can prove Pythogoras' theorem with a diagram, so by extension anything in the physical world is a manifestation of mathematical theory and, since it exists, is isomorphic with a trivial proof for something.

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

#196

Post by wtallis » Fri, Sep 21, 2018, 6:17 AM UTC

abenedic wrote: post #190

abenedic wrote: post #189

Earlier quoted context omitted.

>not an inherent limitation of all backlit displays everywhere. This may be true, but in my experience(not very wealthy, typically sub $400 devices) the presets are set such that 0% backlight in the OS is glaringly bright. I cannot turn it down without rooting the device.

Maybe for tech device things we should have two separate tracks, one for wealthy snd people who can modify devices and one for poor and people who cannot. Even my Thnkpad laptop under Ubuntu has a setting for 10% brightness which is far too high for a truly dark room. The next lowest setting is 0% which is absolute dark. How do you use your laptop under such conditions?

I don't see how backlight settings for a truly dark room are relevant here. I've been annoyed by several of my devices being unable to dim far enough, but never in a situation where I would expect to be able to easily read words printed on paper. An office or classroom setting that has adequate light for pen and paper work could be too dim for an LCD at 100% brightness to be comfortable, but almost any device can be dimmed enough for that environment.

Color temperature can also be a problem, but there's a lot of awareness of that issue nowadays. Most operating systems now support automatic adjustment of color temperature based on time of day, plus manual adjustment. Devices that adjust their color temperature to account for ambient lighting are starting to catch on, and I expect they'll be pretty common in a few years.

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

#197

Post by ken47 » Fri, Sep 21, 2018, 6:31 AM UTC

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…

FYI, the proof has convinced other mathematicians.

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

#198

Post by vbezhenar » Fri, Sep 21, 2018, 6:33 AM UTC

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

It's like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.

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

#199

Post by zakk » Fri, Sep 21, 2018, 6:41 AM UTC

Retra wrote: post #171

zakk wrote: post #127

Earlier quoted context omitted.

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.

Well, that's not what he said, and he still is one of the world's best mathematicians. So one wonders why you would take that surprise as indicative of a mistake on his part rather than on yours?

Well, in science there’s a simple rule: your substantiate your claims.

A plausibility argument like Tao’s one is simply not an argument.

To show that Mochizuchi is wrong you need to point out which equation of his work is wrong, which by the way is Peter Scholze’s plan.

Tao by his own admission does not have the background to evaluate Mochizuchi’s theory and still gives this worthless plausibility argument, appealing to his knowledge of other unrelated proofs. I’m astonished.

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

#200

Post by jedharris » Fri, Sep 21, 2018, 7:17 AM UTC

thanatropism wrote: post #91

man-and-laptop wrote: post #66

Earlier quoted context omitted.

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…

I once tried proving the very first theorem in Cannas da Silva's book of symplectic geometry in this style. Screw that. The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books). Most of the time, the point of proofs isn't to establish something is true, but to communicate something ab…

If you are right then calling them "proofs" is misleading. The results aren't proven, just made convincing. So I guess they are "arguments" -- only detailed enough to convince others who already know enough about the entities being discussed.

Automated proofs by contrast really are proofs but as many of these comments show are not arguments.

So maybe the problem to be solved is to appropriately connect mathematical arguments (what mathematicians call proofs) to proofs, while recognizing that they are actually two entirely separate families -- as different as plants and animals.