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

211–220 of 275 posts

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

#211

Post by ur-whale »

auntienomen wrote: post #126
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.

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…

> Mathematicians digest papers nonlinearly.

That's a fairly weak argument: you can browse an electronic document in a non-linear fashion way easier than a book.

And also: books don't have CTRL-F

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

#212

Post by kiriakasis »

nabla9 wrote: post #52
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…

Formal proof assistants and interactive theorem prover for mathematics already exist. So do proof libraries. See: http://metamath.org/ They are not used because it's tedious to type and proof every step in the process. Mathematicians don't write all steps down. You also need build a library from ground up. We could to the same for computer programs but we don't wan to do that either.

Also I want to add syntax, mathematical syntax is incredibly rich, complex, ambiguous and effective; so much that in some paper it is the hardest part to understand, not always because of bad writing.

At least we are better off than theoretical physicists :-)

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

#213

Post by kiriakasis »

fjsolwmv wrote: post #143
naasking wrote: post #71

Earlier quoted context omitted.

Because most mathematics is not constructive, and most automated theorem proving tools are based on constructive logic.

That doesn't sound right at all. Law of excluded middle is very easily computed with, It's a college homework exercise.

Well, yes because you can embed classical logic in constructive logic in many ways but then you lose a lot of convenience.

The if you had exensionality things get really weird

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

#214

Post by mrob »

wtallis wrote: post #182
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…

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…

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

I'm not surprised. Virtually all "designers" think low contrast text is better, despite high contrast being preferred on paper. They deliberately reduce contrast by setting the text color to gray. Even Firefox's Reader View, which otherwise fixes most mistakes of designers, sets the text to gray unless you override it in userContent.css. Desktop GUIs often have low contrast text too, which is also difficult to fix. Unless somebody somebody knows how to do this their expensive monitor will be wasted.

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

#215

Post by mrob »

Angostura wrote: post #80
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…

Wouldn;t it bump into the same kind of problems that Bertrand Russell's attempts bumped into with the Principia Mathematica? Namely it crashed into Gödel's incomplete theorem? Disclaimer: What I don't know bout maths would fill volumes, in both senses of the word Edit: From the down-votes, apparently not.

Human mathematicians are bound by Gödel's theorem in exactly the same way computer software is. If an informal human-based "proof" does something that would be impossible with a formal software-based proof, then it's incorrect. There is no theoretical advantage to running the calculations on a human brain.

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

#216

Post by dvdkhlng »

onemoresoop wrote: post #73

http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTch-discussions-...

Thanks for the link. As that seems very relevant to the discussion, let me add some context: This is Mochizuki's answer to the recent criticism titled "Report On Discussions, Held During The Period March 15 – 20, 2018, Concerning Inter-Universal Teichmuller Theory (IUTC)"

For TL;DR see around page 40 in that PDF:

> Indeed, at numerous points in the March discussions, I was often tempted to issue a response of the following form to various assertions of SS (but typically refrained from doing so!): Yes! Yes! Of course, I completely agree that the theory that you are discussing is completely absurd and meaningless, but that theory is com- pletely different from IUTch!

> Nevertheless, the March discussions were productive in the sense that they yielded a valuable first glimpse at the mathematical content of the misunderstandings that underlie criticism of IUTch (cf. the discussion of § 3). In the present report, we considered various possible causes for these misunderstandings , namely:

> (PCM1) lack of sufficient time to reflect deeply on the mathematics under discussion (cf. the discussion in the final portions of § 2, § 10);

> (PCM2) communication issues and related procedural irregularities (cf. (T6), (T7), (T8));

> (PCM3) a deep sense of discomfort ,or unfamiliarity ,with new ways of thinking about familiar mathematical objects (cf. the discussion of § 16; [Rpt2014], (T2); [Fsk], § 3.3).

> On the other hand, the March discussions were, unfortunately, by no means sufficient to yield a complete elucidation of the logical structure of the causes underlying the misunderstandings summarized in § 17.

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

#217

Post by roenxi »

ur-whale wrote: post #206
roenxi wrote: post #195

Earlier quoted context omitted.

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

>I can prove Pythogoras' theorem with a diagram I don't think I agree with this statement. As a matter of fact, I've always had a deep unease with so-called "geometric proofs", where a succession of visual transformations of a diagram are used to prove a theorem. You can certain explain the intuition behind the proof of Pythagoras theorem with a diagram, and there's huge pedagogic value in doing that. But to me it is…

scratches head I'm pretty sure I can come up with a codified language proof that you will accept, then define a mapping between the language and transformations of a diagram. And while not an expert on isomorphism, but I'm pretty sure that makes the visual proof isomorphic with the codified language and hence valid (and, indeed, computable).

Basically, although code and proofs are in a sense isomorphic, I think everything and proofs are isomorpic in the same sense. So claiming that proofs should be structured to the same standards as code because code is isomorphic to proof is a bit of a non-sequitur. Why not show the layout of my rock garden is isomorphic to code and hence proving something (my rock garden can be Turing complete) and then claim my rock garden should be structured like a program?

Basically, the idea that the structure mathematicians favour for proofs have fallen behind programmers laying out of code is not well substantiated and the idea that 'proofs are isomorphic to code' is not useful because it is far too broad.

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

#219

Post by Fri21Sep »

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…

The most definitive version of a proof one can imagine is when the proof has been expressed via a formal language and a proof assistant checks that each step of the proof complies with axioms or already proven theorems from a library (which, in this case, are simple rewrite rules in the formal grammar). The [Mizar System](https://en.wikipedia.org/wiki/Mizar_system) is an example of that.

The question of formally proving Wiles' theorem is [discussed here](http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html). Currently there exists no tool powerful enough to formalize such proof. It's considered a challenging problem in computer science.

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

#220

Post by laingc »

doall wrote: post #38
matthewbauer wrote: post #9

I wonder if language is a factor in this at all? I know mathematics is written entirely in English but most likely discussions still happen in local languages. Could part of the proof be lost in translation?

I think Mochizuki won't have any problems with English, since he spent his school days, up to PhD in the US. https://en.wikipedia.org/wiki/Shinichi_Mochizuki About Hoshi, I have seen him in a conference video before, and have an impression that he isn't good at English, which can make a bit difficult in discussion. I don't know about Scholze and Stix.

Scholze has a strong accent, but speaks flawless, sophisticated English.
Post reply on HN