Quick thoughts on computer-verified proofs

[sniffnoy]

So apparently there's now a computer verified proof of the Kepler Conjecture.

Obviously computer verification is now becoming a "thing", with homotopy type theory and Vladimir Voevodsky pushing it and all that. (I still have no idea why there is topology involved.) Not much of a thing, mind you; people still aren't doing it a whole lot. But they're talking about it like it's actually a thing that could happen, rather than something totally impractical, and some people are actually taking steps to make it possible. So writing proofs formally as a routine thing just might be a possible future.

But that's not what I mean to focus on right now. Right now, computer-verified proofs basically only seem to happen in two cases:
1. People who are trying to push computer verification, and so are building up a library or showing off an example
2. There is actually some amount of uncertainty about a proof.

And I mean, this latter is a bit funny, because it means that computer verification is to a large extent starting with the *hardest*, most complicated proofs!

And, like, for computer verification to ever really catch on, there are going to have to be libraries of formal theorems for use. And the people writing these computer-verified proofs to a large extent presumably don't yet have those to go on, except for the most basic things, instead writing them themselves.

So I wonder if this is how things start -- libraries getting written to do something complicated and horrible, and only *then* getting used to do the ordinary.

(This leaves me with visions of math having some of the problems programming currently has -- libraries with horrible interfaces that everyone uses anyway because nobody wants to rewrite it, or they can't get anyone else to use it... I don't know, I think the nature of mathematics would serve to mitigate that effect.)

-Harry

Comments

[grenadier32.livejournal.com]

One thing I've learned after several years as an engineer is that a tool or library has to be used and tested by multiple people with multiple use cases before it can be reasonably recommended for lots of people. It's easy to think "oh yeah, this works great, I should release this for other people!" and then when someone else tries to use it, they quickly discover that it was written to scratch some specific itch, and is poorly factored for anything else.

[sniffnoy.livejournal.com]

Yeah, "poorly factored" is exactly what I'm worried about. But like I said, I suspect it may be hard to factor things quite so terribly in math. Well -- we'll see, I suppose.