Comment by bumbledraven | Hacker News Reader

Comment by bumbledraven | Hacker News Reader

The usual maneuver by which mathematicians leverage that formal notion to capture the arguments they, and all their colleagues, regard as proofs is to say a proof is a finite sequence of assertions that could be filled in to become one of those formal structures. It’s not a bad approach if the goal is to give someone a general idea of what a proof is. The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical.

False. What is "hypothetical" about this formal proof that the reals are uncountable? http://us.metamath.org/mpegif/ruc.html

Each step is clickable, and just a few clicks take you back to the axioms. For more, see chapter 1 of the Metamath Book (http://us.metamath.org/downloads/metamath.pdf)

How is it that Devlin is unaware of logical systems like Metamath? It's at least 10 years old. [Edit: Maybe 20 years? http://us.metamath.org/copyright.html says "The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software."]

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. The example you gave is the sort of proof presented to bright high school students - I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it.

Where proof assistants are used, they're frequently totally counter to the style of thinking traditionally taught in mathematics and computer science - I've heard them described by experts in the field as 'proof obstructions'.

I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) [].

which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose.

I can imagine that this would be a massive turn-off for almost any research student.

I also think that his line

(it almost certainly is not, but more pertinent, how could you ever be sure it is?)

is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high.

> I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it.

And then save time because you can be sure that the proofs you write are correct.

> I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) [].

> which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose.

Did you try isar?

> I also think that his line

> (it almost certainly is not, but more pertinent, how could you ever be sure it is?)

> is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high.

It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel.

> And then save time because you can be sure that the proofs you write are correct.

For better or worse, we both know that's not required to be a successful mathematician. I remember reading a presentation from a guy advocating mechanised proof who realised that almost every important proof in his field had been later shown to be false.

> Did you try isar?

I had a go at using Isabelle (in general) and truthfully never really got onto Isar - I discovered that both my supervisors have written large theories in HOL4 (JIT compilers etc), but have no recent experience with Isabelle, so that's what I'm using. I've seen examples of Isar which look nice, but I'm skeptical about its scalability. You make a good point, thouugh.

> It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel.

Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it.

If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure.

Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based example, but that's merely due to my being ignorant of most pure mathematics - there are probably analogues.

This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical.

[1] - http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/44-...

> For better or worse, we both know that's not required to be a successful mathematician. I remember reading a presentation from a guy advocating mechanised proof who realised that almost every important proof in his field had been later shown to be false.

Some professors I know told me something along those lines about various topics of mathematics. The more advanced the topic gets the less people cope with the complexity. In the end it gets so specialized that only a few people in the world can and are willing to follow the advance. That situation combined with human notorious fallibility brings mathematic research in a very bad situation.

I makes me sad - and angry I have to admit - that the professors I met don't recognize computer-aid as the solution. Besides that I personally had the most pleasure doing mathematics while being guarded by a computer against my stupidity[+].

> Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it.

> If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure.

> Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based

[+] You raise a good point. The computer can't do all the work. Nevertheless it's a huge advance to only have to verify the definitions and theorem statements instead of all that combined with the proofs. It's like having to remember the summary of a book instead of the whole book. Someday we will hit a wall even when using computers but that shouldn't stop us know.

> This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical.

Thats awesome! Nice problem to work on. Stories like this keep my dream alive that there are interesting workplaces in this world.

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident.

His point was that formal proofs are "hypothetical", not that they are rarely encountered. What part of

> The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical.

don't you understand?

I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. which has no real relation to any normal thought.

The syntax you describe bears very little relation to formal system like Metamath in which proofs are readily checkable by people and machines.

I also think that his line (it almost certainly is not, but more pertinent, how could you ever be sure it is?) is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it.

No. Metamath proofs can easily be verified by hand.

Similarly, many programmers go their entire careers without touching assembly language or logic gates, yet we all know that our programs can be (and are) distilled down to this. There are definitely people that worry about this, e.g. compiler writers and mathematical logicians, but to most of us it just isn't that important. In addition, it's an abstraction that leaks fairly infrequently, and so far we haven't observed it in the way you're implying; the most prominent "leaks" of mathematical logic are likely unprovability or having to accept stronger axioms to prove a particular statement (e.g. Choice or maybe Grothendieck-Tarski).

Addendum: the above is mostly tangential to the original article. The author is very correct that a modern mathematical proof exists, and is formulated to, show another person with suitable background how to work out the truth of a statement. But don't let this form of proof distract you from the existence of the foundations of rigorous proof in general; just as we don't let Ruby's English-like syntax convince us that we aren't truly executing computation. The foundations of mathematical logic are complex, like the transistors on a microchip, but they do "work," in the strongest epistemological sense of the word.

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident.

I find that difficult to believe. My basic math courses in college taught proofs using axioms, starting with really basic stuff like proving that the product of two even integers is an even integer. I don't see how anyone with a mathematics degree could miss that, or could do much useful work without that.

You are right in stating that what he is saying is false.

There are a lot of proofs written with assistance of Coq or Isabelle/HOL that can easily be extended to include each and every logical step.

That he said what he said saddens me a lot. Machine-checked mathematical proofs are the future of mathematics and most mathematicians I know are totally ignorant about them.

He's clearly not ignorant of computer assisted proofs, but I also wish he'd show more enthusiasm for them.

https://www.maa.org/external_archive/devlin/devlin_01_05.htm...

Given the software engineering tools available in 1976 (and again in 1994), can you offer a defensible reason he should've been more enthusiastic?

I think Metamath was available in 1994. (http://us.metamath.org/copyright.html says: The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software.) And even if Devlin wasn't aware of it (or systems like it) back then, what's his excuse now?

What does 1994 have to do with it?

Homotopy type theory as a framework for doing proofs is exciting. Vladimir Voevodsky had a talk somewhere on youtube in which he claimed you could get similar length proofs in Coq using HoTT as you could on paper. He's also excited about the prospect of most math papers publishing machine-checked proofs.

I wish I could find the exact video for you.

> He's also excited about the prospect of most math papers publishing machine-checked proofs.

Apparently the feels he can't be sure of the correctness of his own papers without machine checked proofs anymore, and he's a Fields medal winner:

I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct.

But I think that the sense of urgency that pushed me to hurry with the program remains. Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure

(from this http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...)

Vladimir Voevodsky may feel that way, but we were talking about Keith Devlin.

To answer gre's question, 1994 is the year Devlin cites a major breakthrough in the four color problem, in the very link that gre cited as an example of Devlin's lack of enthusiasm about machine checked proofs.

There are plenty of good reasons to mistrust machines when it comes to mathematical proofs, and mathematicians have been correct in their skepticism. Most of the work in Univalent Foundations has been directly aimed at addressing that skepticism. Optimism from its proponents in the 2010s is just as valid as the skepticism in the 70s and 90s.

And I mean just as valid in a very specific way; specifically in the spirit of the originally linked Devlin post published today.

I'm excited about HoTT, too. If anyone has demonstrated a short proof of the four-color map theorem in Coq, that would meet Devlin's criteria for convincing machine-checked proofs.

(Check the link you cited; Devlin mentions 1976 and 1994 as key milestones for machine-checked proofs)

But HoTT and Coq are both still new, particularly when speaking of mathematics. When they figure out how to make LaTeX produce their textbook in a fully MathML-compatible fashion, then we can talk. :)

This is a good talk to show to those mathematicians. Machine checked proofs are way too powerful to ignore.

https://www.youtube.com/watch?v=zmhd8clDd_Y

As your cousin post notes, Devlin isn't ignoring "machine checked" proofs.

The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Otherwise, they'd be software engineers (which Devlin hints at in this essay).

The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician.

Maybe Devlin should first stop denying that humans can write proofs that can be both human- and machine- checked. Then we can talk about whether machines can write those proofs.

Humans can definitely write proofs that can be checked by humans or machines. It's arguing in bad faith to suggest that mathematicians are un-qualified to determine the validity of a machine-checked proof.

There are certainly some stodgy holdouts that will never be convinced, but I don't think Devlin is one of them.

I wasn't suggesting that Devlin was ignoring them, I was responding to my comment's parent that mathematicians he knows are ignorant of them, which I tried to make clear by saying "those mathematicians".

>Machine-checked mathematical proofs are the future of mathematics

I don't disagree.

>most mathematicians I know are totally ignorant about them

Most of them realize that this is a possibility but believe, rightly or wrongly, that they are not going to be relevant in their lifetime.

Interesting. I've thought about this exact topic before and I think his point shouldn't be dismissed so lightly.

What got me thinking about this was an occasion (years ago) when I read a proof in which I didn't understand the jump from one assertion to the next one. It occurred to me then that the atomicity in these proofs (on which the entire structure stands) boils down to steps which are considered to be obvious. However "obvious" is a relative term, not an absolute one. So, at least as most proofs are concerned (and most proofs are not machine generated), his point is valid.

As for systems like Metamath - how rigorous are the proofs that the software is bug free ?

If you really want to philosophise over this, I'd even suggest that ultimately one can't really prove anything. At most, you can believe some assertion is correct to the degree you trust your senses, memory and logic - but I'll stop before this devolves into metaphysics...

As for systems like Metamath - how rigorous are the proofs that the software is bug free ?

The formal system itself is transparently simple. You can easily verify the proofs by hand. Also the system has been reimplemented in several languages.

Metamath gives 25,933 steps in proving that 2+2=4. http://us.metamath.org/mpegif/mmset.html#trivia

Reply on news.ycombinator.com