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

201–210 of 275 posts

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

#201

Post by ur-whale »

To me, this article highlights two things: - the sore need for a way of automatically verifying proofs. - the sore need for a formal, agreed-upon language in which math proofs can be written.

The language of math has always been much more mushy than mathematicians are willing to concede, and the chickens are coming to roost: 21s century math has become so complex and sophisticated that very few people can actually even read the content of proofs, much less understand them.

Shinozuki's case is an extreme example of that: after almost ten years, even he other experts in the field aren't sure of what he's saying.

There is a clear need for formalizing the language of mathematics in a way that allows machine to verify he validity of a proof.

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

#202

Post by ur-whale »

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

The fact that encoding Math proofs in a formal language is currently painful is well acknowledged.

However, it shoudln't deter us from the goal.

People used to code in assembly and Fortran. It was and still is quite painful.

But programming languages have improved, and resorting to those original languages (which is what Coq is) is rarely necessary these days.

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

#203

Post by kiriakasis »

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…

Actually latex would be quite sufficient, basically what you are proposing is an appendix where you list additional details

The real reason people don't do this is simple, it would require an inhumane amount of work and details which will likely be wrong themselves and will for sure be to boring to be checked. Most science is wrong in some aspects, sometime it is better to have a meaningful intuition that can be understood by other expert (and maybe rejected)

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

#204

Post by ur-whale »

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…

There is a big difference between explaining / teaching a proof and verifying its correctness. We're talking about the latter here.

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

#205

Post by mrob »

lacker wrote: post #177
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…

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

Formal proofs increase trust in mathematics. E.g. Fermat's Last Theorem is supposedly true, but I can't understand the proof. I have to trust the mathematicians who say the proof is correct, and I know that in other fields (most notably with the replication crisis in psychology) people accepted things as true when they weren't. If I had a formal proof I could run it through a theorem checker and see that it was correct, and I could use multiple independent implementations of the theorem checker for more confidence. If I'm using human mathematicians as black-box theorem checkers, I don't have the option of using multiple independent implementations, because all mathematicians work with other mathematicians, so it's possible that they're just agreeing with each other's mistakes. With the software I also have the option of examining how it works, all the way down to transistor level if I want to.

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

#206

Post by ur-whale »

roenxi wrote: post #195
zbobet2012 wrote: post #67

Earlier quoted context omitted.

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint. The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is t…

> 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 isn't a formal proof until it has been codified in a language that a computer can walk from start to end making sure each step is valid.

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

#207

Post by jedharris »

jamesrcole wrote: post #178
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.

Excellent point. What mathematicians write to each other are arguments not proofs. Machine checkable proofs are really proofs.

This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and proofs can be improved. Tools for each can be developed without having to support both.

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

#208

Post by kiriakasis »

vbezhenar wrote: post #198
FabHK wrote: post #86

Earlier quoted context omitted.

> 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 like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.

That was exactly the point, if you abstract then you are handwaving details (unless you abstract inside a formal system that itself defines methods for abstraction and then you are back to square one)

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

#209

Post by yesenadam »

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.

I've started doing everything in LaTeX - diary, everything I'm learning about, books I'm writing, maths, documenting my programming etc - the last few months too; it's going great. It took a few months to learn about LaTeX packages, basic TeX etc. (And every time I use TikZ I've forgotten it all again..) It's especially useful mathematically in avoiding errors when doing page-long calculations with pen and paper - copying lines instead of writing them out, and the whole thing looking so lovely and neat - eliminates 95% of the errors I made before, and it's faster. I still do ideas, sketches etc on paper, but anything that's likely to be want to be kept goes straight into LaTeX.

But also..all my favourite books have markings on each page, margin comments, turned-over corners etc. Any pdf book I read more than once or twice, I'll get a paper copy, I think.

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

#210

Post by singularity2001 »

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…

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?
Post reply on HN