# Zulip Chat Archive

## Stream: general

### Topic: simple proof systems

#### Reid Barton (Oct 14 2018 at 02:30):

Sorry in advance for a rather vague question, hopefully I can make it clear what I'm looking for.

Suppose I wanted to "compile" Lean formulas and proof terms to some other logical system. How "simple" could the target logical system be?

#### Mario Carneiro (Oct 14 2018 at 02:31):

hm, it is a bit vague

#### Reid Barton (Oct 14 2018 at 02:32):

I want a human-verifiable procedure for taking a theorem statement and turning it into a formula in some other system, and also a procedure for turning the Lean proof into a valid proof in the other system

#### Mario Carneiro (Oct 14 2018 at 02:32):

you can go pretty simple for almost any system, by appropriate encoding in the language of PA

#### Reid Barton (Oct 14 2018 at 02:32):

So one kind of simplicity which I would like is if the formulas of the target system could be described by an inductive type, and provability could be described by an inductive proposition

#### Reid Barton (Oct 14 2018 at 02:34):

Is the encoding you have in mind sort of how like I could simulate a checker for any language by a universal Turing machine?

#### Mario Carneiro (Oct 14 2018 at 02:34):

yes

#### Mario Carneiro (Oct 14 2018 at 02:34):

I get the sense that misses your point though

#### Reid Barton (Oct 14 2018 at 02:34):

I see.

#### Reid Barton (Oct 14 2018 at 02:35):

I was hoping for a system more like: if I have a proof of P and a proof of P -> Q, then I get a proof of Q. Plus a bunch of axioms. I'm pretty sure that I need additional rules to deal with quantifiers though.

#### Mario Carneiro (Oct 14 2018 at 02:35):

like ZFC style?

#### Mario Carneiro (Oct 14 2018 at 02:35):

+ FOL

#### Reid Barton (Oct 14 2018 at 02:36):

I think so but then I think I have to deal with substitution and that seems a little bit more complicated than I would like

#### Reid Barton (Oct 14 2018 at 02:37):

Is metamath based on something like this?

#### Mario Carneiro (Oct 14 2018 at 02:37):

I was about to suggest metamath indeed

#### Mario Carneiro (Oct 14 2018 at 02:37):

it doesn't have proper substitution

#### Mario Carneiro (Oct 14 2018 at 02:37):

just direct substitution

#### Reid Barton (Oct 14 2018 at 02:37):

I guess another way to frame the question is: Suppose you wanted to be as sure as possible that you had correctly implemented a proof checker which only accepts theorems provable in ZFC+U (or whatever).

#### Reid Barton (Oct 14 2018 at 02:38):

The universal turing machine idea doesn't help you here, because you still need to write the "actual machine" (it is just part of the specification of what constitutes a proof, rather than being the checker itself)

#### Mario Carneiro (Oct 14 2018 at 02:39):

I think you can avoid proper substitution in the axioms and what not by having it be an explicit judgment in the system

#### Reid Barton (Oct 14 2018 at 02:39):

what's not "proper" about direct substitution? Something about not renaming bound variables?

#### Mario Carneiro (Oct 14 2018 at 02:39):

yes

#### Mario Carneiro (Oct 14 2018 at 02:39):

metamath has a notion of text substitution a la grep

#### Reid Barton (Oct 14 2018 at 02:39):

I think I've heard phrases like "proof calculus with explicit substitution", is that relevant?

#### Mario Carneiro (Oct 14 2018 at 02:40):

that's about having terms in the language that are a sort of "deferred substitution"

#### Mario Carneiro (Oct 14 2018 at 02:40):

but you still have to do the substitution at some point

#### Mario Carneiro (Oct 14 2018 at 02:40):

although you can build it into the steps of actual proof, which is basically what metamath does

#### Reid Barton (Oct 14 2018 at 02:41):

but does that mean I can push the work of substitution into the proof itself

#### Mario Carneiro (Oct 14 2018 at 02:41):

yes

#### Mario Carneiro (Oct 14 2018 at 02:41):

that way all your substitutions are direct

#### Reid Barton (Oct 14 2018 at 02:42):

and if I were to target one of these systems then is there some kind of bound on how large the proofs would become in terms of the size of the original Lean proof term?

#### Reid Barton (Oct 14 2018 at 02:42):

like, a useful bound

#### Mario Carneiro (Oct 14 2018 at 02:42):

no, but the problem in that case is not substitution

#### Mario Carneiro (Oct 14 2018 at 02:42):

it is reduction

#### Reid Barton (Oct 14 2018 at 02:42):

oh right

#### Mario Carneiro (Oct 14 2018 at 02:42):

you can prove ridiculous theorems by `rfl`

in lean

#### Mario Carneiro (Oct 14 2018 at 02:43):

If you deduplicate the proof I think substitution is a "modest" overhead, maybe linear in the proof

#### Reid Barton (Oct 14 2018 at 02:43):

how about something like linear in the size of the term plus the total number of reduction steps Lean has to do (if that makes sense)

#### Mario Carneiro (Oct 14 2018 at 02:44):

My favorite characterization is "linear in the run time of the lean checker"

#### Reid Barton (Oct 14 2018 at 02:44):

Sure

#### Mario Carneiro (Oct 14 2018 at 02:46):

You need substitution of some kind built in to your system so that you can express a proof schema like "|- P and |- P -> Q implies |- Q`

#### Mario Carneiro (Oct 14 2018 at 02:46):

but direct substitution is good enough

#### Reid Barton (Oct 14 2018 at 02:46):

Okay this was going to be exactly my next question: do I need some kind of substitution

#### Mario Carneiro (Oct 14 2018 at 02:47):

Actually metamath also has a primitive notion of "disjoint variables" used in substitution

#### Reid Barton (Oct 14 2018 at 02:47):

Well

#### Mario Carneiro (Oct 14 2018 at 02:47):

meaning that you can say "P can be substituted for any expression not containing x"

#### Mario Carneiro (Oct 14 2018 at 02:48):

again, this is grep style, so no provisos like "no free x", just "no x at all"

#### Mario Carneiro (Oct 14 2018 at 02:48):

but that is good enough since you can build the rest into the proof system

#### Reid Barton (Oct 14 2018 at 02:48):

this particular example though is substituting into a fixed formula, right? I could imagine representing it by a constructor of an inductive type

| mp (P Q : formula) (p : proof P) (pq : proof (formula.imp P Q)) : proof Q

#### Mario Carneiro (Oct 14 2018 at 02:49):

yes, here you have lifted the substitution to the beta rule of the metatheory (which is lean, I guess)

#### Reid Barton (Oct 14 2018 at 02:49):

which is just a built-in part of the syntax of proofs

#### Reid Barton (Oct 14 2018 at 02:50):

But then, I don't know how to deal with "forall elim" without invoking substitution in a more serious way

#### Mario Carneiro (Oct 14 2018 at 02:50):

right, you need a true substitution there... but you can get around it with some different axiomatizations

#### Mario Carneiro (Oct 14 2018 at 02:51):

I think the safest/easiest way to do this while still being transparent about it is to have a judgment `P(x |-> y) is Q`

#### Mario Carneiro (Oct 14 2018 at 02:52):

although when you get to the bottom you have to deal with `z(x |-> y)`

which depends on a disjointness requirement

#### Mario Carneiro (Oct 14 2018 at 02:52):

which can be equality if you have decidable equality on the variables

#### Mario Carneiro (Oct 14 2018 at 02:53):

metamath takes a more abstract approach and just axiomatizes what this "disjointness" should satisfy

#### Reid Barton (Oct 14 2018 at 02:53):

Yes that's fine. This looks interesting.

#### Reid Barton (Oct 14 2018 at 02:53):

So I have a rule of inference that takes `forall x, P x`

and `y`

and `P(x |-> y) is Q`

and concludes `Q`

#### Mario Carneiro (Oct 14 2018 at 02:53):

right

#### Reid Barton (Oct 14 2018 at 02:54):

and `P(x |-> y) is Q`

is also defined by some other induction

#### Mario Carneiro (Oct 14 2018 at 02:54):

right

#### Reid Barton (Oct 14 2018 at 02:54):

I like this.

Is this likely to mess up the "size of proof is linear in the Lean kernel runtime" property?

#### Mario Carneiro (Oct 14 2018 at 02:54):

no

#### Mario Carneiro (Oct 14 2018 at 02:54):

because lean has to do this too

#### Reid Barton (Oct 14 2018 at 02:55):

oh, I see!

#### Mario Carneiro (Oct 14 2018 at 02:57):

You can have a similar induction rule for deducing `x is free in P`

for the elim rules

#### Mario Carneiro (Oct 14 2018 at 03:03):

By the way metamath doesn't do it this way, instead it uses a slightly tricky axiom system for pred calc that allows us to deduce these judgments without building them in directly, and lets the forall rule be the simple `|- (forall x, P) -> P`

#### Mario Carneiro (Oct 14 2018 at 03:06):

But I think this is something like the difference between listing 20 obvious axioms for boolean algebras vs listing 3 incomprehensible ones and proving they are equivalent

#### Reid Barton (Oct 14 2018 at 03:10):

So here is one reason why I have this question.

Cryptography people tell me (not in this language of course, and I hope I am not mistranslating anything) that if I have some fancy indexed inductive type `proof P`

, I can design some functions f, g and h with the following properties.

- f is a predicate on short strings (~300 bytes) which can be evaluated quickly (~20ms).
- g is some even cheaper function on such strings, and h(P) is just a recursive hash of the contents of P.
- Given a term of type
`proof P`

I can calculate a string x with f(x) = true and g(x) = h(P). - (Subject to some trusted setup and cryptographic hardness assumptions,) the only way to construct such an x is as above: I have to really know a term of type
`proof P`

, though I can also use other pairs (Q, y) which have been published as certificates of other statements as inputs to my term.

The catch is that the third item is somewhat ridiculously expensive, though in the future it may become less ridiculously expensive.

#### Reid Barton (Oct 14 2018 at 03:11):

As a ballpark estimate for ridiculously expensive, assume 1 constructor costs 1 second to compute

#### Mario Carneiro (Oct 14 2018 at 03:13):

so I guess x is a "proof hash" of some sort, f means "this is a proof of something" and g means "this is the statement that is being proved"?

#### Reid Barton (Oct 14 2018 at 03:13):

Right

#### Reid Barton (Oct 14 2018 at 03:15):

Probably it is a bit better to think that the "proof hash" is a statement like "this is a proof of some statement which hashes to H"

#### Mario Carneiro (Oct 14 2018 at 03:16):

I'm surprised the function g is easy

#### Mario Carneiro (Oct 14 2018 at 03:16):

it's not even that easy to calculate the statement of a proof sometimes

#### Reid Barton (Oct 14 2018 at 03:16):

I think that g can just be extracting some of the bits from the string though I confess I have not thought much about this particular aspect yet

#### Mario Carneiro (Oct 14 2018 at 03:17):

I guess you can do something like that

#### Reid Barton (Oct 14 2018 at 03:17):

I think the idea is that it was the job of the person producing the proof to include the information of what is being proved

#### Reid Barton (Oct 14 2018 at 03:18):

This is really at a super early stage of "is it even conceivable that one could use this for theorem proving"--I'm trying to get a sense of what the minimal demands on the theorem proving side are

#### Reid Barton (Oct 14 2018 at 03:19):

What I find to be really remarkable about these setups is that the cost to verify a proof is independent of the size of the proof

#### Mario Carneiro (Oct 14 2018 at 03:20):

that's a good point. I wonder whether it can be used as a trusted alternative to caching

#### Reid Barton (Oct 14 2018 at 03:20):

So, ignoring some inconvenient details like the ~1000000x slowdown, you could use it as part of a "distributed theorem verification system", without requiring trusted provers

#### Reid Barton (Oct 14 2018 at 03:23):

(Concretely, you could imagine some kind of database to which anyone can upload proof certificates, with the amazing property that in order to verify the correctness of any proof, you only need to check *that certificate* and not the proofs of any of the results which the proof relies on)

#### Mario Carneiro (Oct 14 2018 at 03:24):

Unless they decided to modify `logic.basic`

:)

#### Mario Carneiro (Oct 14 2018 at 03:25):

In some sense we already have this, the difference is that you can do this check without even precomputing the proofs of earlier parts, or even knowing what the proofs are (e.g. proprietary proofs)

#### Reid Barton (Oct 14 2018 at 03:27):

I think what we have is like a non-distributed version of this, where I trust the Lean kernel on my machine to only record as theorems the facts which it has checked. Or do you mean something else?

#### Reid Barton (Oct 14 2018 at 03:28):

Solving the recompilation problem is somehow close to but not exactly the same as the problem this solves, I think.

#### Mario Carneiro (Oct 14 2018 at 03:28):

That's true, but I'm pointing out that if you have mathlib, say, fully compiled, then you are currently in the state of trusting all the results in it, and if a new proof comes along that depends on these facts you only have to check *that proof* and not the rest of the library

#### Mario Carneiro (Oct 14 2018 at 03:29):

In this crypto setup compilation is being replaced by certificate generation

#### Mario Carneiro (Oct 14 2018 at 03:30):

where the difference is that if I send you a certificate you can have the same trust as if you created it yourself, while if I send you my compiled files then you don't know that I haven't tampered with them

#### Reid Barton (Oct 14 2018 at 03:30):

Yes exactly

#### Reid Barton (Oct 14 2018 at 03:31):

And if we had some massive proof of say FLT, then maybe it would be quite expensive for everyone to verify the whole proof, whether or not they do it incrementally over time. If the certificates can be computed by someone just once, then you can save total work (assuming there are > 1000000 people who want to verify the proof)

#### Mario Carneiro (Oct 14 2018 at 03:33):

I think this isn't a realistic threat model though

#### Reid Barton (Oct 14 2018 at 03:33):

Anyways, I think that today we're not really anywhere close to wanting something like this, and the technology is also not really that feasible yet

#### Reid Barton (Oct 14 2018 at 03:34):

Which part is not realistic?

#### Mario Carneiro (Oct 14 2018 at 03:34):

I think when people get mathlib they usually don't do it because they want additional assurance that the theorems in it are true

#### Reid Barton (Oct 14 2018 at 03:34):

Well not for mathlib

#### Mario Carneiro (Oct 14 2018 at 03:35):

I am pretty sure that feit thompson is true because Gonthier checked it, and my running it on my machine did not increase my confidence in the theorem as much as it increased my confidence that I had installed Coq correctly

#### Reid Barton (Oct 14 2018 at 03:36):

In some distant future world, you could imagine that instead of posting papers to arXiv, we publish formal proofs to some other service. I guess your claim is that in that scenario, you are not too worried about people claiming to publish proofs which are in fact bogus.

#### Reid Barton (Oct 14 2018 at 03:37):

Especially given that anyone *could* verify the proof and everything underneath it, it would just be quite expensive for everybody to do so.

#### Mario Carneiro (Oct 14 2018 at 03:37):

I would want the service to be spending effort on checking for bogus proofs

#### Mario Carneiro (Oct 14 2018 at 03:37):

that's not my responsibility

#### Reid Barton (Oct 14 2018 at 03:37):

Right, you could delegate to the service to check correctness which seems quite reasonable

#### Mario Carneiro (Oct 14 2018 at 03:38):

I would be responsible for convincing myself that the service is doing its job to my satisfaction

#### Mario Carneiro (Oct 14 2018 at 03:38):

meaning that this service should be easily checkable (i.e. small trusted kernel)

#### Reid Barton (Oct 14 2018 at 03:39):

Plus you have to trust the people who operate the service to actually verify the proofs

#### Mario Carneiro (Oct 14 2018 at 03:40):

I think there is room for some crypto cross checks at this point

#### Mario Carneiro (Oct 14 2018 at 03:41):

i.e. the process of verification by the service also produces a certificate that I can check quickly

#### Reid Barton (Oct 14 2018 at 03:42):

In general the way to produce a certificate that a computation was done correctly is the same process that I am talking about for generating proof certificates.

#### Mario Carneiro (Oct 14 2018 at 03:42):

Although nowadays this check is replaced with me being able to download and check the proof myself if I want

#### Reid Barton (Oct 14 2018 at 03:42):

(Namely, SNARKs and applications like TinyRAM)

#### Reid Barton (Oct 14 2018 at 03:43):

Right so in actual crypto applications, there is the far more important property that the person producing the certificate doesn't have to give you the proof.

#### Reid Barton (Oct 14 2018 at 03:45):

As I mentioned, this stuff is currently quite impractical for large applications.

Probably a far more practical question would be: could Lean have a mode where it checks a given olean file against lean source, and is this faster than trying to recompute the proof from scratch.

#### Reid Barton (Oct 14 2018 at 03:46):

Or more generally, what information could Lean write out to an .olean or other external certificate file which would make verifying the validity of a theorem more efficient

#### Mario Carneiro (Oct 14 2018 at 03:50):

In principle lean should be able to check an olean file without reference to a lean file at all

#### Mario Carneiro (Oct 14 2018 at 03:51):

and if you wanted you could view this as a "compiled file" same as the compiled binaries of any other program

#### Mario Carneiro (Oct 14 2018 at 03:51):

in particular, it would be difficult to reverse engineer the sources from this

#### Mario Carneiro (Oct 14 2018 at 03:52):

... I think. I need to write an olean viewer to be sure

#### Reid Barton (Oct 14 2018 at 03:55):

Do .olean files and the export textual format and what `#print foo`

produces all contain roughly the same information?

#### Reid Barton (Oct 14 2018 at 03:58):

looking at the export format it seems not to include all information about notation, which must be in .olean files, but aside from minor details like that

#### Mario Carneiro (Oct 14 2018 at 03:59):

I think so

#### Mario Carneiro (Oct 14 2018 at 03:59):

It should have the information necessary to construct an `environment`

object from the imported environments

#### Reid Barton (Oct 14 2018 at 03:59):

I wonder whether there is a way today to convince Lean to export an .olean file to textual format

#### Mario Carneiro (Oct 14 2018 at 04:00):

That would be nice... I probably wouldn't even write such an exporter in lean

#### Mario Carneiro (Oct 14 2018 at 04:00):

(that is, there is no particular advantage to writing it in lean)

#### Reid Barton (Oct 14 2018 at 04:03):

I guess you could import the module for which you had the .olean from a new module, and then run it through `lean --export`

#### Reid Barton (Oct 14 2018 at 04:06):

it seems to work

#### Reid Barton (Oct 14 2018 at 04:07):

though I wouldn't be 100% confident that lean importing an arbitrary .olean file and then exporting its contents and checking them in an external checker means lean is actually in a valid state after reading the .olean file

#### Mario Carneiro (Oct 14 2018 at 04:20):

why? The checker doesn't matter for that

#### Mario Carneiro (Oct 14 2018 at 04:21):

Lean itself will complain if the olean is bad

#### Mario Carneiro (Oct 14 2018 at 04:21):

although I'm not sure how you can induce that without writing the olean bits manually, since lean won't produce olean files for errored files

#### Kevin Buzzard (Oct 14 2018 at 10:22):

I want a human-verifiable procedure for taking a theorem statement and turning it into a formula in some other system, and also a procedure for turning the Lean proof into a valid proof in the other system

My understanding (which may be wrong) is: Computer scientists want (and occasionally some claim that they have built) a procedure for translating code written in one common language to code written in another common language, and the reason none of these procedures are ever used in practice is that in practice they are typically not very good at all.

I am pretty sure that feit thompson is true because Gonthier checked it, and my running it on my machine did not increase my confidence in the theorem as much as it increased my confidence that I had installed Coq correctly

My understanding (which is much more likely to be correct this time) is that Feit Thompson is true because the pure mathematics community did an *extremely* good job of checking it in the 1960s, decided it was correct, and awarded Thompson the Fields Medal as a consequence. This is exactly why pure mathematicians are not excited by Gonthier et al's verification. Checking 400 pages of lemmas about finite groups and undergraduate/MSc level representation theory and number theoy is not difficult for a team of humans to do, it can be broken down into manageable sub-jobs etc.

#### Mario Carneiro (Oct 14 2018 at 10:40):

Yeah, but I didn't understand what Thompson did at all, I at least have some idea of how Gonthier did it

#### Mario Carneiro (Oct 14 2018 at 10:41):

I think you should not forget that one of the applications of formal mathematics is that at least in principle you can pick it up and read it from *zero* prior knowledge of the field

#### Mario Carneiro (Oct 14 2018 at 10:42):

And I know several people who did exactly that, including myself

#### Mario Carneiro (Oct 14 2018 at 10:46):

(Note that that quote was about my subjective perception of the truth of the theorem, not the mathematics community at large.) The whole point of this crypto stuff is that just because *you* trust X body of knowledge / institution / person doesn't mean *I* do, and the problem is to figure out how to reliably transfer your trust to me

#### Kevin Buzzard (Oct 14 2018 at 13:00):

Aah I see! So this is a perfect analogy. I say "I am a mathematician and my tribe can guarantee that Feit-Thompson is proved" and you reply "I am a computer scientist and I require a different kind of justification than just assurances from your tribe".

#### Patrick Massot (Oct 14 2018 at 13:01):

I think you should not forget that one of the applications of formal mathematics is that at least in principle you can pick it up and read it from

zeroprior knowledge of the field

I thought mathlib didn't care about human readability?

#### Mario Carneiro (Oct 14 2018 at 13:06):

I'm talking about formal proof in general. Certainly it's more true of metamath than mathlib, because there are fewer skipped steps

#### Mario Carneiro (Oct 14 2018 at 13:07):

The point is that it doesn't matter if it's been written to be human readable in the mathematician's sense. In fact, it's better if it doesn't make too much use of tactics that do what Kevin wants (i.e. trivial for a mathematician steps omitted)

#### Mario Carneiro (Oct 14 2018 at 13:08):

because that way you can follow what's happening even if you aren't a mathematician

#### Mario Carneiro (Oct 14 2018 at 13:11):

the worst kind of proof for people who want to learn like this are the big complicated statement proven by some blasty tactic. It's like the movie ends just as it's setting up for the climax, you feel robbed

#### Mario Carneiro (Oct 14 2018 at 13:13):

luckily lean doesn't have too many blasty tactics yet, so it is still feasible to read a proof and get the details

#### Kevin Buzzard (Oct 14 2018 at 13:32):

I have been telling my maths students to never read any proofs in mathlib because they are all unreadable, and if they want to know why some theorem is true then to look it up on Wikipedia, which is written for humans. I am the anti-Paulson. I believe that proofs generated by computers in the future will inevitably be unreadable, and that anyone who attempts to make them readable will in some sense be holding the area back. I was always struck by something Johannes said to me months ago when I asked him why he'd changed my 10 line tactic proof into an incomprehensible two-line term proof, and he replied that he liked the challenge of finding a short efficient proof of something which was easy in maths. While he might not want to extrapolate this comment himself to longer proofs, I don't mind doing so.

#### Mario Carneiro (Oct 14 2018 at 13:37):

My view is that there is a kind of readability that can't be harmed by "unreadable" proof style

#### Mario Carneiro (Oct 14 2018 at 13:37):

because the information is still there to be given to the computer

#### Mario Carneiro (Oct 14 2018 at 13:38):

and there are some enterprising kids that actually prefer this kind of exactitude to the "aimed for human level" style that is traditional in maths

#### Mario Carneiro (Oct 14 2018 at 13:40):

This is where stuff like `#explode`

is useful, when you just want to see EVERYTHING and make your own choices about what is important

#### Mario Carneiro (Oct 14 2018 at 13:40):

rather than whatever the author thought was important or trivial

#### Patrick Massot (Oct 14 2018 at 14:38):

I have been telling my maths students to never read any proofs in mathlib because they are all unreadable, and if they want to know why some theorem is true then to look it up on Wikipedia, which is written for humans.

I just did the exercise of reading the Wikipedia page on topological rings. It's full of plain wrong statements...

#### Kevin Buzzard (Oct 14 2018 at 17:23):

You have a clear choice then :-) Human efforts with wrong statements, or `topological_structures.lean`

written by Johannes and never meant to be read by a mathematician :-) Pure maths is two things and you are lucky enough to be able to choose which one you like best.

#### Johan Commelin (Oct 14 2018 at 23:35):

@Mario Carneiro @Reid Barton I find this topic of cryptographic proof certificates really interesting! Do you know if anything like this has been implemented for some theorem prover? I've thought about this on and off (basically as an amateur) and I couldn't find anything written about it. Are there references that go beyond speculating how nice it would be to have this? From Reid's description it is still quite a leap to an actual (fast) implementation.

Last updated: Dec 20 2023 at 11:08 UTC