Translating proofs between proof systems

Stream: new members

[Benjamin]

It seems like a lot of work is duplicated proving theorems between different proof systems. Is it possible to create bridges between proof systems, allowing proofs from one to be used in the other? I can think of two ways this could be done. One would be to make a program that compiles proofs from one language into the language of another, but this may be hard because each proof system organizes its theorems and axioms differently. Another way would be to prove that anything that some other program verifies is true. But maybe this would be just as hard as manually re-proving everything of importance.

I can't be the only one to have this idea, so is there any consensus that this wouldn't work, or any progress realizing this goal?

[Johan Commelin]

People are actively working on this, but so far there aren't many bridges that get actively used.

[Johan Commelin]

@Mario Carneiro has shown that we can use all of Metamaths set.mm in Lean, if we build a little bit of glue.

[Johan Commelin]

The downside of these bridges, is that they need to be maintained. And both sides of the bridge need to work on this.

[Johan Commelin]

For example Lean's mathlib is growing rapidly, and we don't care about backwards compatibility at all. If people want to build a bridge to use mathlib in other programs, this must be a royal pain.

[Jasmin Blanchette]

There are quite a few papers about all sorts of bridges, and tools like Dedukti. To the best of my knowledge, nothing of that really works in practice, and there are lots of obstacles.

[Jasmin Blanchette]

I think it can be done if you want to import a really big theorem (small statement, big proof), but hardly for entire libraries, which is what people care about usually.

[Patrick Thomas]

Is it a matter of standardization or incompatible proof systems or something else?

[Mario Carneiro]

Incompatibility of the logic is not usually a big problem. Non-idiomaticity is the biggie

[Mario Carneiro]

I think it's a surmountable problem but it requires a bit of social buy-in

[Mario Carneiro]

people have to actually care about how their theorems are presented in another language

[Julian Berman]

(Sorry if this is a very bad question, but) at some level do theorem provers (Lean specifically I guess) manifest some fully inlined verifyable thing, without lots of importing and hopping around? Presumably having some sort of transactable serialized form of that fully verifyable thing is a possible step on this path? Or further, is it a sensical question to ask whether that fully inlined thing could be defined in terms of some intermediate language kind of like bytecode on a VM, and then at least there's a stabler layer than the "user-facing" mathlib API (or every theorem prover's specific API) on which you can transact across different environments?

[Bryan Gin-ge Chen]

You might be interested in this page on Lean's export format: https://github.com/leanprover-community/lean/blob/master/doc/export_format.md

[Julian Berman]

Aha very interesting! Thanks.

[Jasmin Blanchette]

Some slides I presented in 2016:
dagstuhl2016-proofs.pdf

[Jasmin Blanchette]

Explanations:

1. Flyspeck (by Hales et al.) was originally spread over three systems. They ended up redoing the Coq parts in HOL4 and never connecting HOL Light and Isabelle/HOL, even though the logics are very close and even though there exists some bridges (including a fast one by Kalizsyk and Krauss).

[Jasmin Blanchette]

1. I don't know exactly what the obstacles are to connecting the HOL Light and Isabelle/HOL proofs, but apparently the bridges can't do it.

[Jasmin Blanchette]

2. Although HOL Light has lots of analysis libraries, to be useful in Isabelle one has to be able to generalize it beyond reals, to use type classes in an idiomatic way, fit in with the rest of the library.

[Jasmin Blanchette]

3. I had a student whom I wanted to develop proofs for me. I wanted him to develop idiomatic, well-indented Isabelle proofs that can form the basis for further development and generalization.

[Jasmin Blanchette]

3. A "proof market" approach, by Dale Miller et al., where bidders offer to solve the proof obligations for you in any system, would have been completely uninteresting to me.

[Jasmin Blanchette]

In short, I think whole-theory translation tools, at the level of proof calculi, as envisioned by Dowek and Miller, are not practical for a wide range of scenarios that interest me and hence the wrong thing.

[Jasmin Blanchette]

On the other hand, ad hoc tools that adapt HOL Light syntax to Isabelle/HOL are already used by people like Paulson and are actually useful and save time.

[Jasmin Blanchette]

In the end, it boils down to "non-idiomaticity" as Mario pointed out, but I thought it would be worth spelling out what that can mean in practice.

[Jasmin Blanchette]

There's also the following question: Suppose you want to use SomeCoqLib in Lean. Do you want to have a bridge so that you effectively link against SomeCoqLib (just like a Python program can link against a C library) or do you want to port SomeCoqLib to Lean and then modify it in Lean? In the former case, what do you do if you need to generalize SomeCoqLib? Lean Coq? In the latter case, you miss out on new SomeCoqLib features, and you have to deal with the clone -- but at least you can do what you want with it, and make it more native.

[Julian Berman]

The FFI metaphor is interesting

[Julian Berman]

As are the slides of course, thanks for sharing. Especially on slide 8 I wonder how different proofs are than other kinds of software there?

[Julian Berman]

(In terms of most proofs being append-only and not modified). For "well defined/have-good-interface" parts of software libraries I don't know that that's quite so different either, people don't heavily refactor them

[ZY Cao]

Yes, I opened a tutorial project, and still have the same issue

[Jasmin Blanchette]

As I see it, the difference between software and proofs is as follows. In the Flyspeck case, they proved $A$ in Isabelle and $A' \to B$ in HOL Light, where $A$ and $A'$ are morally the same but use symbols defined in different systems (e.g. Isabelle division vs. HOL Light division).

[Jasmin Blanchette]

If this were software, you'd create bindings: You'd just say: Division in Isabelle = division in HOL Light, etc.

[Jasmin Blanchette]

and then you'd import $A$ in HOL Light, as $A'$, and use it to discharge the condition $A'$.

[Jasmin Blanchette]

This is effectively what we do in our minds when we audit and accept the Flyspeck proof.

[Jasmin Blanchette]

But to our community, these bindings are not good enough; we'd like ideally the entire proof to be checked by one system (to maximize trust).

[Jasmin Blanchette]

And if not, we'd need at least a good tool and methodology for verifying the bindings.

[Kevin Buzzard]

One could imagine that different mathematicians have different models of what mathematics is, and write their papers with these models in mind, and yet because of mathematicians' black magic someone who firmly believes that mathematics is built using foundation X (but never talks about this in public) will happily use results which someone proved with foundation Y in their minds as they proved it.

[Jasmin Blanchette]

Yes, something like that. I believe your paper that spent 2 years on arXiv before getting submitted was a bit an example of that, where you had to delve deeply into the literature to make sure everything fits.

[Jasmin Blanchette]

All of this being said, my main conclusion is this:

Instead of talking about translation tools, I would propose to first focus on workflow and concrete use cases. Tools can help a workflow. Tools developed without a workflow in mind often end up having zero users (like the many bridges between proof assistants built over the years).

[Jasmin Blanchette]

(The general idea of focusing on workflows first and not tools is something I learned from Manfred Broy, professor emeritus at TU München.)

[Mario Carneiro]

As an example of a workflow, if we had some nontrivial amount of mathematics built using the set.mm library as a dependency, then it would help to ensure the quality of the bridge. I think the problem with setting this up is a sort of chicken and egg problem regarding the quality of the bridge

[Mario Carneiro]

I hesitate to propose that it be available as a dependency for mathlib itself, since that will double it in size

[Mario Carneiro]

Jasmin Blanchette said:

If this were software, you'd create bindings: You'd just say: Division in Isabelle = division in HOL Light, etc.

This is effectively what we do in our minds when we audit and accept the Flyspeck proof.

But to our community, these bindings are not good enough; we'd like ideally the entire proof to be checked by one system (to maximize trust).

I think this is the right attitude. The real work is the bindings, not the bridge. The bridge can be validated once and for all, for the most part, but the bindings are the alignment of concepts, and this evolves with the libraries

[Mario Carneiro]

I believe that it is possible to get a bridge going where all the user has to provide are the bindings (keeping in mind that proofs need bindings too)