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

171–180 of 275 posts

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

#171

Post by Retra »

zakk wrote: post #127
avip wrote: post #14

Earlier quoted context omitted.

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.

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?

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

#172

Post by n_t »

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…

Usually grad level courses were about reading research papers. And many times the exercise is to read the paper, try to predict what next para or page will be about and even try to find faults, even though there might be none. I assume Math department does the same.

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

#173

Post by stallmanite »

rocqua wrote: post #105
mrob wrote: post #57

Earlier quoted context omitted.

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

Maybe a default path through the document could be specified by the author or by convention

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

#175

Post by captain_perl »

wtallis wrote: post #117
dogecoinbase wrote: post #108

Earlier quoted context omitted.

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.

Dislike, sure. Personal preferences are acceptable. But claiming that it's impossible for a computer/tablet display to be as readable as paper and that all electronic displays cause more eyestrain is unreasonable. Especially when the person making that claim has already demonstrated that they are familiar with terms like resolution, contrast ratio and form factor, but they fail to even propose a hypothesis for what m…

Mathematicians are happy to use computers for typesetting papers, but not for the initial creative phase:

1) computer displays require you to scroll, which interrupts your mental flow

2) paper and pencil or pen is free-form

3) in advanced mathematics, results are rarely calculated in numerical form, so the computer isn't helpful

4) notebooks are permanent. No backups needed.

I imagine the same is true for most cartoon artists.

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

#176

Post by cxseven »

cycrutchfield wrote: post #26
peq wrote: post #21

Mathematicians should do more computer verifiable proofs to avoid discussions like this. > Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.” This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.

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…

For the Kepler Conjecture, human mathematicians first found a way to show that it could be proved by checking a finite (but long) list of computer-verifiable claims.

Here Scholze is saying that part of the proof simply hasn't been written, so there's nothing to verify. I think he's missing that computer verification proponents are also aware of that and are either

1. trying to motivate the camp that claims to understand Mochizuki's work to formalize and computer-verify it

and/or

2. suggesting that some of the gaps can be filled in by automatic theorem provers

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

#177

Post by lacker »

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…

I don't really understand why the entire known mathematics is not automatically proven yet.

I think the problem is that this would be a significant amount of programming and data entry work, and there's no incentive for anyone to put in this work. There are many important math papers that are written at a level that is enough for a human math professor to understand, but not for a symbolic mathematics program to understand.

Since math research is generally prioritized by other math professors, and the current system of publications is optimized for math professors to read, they have no incentive to convert to a "formal language proofs are what matters" model. And there is no real financial incentive for computer programmers to implement something like this if math professors don't want it.

At the end of the day, what is the benefit of formally proving mathematical theorems via computer? If the only people consuming math proofs are other mathematicians, the only point is to check that you haven't made a mistake, which is useful but perhaps not worth much investment because the current system already does okay at catching mistakes.

If you could actually develop new mathematical research more easily with computer assistance, then I think these formal methods would be quite valuable, but I don't see how that would happen.

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

#178

Post by jamesrcole »

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 term "proof" seems to be a lot of the problem, because it implies something definitive.

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

#179

Post by thrmsforbfast »

throwawaymath wrote: post #162
thrmsforbfast wrote: post #149

Earlier quoted context omitted.

> That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on." THIS is the real reason more mathematics isn't computer-checked. You massively buried the lede. >…

> 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 button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions.

> 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

No.

Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals.

If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand.

If I want to prove something arbitrary about real closed fields, I can press a button and go for a run.

Computers are much better at proving things about real closed fields than they are at proving things about integers!

> I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.

One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms.

This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)

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

#180

Post by wtallis »

abenedic wrote: post #168
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.

> 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 somehow harder on your eyes than an indirectly-lit piece of paper, then you should be trying to figure out whether you simply have the backlight set too bright for your surroundings, or if your screen's contrast ratio at reasonable brightness levels is inadequate. Your LCD's default settings are probably optimized for movie-watching more than reading, but that's easily fixed and definitely not an inherent limitation of all backlit displays everywhere.

Post reply on HN