upper bounds on proof translation

Stream: Program verification

[Jalex Stark]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

right

[Jalex Stark]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jalex Stark]

okay, thanks

[Mario Carneiro]

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

[Mario Carneiro]

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]

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