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

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

#181

Post by nateburke » Fri, Sep 21, 2018, 4:21 AM UTC

groby_b wrote: post #154

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…

Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yea…

Paper math books also do not serve up distracting ads.

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

#182

Post by wtallis » Fri, Sep 21, 2018, 4:35 AM UTC

groby_b wrote: post #154

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…

Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yea…

The reddit thread in question was surprisingly lacking in discussion of the usability aspects you're focusing on. I think most of those issues make for a much more productive conversation, because there's real room for improvement in those areas—paper and current computer/tablet technology each have their own usability pros and cons. I'm not at all uninformed about those usability challenges. I was just surprised and disappointed at how many people assumed that paper had an unbeatable advantage on the purely visual aspects of presenting information, as if computers were still limited to 100dpi with really poor black levels.

> The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position.

I didn't propose any specific markup because the specific syntax isn't the problem. The problem is that the predominant markup language for mathematical documents is LaTeX, which is a bit too presentation-oriented rather than semantic/structure-oriented for it to be really easy to use it to produce documents that can be interactively folded (especially when the output file format is almost always PDF). Something that used eg. MathML and an HTML/XML based overall document structure can trivially encode all the information necessary for rich interactive reading, and proposing specific tag or class names to indicate what lines of a proof should be collapsed by default only invites bikeshedding.

I think you're quite unjustified in accusing me of being so thoroughly uninformed.

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

#183

Post by [deleted] » Fri, Sep 21, 2018, 4:41 AM UTC

thrmsforbfast wrote: post #179

throwawaymath wrote: post #162

Earlier quoted context omitted.

> When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true...Integers aren't decidable...Reals are decidable I'm not talking about decidability. I'm talking about computability. Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed. But that has no bearing…

> I'm not talking about decidability. If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures! Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a butt…

[deleted]

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

#184

Post by derangedHorse » Fri, Sep 21, 2018, 4:51 AM UTC

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…

You could say the same thing about code, yet we're able to build upon our abstractions to make something both high level and able to be broken down to the foundations.

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

#185

Post by derangedHorse » Fri, Sep 21, 2018, 4:56 AM UTC

nateburke wrote: post #181

groby_b wrote: post #154

Earlier quoted context omitted.

Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yea…

Paper math books also do not serve up distracting ads.

Math ebooks shouldn't either lol

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

#186

Post by anonlastname » Fri, Sep 21, 2018, 5:09 AM UTC

darkmighty wrote: post #128

WalterGR wrote: post #100

Earlier quoted context omitted.

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…

I think coq has some kind of ml software. I saw it mentioned in the proof general UI. I'm not sure how good it is

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

#187

Post by busyant » Fri, Sep 21, 2018, 5:13 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.

> It's sufficient for Mochizuki. Everyone else can decide for themselves

This sounds like a variant of the Turing test.

Mochizuki and your pet dog both claim to have proven the ABC conjecture. The ABC conjecture has been proven when you can understand one proof but not the other.

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

#188

Post by mikorym » Fri, Sep 21, 2018, 5:16 AM UTC

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…

There is an alternative way (but not a replacement) to go about it as well. Rather than reverifying proofs (I mean now ones that have been proved in the literature) one could study central features. And whenever a feature breaks, then one can stop to think whether the theorems themselves hold water or not.

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

#189

Post by abenedic » Fri, Sep 21, 2018, 5:24 AM UTC

wtallis wrote: post #180

abenedic wrote: post #168

Earlier quoted context omitted.

> improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs. And what Grad student can afford those at [Insert State University]. I was a PhD student in math not long ago, and vastly preferred paper books, and even printed out articles. It is way way easier on your eyes than something actively blasting light. Maybe in 20 years high quality…

> It is way way easier on your eyes than something actively blasting light. See, this is the kind of bad argument that really irks me. There are good arguments about how computers aren't ready to replace pen and paper for actively doing math, and even a few shortcomings for computers replacing paper textbooks. But "actively blasting light" doesn't mean anything. Photons are photons. If you think a backlit display is…

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

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

#190

Post by abenedic » Fri, Sep 21, 2018, 5:35 AM UTC

abenedic wrote: post #189

wtallis wrote: post #180

Earlier quoted context omitted.

> It is way way easier on your eyes than something actively blasting light. See, this is the kind of bad argument that really irks me. There are good arguments about how computers aren't ready to replace pen and paper for actively doing math, and even a few shortcomings for computers replacing paper textbooks. But "actively blasting light" doesn't mean anything. Photons are photons. If you think a backlit display is…

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