The next generation of proof assistants: ten questions

Checking for new stuff on Freek Wiedijk’s home page I stumbled upon slides of his recent talk given at the Workshop on Logical and Semantic Frameworks in Natal, Brasil. He poses there ten questions about how the next generation of proof assistants should look like. In this post I want to give my answers to those questions.

Should the next generation of proof assistants be based on ZFC set theory?

Short answer: yes, of course. Long answer: no, why would we want to limit the proof assistant to one foundation? The next generation of proof assistants should be generic enough to be able to support many logics. Isabelle is like that now and so is Metamath. As the standard foundation for modern mathematics ZFC should be well supported, but alternatives may be interesting for purposes other than pure mathematics or just for experimentation.

Should the next generation of proof assistants have an advanced type system?

One possibility mentioned in the slides where types are a layer on top of an untyped foundation is probably the best idea. Having some type system would simplify proofs of facts about how set membership changes when functions are applied. In IsarMathLib proofs of such facts have to be done explicitly (using standard Isabelle’s apply_funtype lemma). It is not difficult but repetitive and boring.

Should the next generation of proof assistants take partiality seriously?

To be honest, I don’t understand the question. One remark however: I don’t think the statement 1/0=0 is disprovable in Metamath as Wiedijk claims. In ZF set theory the situation is  that to define the value of a function at some point of its domain we first define what is the image of a set by a function. Having that we define the value of the function at  x as the union of the image of \{ x\}. If f is a function and x is in its domain then the image is a singleton and the union extracts its only element (recall that \bigcup \{ y\}=y in ZF). When x is not in the domain of f however, (like zero is not in the domain of division), the image of \{ x\} is empty and so is its union. Thus f(x) is the empty set, which is zero of natural numbers. So in a way, you can prove that 1/0=0 (except that zeros on the right and left hand side are typically different things). I write some more about that in another post.

Should the next generation of proof assistants take category theory seriously?

Category theory can be done based on ZFC (with some additional axioms) and there is some work on formalization in Isabelle/HOL. However, the question is, can we treat category theory as foundation which we use to formalize mathematics?  I would really like someone to make a serious attempt at implementing category theory in some proof assistant starting from its axioms and proving some typical theorems. Both failure and success of doing so would be very instructive. Until that happens, my answer is no.

(Btw, there is an interesting discussion on Math Overflow about the role of the Replacement Axiom in category theory. Some people think it’s necessary, others find its consequences unacceptable. It seems that there is some overlap between those two sets (categories?) of people. This is similar to the situation with the Axiom of Choice in set theory some hundred years ago. )

Should the next generation of proof assistants be based on a logical framework?

Yes. The reasons are well explained on the slides.

Should the next generation of proof assistants have a self-verified kernel?

I don’t think it is essential. It would be good if the core system was short enough to be convincing to humans (like Metamath is) and possible to verify by hand. That is the important part. The self verification is not worth much – as Wiedijk notes “if it is incorrect it can falsely claim to be correct”. In addition, there is some design tension between building a system for doing formalized mathematics and software verification. These tasks are similar in theory, but quite different in practice from the user perspective. If we want a better proof assistant for formalized math (and I do), we don’t want the designers to focus on software verification.

Should the next generation of proof assistants be programmed in itself?

It would be better if it was not. The reasons are explained in the previous answer.

Should the next generation of proof assistants be competitive with commercial computer algebra?

Probably not. Maybe next after that.

Should the next generation of proof assistants use a declarative proof style?

Yes. But the most important is not how the proofs are written but how they look like after being processed by the presentation layer. I think this is the killer app for formalized mathematics: having a faithful semantic representation of mathematical knowledge in a machine that can be studied by humans. “No mystery” hyperlinked proofs that can be searched, viewed at desired level of detail and refactored. Imagine the possibilities.

How should the next generation of proof assistants be arrived at?

Better question is how can they be arrived at. I don’t know the answer. Such things typically come from academia. The problem is that the products of  Computing Science departments (where the knowledge necessary to create the NGoPA is)  are biased towards software verification, thus can not improve in the “better match with existing mathematical culture” area. Mathematics departments are simply not interested in formalized mathematics.

I have a fantasy sometimes that a very rich person just throws a large amount of money at the problem for pure love of mathematics. Something like that did happen for poetry, so why not for formalized mathematics?

About these ads

Tags:

6 Responses to “The next generation of proof assistants: ten questions”

  1. Omar Says:

    “Btw, there is an interesting discussion on Math Overflow about the role of the Replacement Axiom in category theory. Some people think it’s necessary, others find its consequences unacceptable.”

    That second sentence is not true at all! I don’t think anybody “finds its consequences unacceptable”! The situation is more like this: a) some find the consequences of NOT having replacement (while keeping the current definitions) unacceptable, b) there is a way to keep some of the nice properties replacement gives by changing the definitions but many people find the changed definitions unsatisfactory, c) many people did not realize some of the arguments they made relied upon replacement.

  2. slawekk Says:

    Thanks for clarification. Indeed, I misunderstood the motivation behind some people trying to find alternatives to replacement.

  3. Ramana Says:

    Did you extrapolate the content of this talk from the slides, or did you also find some paper or have a discussion with someone at the talk? The slides and your response are already interesting though :)

  4. slawekk Says:

    I did not attend the talk. I only read the slides. I don’t think there is a paper about the talk other than the slides.

  5. Alex Says:

    Regarding “foundations and category theory”, one of the really beautiful things that category theory does (but I don’t think any theorem prover currently could do) is to “internalize” concepts — see the nLab on this one http://ncatlab.org/nlab/show/internalization

    It’s beautiful, in that e.g. a group object internal to the category of topological spaces is a topological group; and one internal to the category of differential manifolds is a Lie group. Any theorem proved about a group object in any category C is passed on to these specific “subtypes” of groups.

    What would be interesting is categorification…but I digress.

  6. Untyped formalized systems are wrong « Victor Porton's Math Blog Says:

    [...] Kolodynski converted me into his religion of doing formalized math with Isabelle/ZF and answering “yes” to the question “Should the next generation of proof assistants be…, but now I [...]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


Follow

Get every new post delivered to your Inbox.

%d bloggers like this: