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

231–240 of 275 posts

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

#231

Post by Jweb_Guru »

Retra wrote: post #169
resters wrote: post #111

Earlier quoted context omitted.

What is the painful part? The level of detail required for it to check?

The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prov…

Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).

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

#232

Post by alimw »

singularity2001 wrote: post #210
Retra wrote: post #169

Earlier quoted context omitted.

The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prov…

Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?

You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.

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

#233

Post by thanatropism »

jedharris wrote: post #200
thanatropism wrote: post #91

Earlier quoted context omitted.

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

Again, the goal is not to convince, but to understand. Thus the ubiquitous "proof is left as an exercise for the reader".

To extent that mathematics is a science, the whole point is to understand. Of course, people time and again have succumbed to the feeling that (e.g.) numbers are divine, but there's nothing mathematical about that.

---

It's not like it has been established as a mathematical theorem based on simpler ontological facts that capital-T truth exists. And everything in our daily experience points out to the contrary.

That fact that computers and programming languages have evolved from XOR and NAND semiconductors says a lot about the power of a particular branch of mathematics; it says nothing about the nature of mathematics. That idea is like claiming that the existence of probability theory implies that mathematics is about reasoning with uncertainties.

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

#234

Post by rofo1 »

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…

Which topology books contain prose, in your opinion?

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

#235

Post by rofo1 »

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…

Here's another "not sure if correct proof": Jordan's theorem!

Seemingly "evident" result, extremely difficult to prove in some cases (e.g. continuous, nowhere differentiable function etc.)

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

#236

Post by shoo »

Smaug123 wrote: post #98
barbecue_sauce wrote: post #64

Earlier quoted context omitted.

You have an MSc in mathematics but don't consider yourself an expert?

Where high-school mathematics was analogous to learning to form letters with a pencil, undergraduate BSc mathematics is analogous to learning to form words and short sentences. By the end of your BSc in the analogy, you can look at a sentence and recognise at least what sort of genre it might be part of, and you can write down many of the most common words as well as a number of rehearsed useful sentences. An MSc is…

> If you're lucky, you did a research project in which you perhaps rewrote a certain very specific short paragraph in your own words.

Well stated. this pretty accurately characterises my experience of undergraduate studies & an honours year in mathematics

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

#237

Post by proto-n »

zakk wrote: post #199
Retra wrote: post #171

Earlier quoted context omitted.

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…

Except that he doesn't say it is incorrect, he says that "it seems bizarre" to him that seemingly Michozuki's paper doesn't have any uses beyond proving the ABC conjuncture. The rest of this comment is just explaining how it's usually not like this.

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

#238

Post by arunix »

Myrmornis wrote: post #192
Retra wrote: post #170

Earlier quoted context omitted.

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.

What tool(s) do you use for working with LaTeX?

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

#239

Post by zakk »

proto-n wrote: post #237
zakk wrote: post #199

Earlier quoted context omitted.

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…

Except that he doesn't say it is incorrect, he says that "it seems bizarre" to him that seemingly Michozuki's paper doesn't have any uses beyond proving the ABC conjuncture. The rest of this comment is just explaining how it's usually not like this.

When the world's most brilliant mathematician (or at least one of the most brilliant) says "it would be rather bizzarre if your argument worked" the implications are absolutely clear.

As a scientist I would never make such a statement, moreso for a theory I admittedly don't understand.

Tangentially, it's not Tao's case, but I have seen a lot of bullying in the academia along these lines... "I am not saying it's wrong, just very bizzarre", "I am not saying it's wrong, but my Ph.D. student worked on it for two years and couldn't solve it", "I am not saying it's wrong, actually I don't even understand the details, but please recheck everything..." etc...

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

#240

Post by falcor84 »

busyant wrote: post #187
fjsolwmv wrote: post #148

Earlier quoted context omitted.

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.

I love your idea in principle, but it would be very problematic, and very sensitive to the tester's prior experience. I think that many people would (un)naturally be more trustful of mathematically-looking squiggles than a dog's barks, while others, especially if they got burned by damn lies before, would inherently distrust mathematics. In any case, people are very prone to trying to complete gaps in their understanding of a speaker based on prior conceptions.
Post reply on HN