This is well worth reading for anyone interested in how mathematicians think about proofs.
It makes a great counterpoint to Lamport’s paper, posted earlier:
If you’re a formal methods person, especially one with a CS background, who feels the urge to complain (like so many do) about how mathematicians don’t want to use Coq or Agda or Isabelle or Lean or whatever, go read this first. And reflect on it.
As a non-mathematician, the Lamport paper just looked to me like he was bringing the modularity in programming to proofs. This work is also modular. Both allowed expanding on or ignoring specific pieces of proofs. Lamport concluded thinking computer scientists would create better ways of doing structured proofs. So, what made you see this one as a contradiction to the earlier one?
I agree with your other comment. Fortunately, there’s at least a little work on human-centric provers. Maybe it will grow later on work like in this paper get out there.
Not a contradiction, just a different perspective. And a much more mature and effective strategy: rather than trying to change established practices, Ganesalingam and Gowers embrace and try to understand them – and only then attempt to contribute something. As an automated theorem prover, their work is nothing special. But as “UX” it’s way ahead of the pack.
I think that the important idea here is that a mathematical proof is an explanation. It must be fully convincing, but that doesn’t mean every detail must be spelled out down to axioms. The mainstream culture of mathematics places value on “elegant” proofs and rejects tedious or pedantic ones. There is a highly developed culture of nuanced abstraction in mathematical writing, and it’s not going away just because computers (and the specific notions of modularity that programming languages have developed) showed up on the scene. A mechanized proof that satisfies a program but yields no human insight is just not interesting to most mathematicians: they value insight above rigor. Maybe you have different values, but that doesn’t give you the right to impose them on others. Progress will be made not by conquering, but by reconciliation.
As I see it, this isn’t really a human vs. machine thing, it’s about cultural values. After all, it’s humans on both sides here: one side is much newer, much smaller, and happens to place more emphasis on machinery. The culture of proof in computer science owes much to logic, and in particular the early 20th century work on “foundations” – a largely failed (and perhaps misguided) project from the perspective of most of modern mathematics. (And please, lets not even get into constructive vs classical logic here!)
Like I always say, if you care about this stuff, start reading in the history and philosophy of mathematics. (and by “you” I mean anyone reading this, not just Nick!)
A couple of good (and accessible) starting points:
“Ganesalingam and Gowers embrace and try to understand them – and only then attempt to contribute something. As an automated theorem prover, their work is nothing special. But as “UX” it’s way ahead of the pack.”
Thanks for the explanation. That confirms some intuition from the Wired article I had on human vs mechanical proofs. It sounds like what they’re doing is similar to Richard Gabriel’s essays for IT or marketing theory in general where it’s better to identify the bandwagons with huge momentum to find ways to attach ones’ own ideas to them. The computational verifiers have been going against momentum by doing stuff in such a different way that current field of human proof says, “Uh, that’s not what we do. Are you sure you’re in the right room with those ideas?” Whereas, this work starts with their methods, then creates computational equivalents where possible, and shows how they can benefit them without changing much of what they’re doing.
Yeah, I’d say that’s an approach that will win over a lot more mathematicians if any can at all that is. Not to say we can’t do both as we see with program verification field getting lots of practitioners and results. It’s just they’ll remain separate unless people start doing program verification in a way closer to how mathematicians think. I’m not sure that’s going to happen since problems from high-level representations mismatching low-level implementations are why they took current approach to begin with. There’s some potential, though, when using algebraic or state models given it was done in the past knocking out lots of problems.
There’s also already methods being developed to convert the high-level stuff into equivalent low-level stuff like Imperative/HOL or the ceritfying compilers for proof assitants. Might be possible to grab some extra mathematicians into formal verification if they can do human-centric proofs on high-level algorithms with the transformation tools doing the rest to let them avoid tedium or steps computers do better. Anything really interesting they come up with would likely be duplicated later by people in the program-centric side of things.
Just speculating there since I’m too distant from the practice to know for sure. I’m probably going to have to learn (or attempt to learn) the methods of mathematical proof in the future to get better at my meta-explorations of these issues. I was looking for easy books on it based on recommendations by folks on places like Hacker News. I bookmarked your two. Here’s the others I that popped up a lot in discussions which had good reviews for newcomers in case any of you have experience with them:
Concepts of Modern Mathematics by Stewart
Introduction to Mathematical Reasoning: Numbers, Sets, and Functions by Eccles
A few people also recommended How to Prove It by Velleman though most didn’t say it was for newcomers. Maybe one or two said it was with most just claiming it’s helpful for understanding proof.
I bring these up because I like to collect resources that I can pass on to lots of people to bring them in these sub-fields. People learning invariants and such seem to have hardest time with initial concepts of formalizing ideas into math form. Then, the proving gets them after that. Ideally, I’d have one to a few books (less quantity/cost the better) to use myself and/or recommend to others that cover those really well. Once they get those concepts, the rest might come more easily. Especially the simpler specifications or proofs used in stuff like SPARK Ada given it’s mostly Boolean and first-order logic. Optionally, they can work from there to learn either human- or machine-oriented proving with greater complexity.
EDIT: Went ahead and bought these to review them myself. If I can’t use any one, I’ll just donate it to library or give it to someone more mathematically inclined to further their development.
This changes everything. So many mathematicians have carte blanche ignored provers despite their obvious utility. I think it’s mostly because the adjustment pains are simply too great to find them useful.