CICM 2020: Metamath Zero talk

[Mario Carneiro]

For those who might be interested, I just presented MM0 at the CICM conference, and the video is now on youtube:

https://youtu.be/CxS0ONDfWJg

(It occurs to me that I should have announced this *before* the talk, in case folks were interested in registering for free in order to attend directly. You can still ask questions here if you want.)

Mario Carneiro

[Raph Levien]

Great talk, and I hope it gets a wider audience. I have to confess to some envy, as you're accomplishing a great deal of what I set out to do with Ghilbert and stalled out on.

A question: when translating to Lean, do you have to depend on classical logic (ie "open classical"), or are you somehow able to avoid that?

If I get some time (a bit rare these days) I would like to play with it in more detail.

Raph

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.com.

[Mario Carneiro]

On Thu, Jul 30, 2020 at 1:11 AM Raph Levien <raph....@gmail.com> wrote:

A question: when translating to Lean, do you have to depend on classical logic (ie "open classical"), or are you somehow able to avoid that?

Lean and metamath take a significantly different approach to axioms. In metamath, of course, there are many axioms, starting with classical propositional logic, then predicate logic, then the axioms of ZFC one at a time, with choice delayed to the last moment. In lean, there are only three axioms, but the "no axioms" baseline is very high (I'm not positive but I think it already exceeds ZFC in consistency strength), containing dependent type theory with inductive types and a hierarchy of universes.

In lean, it is possible to build a model of ZFC as a certain inductive type. For obvious reasons, you need lean's choice to prove the ZFC choice axiom, but less obviously you also need it to prove replacement, because you have to choose a pre-set corresponding to each set in the mapping. (The ZFC model is a quotient by extensionality of an inductive type of pre-sets.) But choice actually gets involved much earlier, because the "no axioms" baseline of lean is only enough to get *intuitionistic* logic, not classical logic, and in lean the axiom of choice is used to prove the law of excluded middle. Since metamath assumes classical logic from the get-go, choice is therefore used in almost all translated theorems.

Luckily, as a social matter, Leaners are used to not thinking about axiom usage at all; basically all of mathlib uses all three axioms and this system is basically equivalent to ZFC + countable inaccessible cardinals, so it is quite compatible with set.mm foundations.

Mario

 

On Wed, Jul 29, 2020 at 10:11 AM Mario Carneiro <di....@gmail.com> wrote:

For those who might be interested, I just presented MM0 at the CICM conference, and the video is now on youtube:

https://youtu.be/CxS0ONDfWJg

(It occurs to me that I should have announced this *before* the talk, in case folks were interested in registering for free in order to attend directly. You can still ask questions here if you want.)

Mario Carneiro

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CADBEgNM6WD4rYwrFqJQ1sE5z%3DL%2BZAy2b7h5jyEqd0%2Bug%2BSaoeQ%40mail.gmail.com.

[David A. Wheeler]

> On Thu, Jul 30, 2020 at 1:11 AM Raph Levien <raph....@gmail.com> wrote:
> > A question: when translating to Lean, do you have to depend on classical
> > logic (ie "open classical"), or are you somehow able to avoid that?

On Thu, 30 Jul 2020 11:13:56 +0200, Mario Carneiro <di....@gmail.com> wrote:
> Lean and metamath take a significantly different approach to axioms. In
> metamath, of course, there are many axioms, starting with classical
> propositional logic, then predicate logic, then the axioms of ZFC one at a

> time, with choice delayed to the last moment. ...

Clarification: Mario is talking here about the *set.mm* metamath database,
not about metamath in general, since obviously metamath
can be used without using classical logic or ZFC simply by
creating a different database.

Mario's extremely well aware of that, and is an expert on that topic,
but I thought other readers here might be confused.

--- David A. Wheeler

[Jon P]

Hi Mario, 

Very nice talk, thank you for posting it. 

Is it ok to ask some basic questions? It is a really nice project you are doing and I would love to understand it, however I am afraid I am not so strong in all this stuff. Feel free not to answer if you are busy, that is no problem, if it's ok I'll just write what I think and then maybe you could tell me where I have got confused?

So I understand about metamath. You have some hypotheses and a theorem and a list of substitutions which use rules from the database or hypotheses to establish the theorem. I also understand that there is a question around whether you can trust the verifier, so we have 5 independent ones to improve that.

I think I also get a little of the idea of formal verification for programs, so you have some abstract model of a computation system (like x86) and using that you prove that, if the hardware executes the model accurately, that the program will give the output you want. Like maybe some function called Prime(X) which returns 0 for primes and 1 for non-primes, you could prove that, if this terminates, the answer will be correct. However I guess there is still the problem of trusting the verifier (whether human or machine). I also have never seen a verification of a program so if you know any beginner materials on it I'd be interested.

I think you're trying to combine both of these right? From what I understand of your system there's MM0, which is a verifier, which takes and mm0 and mmb files and checks if the proof is correct. I assume this is much like the metamath verifiers? Then there is MM1 which is a tool for generating mm0 and mmb files which is not verified but it doesn't matter because it's output is checked so how the output was generated is not important.

And then there is MMC which is a language which compiles programs and also creates proofs of the correctness of those programs? So if I write some program, like Prime(X), the compiler will output some machine code and also a proof that Prime(X) does what it is specified to do, on x86, up to the assumption that the hardware executes the model correctly? And the idea is to write the MM0 verifier in MMC so that it is verified during the compilation process which gives confidence in it?

If that is all reasonably correct I guess where I am confused is how you are doing this reflexive verification. 

I would have thought, naively, that for justifying any program, X, you have 3 options. Firstly you can assume X is valid. Secondly you can use Y to justify X, the problem of this is that it's then justifications all the way down. Thirdly you can use X to justify X, as in if the program is a program verifier then you can feed it into itself and if it says it's good then it's good.

However I don't understand how that's not circular? For example consider the verifier: For all input return "this program is verified." That has the ability to verify itself and will come out with a positive response however I don't think it's really established anything particularly meaningful. I guess I can't see on a philosophical level how you can get out of that trap.

Is it more of a strengthening exercise where you can't be sure that it's verified but the probability of MMC having a mistake and then MM0 having a mistake becomes super low or something?

If you're interested in answering, and I can totally understand if you're not, could you go easy on me when explaining? I get easily confused. Thanks, Jon.

[Mario Carneiro]

On Fri, Jul 31, 2020 at 3:55 PM Jon P <drjonp...@gmail.com> wrote:

Hi Mario, 

Very nice talk, thank you for posting it. 

Is it ok to ask some basic questions? It is a really nice project you are doing and I would love to understand it, however I am afraid I am not so strong in all this stuff. Feel free not to answer if you are busy, that is no problem, if it's ok I'll just write what I think and then maybe you could tell me where I have got confused?

So I understand about metamath. You have some hypotheses and a theorem and a list of substitutions which use rules from the database or hypotheses to establish the theorem. I also understand that there is a question around whether you can trust the verifier, so we have 5 independent ones to improve that.

I think I also get a little of the idea of formal verification for programs, so you have some abstract model of a computation system (like x86) and using that you prove that, if the hardware executes the model accurately, that the program will give the output you want. Like maybe some function called Prime(X) which returns 0 for primes and 1 for non-primes, you could prove that, if this terminates, the answer will be correct. However I guess there is still the problem of trusting the verifier (whether human or machine). I also have never seen a verification of a program so if you know any beginner materials on it I'd be interested.

I think you're trying to combine both of these right? From what I understand of your system there's MM0, which is a verifier, which takes and mm0 and mmb files and checks if the proof is correct. I assume this is much like the metamath verifiers? Then there is MM1 which is a tool for generating mm0 and mmb files which is not verified but it doesn't matter because it's output is checked so how the output was generated is not important.

And then there is MMC which is a language which compiles programs and also creates proofs of the correctness of those programs? So if I write some program, like Prime(X), the compiler will output some machine code and also a proof that Prime(X) does what it is specified to do, on x86, up to the assumption that the hardware executes the model correctly? And the idea is to write the MM0 verifier in MMC so that it is verified during the compilation process which gives confidence in it?

That's correct. You said that we ensure the correctness of the metamath verifiers by having many of them, I want to go one step further and verify that the program itself is implemented correctly with a formal proof.

If that is all reasonably correct I guess where I am confused is how you are doing this reflexive verification. 

I would have thought, naively, that for justifying any program, X, you have 3 options. Firstly you can assume X is valid. Secondly you can use Y to justify X, the problem of this is that it's then justifications all the way down. Thirdly you can use X to justify X, as in if the program is a program verifier then you can feed it into itself and if it says it's good then it's good.

However I don't understand how that's not circular? For example consider the verifier: For all input return "this program is verified." That has the ability to verify itself and will come out with a positive response however I don't think it's really established anything particularly meaningful. I guess I can't see on a philosophical level how you can get out of that trap.

It is circular, I don't contest it. I go into more detail on the philosophical implications of self-verification in a previous talk I gave in January on the topic:

http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_carneiro.pdf
https://www.youtube.com/watch?v=CqZzbaEuNBs

 

The point is that even a circular proof of correctness is an improvement on no proof of correctness, it's just not as good as a non-circular proof. In order to make up the difference you still have to look at the code and verify that it's reasonable. You have to do this with a standard unverified kernel too, only now you have the assurance that the fine details are correct and the inspection is to make sure that there aren't any obvious problems. The need for inspection also means that it is important for the bootstrap to be as small as possible. It should also be possible to set even smaller programs under MM0, but these will not be self verifying, they rely on full inspection (or rather, they can be verified by MM0, not themselves). I take a lot of inspiration from the Bootstrappable project for this sort of thing.

The other thing that can be done is to translate the proof to another proof system. This allows you to turn an MM0 proof of MM0 correctness into an MM/Lean/Isabelle proof of MM0 correctness. This doesn't make it any less circular, but with multiple bootstraps you only have to trust one of them, and if you are predisposed to trust a particular proof assistant then this might be more psychologically satisfactory. (But I want to emphasize that all these proof systems are all still running on your (say) x86 hardware, so a bug in the hardware affects them all.)

Basically, self-verification is not a substitute for all the other, traditional methods for ensuring code correctness, namely looking at the code, reimplementing it in several languages, unit testing and so on. However, it is far more reliable, especially when you combine a cursory inspection with a formal proof (where the cursory inspection is there to eliminate the equivalent of trusting trust attacks).

Is it more of a strengthening exercise where you can't be sure that it's verified but the probability of MMC having a mistake and then MM0 having a mistake becomes super low or something?

MMC doesn't have to be verified either, because it, like MM1, is proof producing. The only thing that has to be trusted is the MM0 kernel and the definition of x86, because MMC produces proofs of correctness relative to that definition of x86 that will be checked by the MM0 kernel. But since the program being checked is the MM0 kernel, we have the circularity as described above.

If you're interested in answering, and I can totally understand if you're not, could you go easy on me when explaining? I get easily confused. Thanks, Jon.

I of course am quite happy to answer these questions at length (sometimes too much length :P ), and appreciate the interest in my work.

Mario

[Jon P]

Thanks so much for your nice response Mario. I think the work you’re doing is really awesome and I’m very thankful that you would take your time to explain things to me. I feel similarly with everyone else in this community, I’m so impressed by everyone here.

I dig the idea that each independent check decreases the probability of being wrong, so I can see how formal proofs in multiple proof assistants on multiple machines makes it unlikely that MM0 is flawed, that makes a lot of sense. I also see why having MM0 be as small as possible is very good. I also guess there are philosophical problems around creating something provably logically infallible.

Can I ask about how MMC proofs work? So I had a little look at formal verification for software and it showed techniques like exhaustively searching the state space or using automated induction, are you thinking along these lines where the computer will run a standard algorithm for each program?

Or is it more like an MM proof where there are explicit steps? For example Prime(X) is the sort of function which I can’t really imagine checking in an automated way as there are so many inputs, though maybe there is some nice induction depending on how it works (a sieve of Eratosthenes might be amenable to an inductive proof for example). 

Does the user have to specify the steps themselves or can the compiler help generate them or is it a totally different system? If MMC produces proofs which are checkable by MM0 does that mean they are similar to MM proofs in style? It’s interesting to me that MM0 can check both MM proofs and x86 proofs and yet remain small, that is very intriguing.

If so there has been a lot of work to build up the set.mm database of proofs, is there a similar process to build up MMC functions and their associated proofs? For example given a verified addition function you could build a multiplication function and then a function for the multiplication of matrices or something.

I think these formal methods are obviously the future of mathematics so it’s really cool to be able to watch them develop. I also think there may be interesting applications to The AI Control Problem, for example letting an AI expand its capabilities iff it can prove the expanded system is constrained in the same way it is constrained itself. There is some similar paradigm to what you are doing about a system verifying itself (or it's offspring). This sounds like it might make it feasible to control an arbitrarily sophisticated system which is cool because without control there are a lot of worries. I asked Stuart Russel about it in a Reddit AMA and he said he’s considered formal proofs as a method for AI Control which is interesting. I’ve watched enough Stargate SG-1 to know I don’t want to have to deal with replicators.

[Mario Carneiro]

On Sun, Aug 2, 2020 at 11:38 AM Jon P <drjonp...@gmail.com> wrote:

Thanks so much for your nice response Mario. I think the work you’re doing is really awesome and I’m very thankful that you would take your time to explain things to me. I feel similarly with everyone else in this community, I’m so impressed by everyone here.

I dig the idea that each independent check decreases the probability of being wrong, so I can see how formal proofs in multiple proof assistants on multiple machines makes it unlikely that MM0 is flawed, that makes a lot of sense. I also see why having MM0 be as small as possible is very good. I also guess there are philosophical problems around creating something provably logically infallible.

Can I ask about how MMC proofs work? So I had a little look at formal verification for software and it showed techniques like exhaustively searching the state space or using automated induction, are you thinking along these lines where the computer will run a standard algorithm for each program?

That is certainly an approach that is used to check program correctness, but (1) it's not particularly well suited to formal proof and (2) it doesn't cover most actual proofs of interest. Of course the reason we want a theorem prover in the mix is so that we can state and prove theorems of arbitrary mathematical complexity about programs. For example, if we have a program that enumerates primes, we can use the proof that there are infinitely many primes to show that it will never finish (or rather, it will overflow before finishing).

 

Or is it more like an MM proof where there are explicit steps? For example Prime(X) is the sort of function which I can’t really imagine checking in an automated way as there are so many inputs, though maybe there is some nice induction depending on how it works (a sieve of Eratosthenes might be amenable to an inductive proof for example). 

The kind of proofs that MMC works with are fully symbolic proofs. The original proponent of this approach was Tony Hoare, and Hoare logic (https://en.wikipedia.org/wiki/Hoare_logic) is a logic where you prove properties of the form "if P holds on entry to code segment C, then C will not crash and after finitely many steps, C will complete with Q holding afterwards", abbreviated {P} C {Q}. This has a nice compositional structure, for example if {P} C1 {Q} and {Q} C2 {R} then {P} (C1; C2) {R}. This has since been refined into Separation logic in order to avoid the expressions P,Q,R talking about the entire state of the machine but rather only the part that matters for the code segment in question.

 

Does the user have to specify the steps themselves or can the compiler help generate them or is it a totally different system? If MMC produces proofs which are checkable by MM0 does that mean they are similar to MM proofs in style? It’s interesting to me that MM0 can check both MM proofs and x86 proofs and yet remain small, that is very intriguing.

x86 is just a definition, like you would make in set.mm. It's just a very large and complicated definition split into many sub-functions. Every individual theorem is relatively small, and it is possible to prove the semantics of a single instruction without too much difficulty, just like one might unfold the definition of a group to prove that multiplication is associative.

The user provides a proof at the level of the input language, which looks like C with this separation logic layered on top. The compiler will progressively refine this C code through several intermediate stages, until eventually arriving at x86 machine code, and stage has its own semantics and each transformation is associated with a semantics preservation theorem. So while the code is being refined down, the proof is being built up simultaneously, so that when you get to the end, you have machine code but also a proof of semantic correctness using that original separation logic proof as the guide. So it's partially human written and partially constructed by the compiler.

The actual proof object that is generated is essentially a MM theorem, using lots of carefully constructed lemmas. It shouldn't be egregiously large, but it probably won't be especially readable.

If so there has been a lot of work to build up the set.mm database of proofs, is there a similar process to build up MMC functions and their associated proofs? For example given a verified addition function you could build a multiplication function and then a function for the multiplication of matrices or something.

Yes, in a sense. I mentioned that the compiler needs carefully constructed lemmas for the translation between intermediate stages. These lemmas have to be proven manually, and essentially form a part of the compiler. Without them, the compiler can't compile (or at least, it can't compile to produce a proof). But there are more lemmas that can be proven beyond the basics, and what these do is effectively make the language itself more expressive, adding new types and new code constructs in the programming language. For example one might define a "for" loop in terms of "while", prove some lemmas about the lowering process, and then MMC will have a "for" loop.

The other half of the work is writing specific programs in the language. Because proofs are embedded in the code, this is a nontrivial task, and in a sense represents the "meat" of the work for a particular program. If you have a program that enumerates primes, this is where facts about primality get involved. Here reuse is also possible, forming a "verified software library" of functions with proven properties. I'm not making any serious effort to modularize the verifier in this way, but for general use this is certainly something that should be developed.

 

I think these formal methods are obviously the future of mathematics so it’s really cool to be able to watch them develop. I also think there may be interesting applications to The AI Control Problem, for example letting an AI expand its capabilities iff it can prove the expanded system is constrained in the same way it is constrained itself. There is some similar paradigm to what you are doing about a system verifying itself (or it's offspring). This sounds like it might make it feasible to control an arbitrarily sophisticated system which is cool because without control there are a lot of worries. I asked Stuart Russel about it in a Reddit AMA and he said he’s considered formal proofs as a method for AI Control which is interesting. I’ve watched enough Stargate SG-1 to know I don’t want to have to deal with replicators.

:)

Mario

[Jon P]

Awesome Mario, thanks for the response, it takes me a few days to respond because I have to think a lot ha ha.

I can see how fully symbolic proofs are better. I can also see how you arrived at this place if separation logic has been implemented in COQ and HOL, it feels like a big step from MM.

It makes sense too that x86 can be formally specified. I think it’s really clever that the compiler can progressively refine the proof down to lower levels, this lets the humans just read the high level stuff which is cool. Do you have the x86 definitions in a file somewhere? I’d be interested to see them, though may well not understand.

Can I ask what the relationship between MM1 and MMC is? For example if I am writing a program in MMC can I use MM1 to help me produce the high level proof for the program or is MM1 more a tool for making MM0 proofs only? I imagine some sort of proof assistant for MMC would be helpful.

I am also curious as to what else you want to use MMC for, it feels like you’re building a whole, very sophisticated, programming language just to write one program in it (MM0). Do you have other ideas for projects? I can imagine there are a lot of applications for things like aerospace, cryptography and finance etc where people need really robust code.

How far through implementing all this are you? I know you’ve done quite a lot of it which is impressive. What are your next steps?

Also do you want any help? I am 99% sure I don’t have any skills which could be of use to you and I am trying to help with the OpenAI proof assistant a bit when I have energy so I don’t think I will be able to help much. However I do love this field so want to get more into it and if others are reading this they may be interested too.

Mostly I’d just like to be encouraging, what you’re doing is incredible. I think formal methods are definitely the future.

[Mario Carneiro]

On Wed, Aug 5, 2020 at 4:09 AM Jon P <drjonp...@gmail.com> wrote:

Awesome Mario, thanks for the response, it takes me a few days to respond because I have to think a lot ha ha.

I can see how fully symbolic proofs are better. I can also see how you arrived at this place if separation logic has been implemented in COQ and HOL, it feels like a big step from MM.

It makes sense too that x86 can be formally specified. I think it’s really clever that the compiler can progressively refine the proof down to lower levels, this lets the humans just read the high level stuff which is cool. Do you have the x86 definitions in a file somewhere? I’d be interested to see them, though may well not understand.

Indeed I do: https://github.com/digama0/mm0/blob/master/examples/x86.mm0

It would be better with syntax highlighting but you will need to open it in vscode for that.

 

Can I ask what the relationship between MM1 and MMC is? For example if I am writing a program in MMC can I use MM1 to help me produce the high level proof for the program or is MM1 more a tool for making MM0 proofs only? I imagine some sort of proof assistant for MMC would be helpful.

MMC is a DSL inside MM1. That means that an MMC program is written as the input to a tactic running in MM1. For example, https://github.com/digama0/mm0/blob/master/examples/verifier.mm1 contains the draft of the MM0 verifier in MMC. The code is all MM1 until line 38, when we enter what is essentially a big quoted expression within which the language is changed to MMC and you start seeing keywords like "proc" and "typedef" more reminiscent of C than a proof language.

In certain places, like at the _ on line 69, a proof is expected, and this proof has the same format as the usual MM1 proofs. The compiler will specially prepare a proof context so that even though you are actually inserting a bit of proof in the middle of the giant proof the compiler is working on, you don't see any of that and you only have the facts that you request so as to not make it overwhelming. When you are in these little proofs, you can use all the usual tools that MM1 provides. Alternatively, if the theorem is quite heavyweight and you don't want to embed it in the middle of the MMC program, you can interrupt the program between any top-level items (i.e. at the beginning of the function), finish the tactic invocation and the do block and then write a theorem in MM1 just like one writes pure mathematical theorems, give the proof, then return to MMC and refer to the theorem in the mini proof block where it is needed.

I am also curious as to what else you want to use MMC for, it feels like you’re building a whole, very sophisticated, programming language just to write one program in it (MM0). Do you have other ideas for projects? I can imagine there are a lot of applications for things like aerospace, cryptography and finance etc where people need really robust code.

Ha, you noticed. I will try to keep the sophistication down for the first draft because it's definitely possible to overengineer in this area, and this was specifically something I wanted to avoid. But I'm also doing a PhD dissertation with this project and want to make sure I get something independently useful even if the MM0 verification turns out to take longer than expected.

 

How far through implementing all this are you? I know you’ve done quite a lot of it which is impressive. What are your next steps?

The MMC implementation is just starting. I have just started on the typechecker, which is responsible for doing type inference and passing around typing proofs in the separation logic, but I also haven't written any of the proof support that the compiler needs yet, for example the separation logic itself hasn't even been defined yet, and I'm waiting to see the shape of the lemmas that the compiler requires before writing that so that I can be sure it is accomplishing the task set to it (and no more).

There is also still some pure MM1 work to be done to prove x86.mm0 and mm0.mm0, which mostly entails proving the existence of various kinds of inductive types. This is the sort of thing that every proof assistant automates eventually, so I'm not sure if it's worth it to push through the 10 or so inductive datatypes I need by hand, or write the tactic to solve them all (which is usually worthy of a research article on its own but is a considerable time sink). In metamath we never bothered to automate this kind of thing, possibly because there were never enough CS-themed projects to necessitate recursive data structures built out of disjoint union and cartesian product. But these are extremely common in programming languages (they are called "algebraic data types"), and they are useful for modelling syntax, for example you might define the collection of all propositional logic expressions as:

inductive prop_expr

| imp : prop_expr -> prop_expr -> prop_expr

| not : prop_expr -> prop_expr

| var : NN0 -> prop_expr

and from this specification, the datatype compiler will generate a type "prop_expr" with functions "imp", "not", "var" with the stated types, as well as a recursion and induction principle for defining functions by structural recursion and proving properties by structural induction, for example

|- A. a e. prop_expr A. b e. prop_expr (P [a / x] -> P [b / x] -> P [imp a b / x]) /\

   A. a e. prop_expr (P [a / x] -> P [not a / x]) /\

   A. n e. NN0 P [var n / x] ->

   A. x P

for the induction principle, and

|- rec_prop_expr I N V (imp a b) = I a b (rec_prop_expr I N V a) (rec_prop_expr I N V b)

|- rec_prop_expr I N V (not a) = N a (rec_prop_expr I N V a)

|- rec_prop_expr I N V (var n) = V n

for the recursion principle. The work being done now in set.mm on well founded recursion along general well founded orders is the first baby step in this direction but we're quite far from having the whole thing automated away in MM.

Also do you want any help? I am 99% sure I don’t have any skills which could be of use to you and I am trying to help with the OpenAI proof assistant a bit when I have energy so I don’t think I will be able to help much. However I do love this field so want to get more into it and if others are reading this they may be interested too.

I have a bunch of proofs to be done, which I could outsource if anyone is interested. For example x86.mm1 currently contains a huge number of fairly simple theorems that have been stated and not proved, so it's fairly straightforward to get into it if you (or others) are interested. You would have to learn the MM1 language, but that's not a terrible side effect, and I would be happy to help with onboarding any way I can.

 

Mostly I’d just like to be encouraging, what you’re doing is incredible. I think formal methods are definitely the future.

Thanks!

Mario

[Jon P]

Thanks so much for all these explanations Mario, it's really kind of you. What you're doing is awesome. I have to read each message 5 times to try and pick apart the ideas you're using, I mean I've been programming for a few years and have never heard of algebraic data types, though have used linked lists and trees a decent amount.

I'd love to be able to help but I think I'm several levels too far down in terms of skills, hopefully I'll keep progressing though. I have been trying to learn the new OpenAI tool, which is really cool, and help Norm by marking some of the old groups and rings stuff for deletion and do my own project to prove the area of a triangle, which has been stuck for a long time now. So I think maybe I have enough things to chew on of the right size for me. 

I'll be watching out for your future talks though! Keep us updated as it's an awesome project. My friend said he thinks the proof system that will win in the end (as I think network effect will probably drive mass adoption of a single protocol) is the one which can translate from the most others so I think you are probably winning at the moment in that respect. :)