Zulip Chat Archive

Stream: Program verification

Topic: upper bounds on proof translation


view this post on Zulip Jalex Stark (Jul 01 2020 at 19:56):

Suppose we have a metamath proof that a particular theorem prover L is correctly implemented (whatever that means), and we know that it builds all the files in mathlib.
Does this give us a way to extract a metamath statement and proof of each mathlib statement?
I asked @Mario Carneiro a related question in a place where such discussion was off-topic

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:01):

I guess it doesn't make sense to talk about a reimplementation of Lean without reference to the lean source code

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:02):

The two issues with that proposal are in the two assumptions: how is the theorem prover L being proven correct, and how is it running on mathlib? If you are running the theorem prover inside metamath then it would be far easier to just translate the proofs to metamath instead

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:03):

The proof translation is bounded by the runtime of the lean verified implementation (however it runs)

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:05):

There is a general theorem that asserts this but the constant is pretty terrible since you have to simulate a machine one state at a time using inference steps

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:06):

so in practice, the translation problems that have been attempted were easier to do "directly" rather than going through a reimplementation of the prover?

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:07):

well, really the prover is being reimplemented but it is recognizable as the translation program itself

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:07):

okay, so you do translate all of the proofs with one program

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:07):

the lean kernel is turned into a proof-producing kernel where the proofs are in a different language

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:08):

so you just directly replace trust in the lean kernel with trust in the base system

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:09):

right

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:10):

do you envision metamath C to be a good language for reimplementing provers in?

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:10):

Not really, it's mainly useful for programs that have to be trusted (provers or otherwise)

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:11):

that is, it produces programs that prove properties by virtue of their running on real machines

view this post on Zulip Jalex Stark (Jul 01 2020 at 20:12):

okay, thanks

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:13):

So you can write proof kernels in MMC, as well as things like fast trusted bignum arithmetic or other verified numeric computations

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:14):

there are several examples of big computer proofs being done with an interactive part plus a verified program part that is implemented in a language like C

view this post on Zulip Mario Carneiro (Jul 01 2020 at 20:14):

and MMC is trying to address the requirements of programs like these


Last updated: May 08 2021 at 21:09 UTC