## Stream: Program verification

### Topic: upper bounds on proof translation

#### 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

#### 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

#### 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

#### Mario Carneiro (Jul 01 2020 at 20:03):

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

#### 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

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

#### Mario Carneiro (Jul 01 2020 at 20:07):

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

#### Jalex Stark (Jul 01 2020 at 20:07):

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

#### 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

#### Jalex Stark (Jul 01 2020 at 20:08):

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

right

#### Jalex Stark (Jul 01 2020 at 20:10):

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

#### Mario Carneiro (Jul 01 2020 at 20:10):

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

#### Mario Carneiro (Jul 01 2020 at 20:11):

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

okay, thanks

#### 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

#### 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

#### 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