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

91–100 of 275 posts

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

#91

Post by thanatropism »

man-and-laptop wrote: post #66
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…

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 about the internal structure of a piece of mathematics.

The problem with Mochizuki is that he did his work isolated from the rest of the world, so the internal structure of the kind of maths he invented is opaque. Accordingly, what mathematicians are really trying to do is to examine what makes this new maths tick; the books that make this accessible to mathematicians worldwide will not be fully-verifiable proofs of a statement, but webs of separate propositions whose statements are illuminating and whose proofs are easy to understand. If they're really successful, some may even be left as an exercise to the reader.

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

#92

Post by [deleted] »

barbecue_sauce wrote: post #64
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…

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

[deleted]

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

#93

Post by atmanthedog »

ericsoderstrom wrote: post #40
doitLP wrote: post #25

Earlier quoted context omitted.

> We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine" This same could be said of many other professions, medicine and psychology to start. It seems a related manifestation of the Gells-Mann Amnesia.

Math is different in that one feels there should be something close to "absolute truth." That is, given a set of axioms, it is possible to verify with complete certainty whether a proof follows from those axioms or not. Though when proofs become so long and abstruse that only a handful of people can even read them, perhaps that's no longer true. In other fields, it's more clear that nothing is known with 100% certain…

Unfortunately, math doesn't really permit this type of truth: if your axioms are strong enough to prove general statements about arithmetic, there is no effective procedure to determine whether an arbitrary proof follows from those axioms.

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

#94

Post by Moodles »

barbecue_sauce wrote: post #64
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…

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

Haha not at all. My MSc project was about splitting graphs into other types of graphs and some generalizations of graphs into hypergraphs. I don't even consider myself an expert on graphs, let alone number theory.

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

#95

Post by Smaug123 »

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 not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.

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

#96

Post by edflsafoiewq »

westoncb wrote: post #60

> “The abc conjecture is a very elementary statement about multiplication and addition,” said Minhyong Kim of the University of Oxford. It’s the kind of statement, he said, where “you feel like you’re revealing some kind of very fundamental structure about number systems in general that you hadn’t seen before.” I can kind of see that, but there's something in it that gives me the feeling of arbitrariness. It's lookin…

Another way to think about it is to consider what needs to happen for rad(abc) to be much less than c. This can only happen if the "dropping" you mention drops a whole lot of factors. In other words, it can only happen if a, b, and c all contain mostly large powers of primes.

The prime factorization of a number is essentially "random". That makes numbers that are large powers of primes rare; it's like rolling a die and continuously getting the same face. Now if you add two numbers, the prime factorization of the sum does not appear to be related to the prime factorization of the summands, so adding two very rare numbers and getting yet another very rare number seems unlikely. And that seems to be roughly what the abc conjecture says: it is not likely that all of a, b, and c are rare.

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

#97

Post by Moodles »

dan-robertson wrote: post #83
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…

There’s this curious thing in mathematics where most things are either obviously true or obviously false and those that aren’t are mostly inconsequential. Those that remain are certainly more interesting but also typically their proofs are a few obvious steps. Obvious in this case means something like “clear to a mathematician familiar with the field” or “otherwise many things will fall apart” This leads to the situa…

Some fun large counterexamples to conjectures: https://math.stackexchange.com/questions/514/conjectures-tha... So maybe Fermat's Last Theorem etc isn't always obviously true. But I do get your point.

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

#98

Post by Smaug123 »

barbecue_sauce wrote: post #64
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…

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 like reading some examples of long sentences and short paragraphs, and being shown some long paragraphs or even chapters of books (which you have no hope of understanding, but you try, and the experience is salutary). If you're lucky, you did a research project in which you perhaps rewrote a certain very specific short paragraph in your own words.

The job of a research mathematician is analogously then to read and write books.

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

#99

Post by Jach »

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

Someone already linked metamath, it also gives a flavor of just how long some proofs can be when you fully formalize them and start from ZFC axioms. From the trivia page at http://us.metamath.org/mpeuni/mmset.html#trivia "The complete proof of [(2+0i) + (2+0i) = (4+0i)] involves 2,863 subtheorems including the 189 above. These have a total of 27,426 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory."

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

#100

Post by WalterGR »

bollu wrote: post #51
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…

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?

Post reply on HN