Zulip Chat Archive

Stream: new members

Topic: Translating proofs between proof systems


view this post on Zulip Benjamin (Sep 24 2020 at 17:04):

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?

view this post on Zulip Johan Commelin (Sep 24 2020 at 17:06):

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

view this post on Zulip Johan Commelin (Sep 24 2020 at 17:07):

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

view this post on Zulip Johan Commelin (Sep 24 2020 at 17:08):

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

view this post on Zulip Johan Commelin (Sep 24 2020 at 17:08):

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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 18:00):

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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 18:00):

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.

view this post on Zulip Patrick Thomas (Sep 24 2020 at 18:01):

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

view this post on Zulip Mario Carneiro (Sep 24 2020 at 18:33):

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

view this post on Zulip Mario Carneiro (Sep 24 2020 at 18:33):

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

view this post on Zulip Mario Carneiro (Sep 24 2020 at 18:34):

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

view this post on Zulip Julian Berman (Sep 24 2020 at 19:13):

(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?

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 19:14):

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

view this post on Zulip Julian Berman (Sep 24 2020 at 19:15):

Aha very interesting! Thanks.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:42):

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

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:43):

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).

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:44):

  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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:46):

  1. 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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:47):

  1. 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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:48):

  1. 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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:49):

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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:50):

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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:51):

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.

view this post on Zulip Jasmin Blanchette (Sep 24 2020 at 19:54):

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.

view this post on Zulip Julian Berman (Sep 24 2020 at 20:57):

The FFI metaphor is interesting

view this post on Zulip Julian Berman (Sep 24 2020 at 20:59):

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?

view this post on Zulip Julian Berman (Sep 24 2020 at 21:00):

(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

view this post on Zulip ZY Cao (Sep 24 2020 at 21:05):

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

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:28):

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

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:28):

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

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:29):

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

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:29):

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

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:30):

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).

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:31):

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

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 08:31):

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.

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:32):

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.

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:33):

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).

view this post on Zulip Jasmin Blanchette (Sep 25 2020 at 08:39):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:28):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:29):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:36):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:37):

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)


Last updated: May 14 2021 at 04:22 UTC