MM1 proofs with tactics, how are they created/understood/analyzed ?

[Sylvain Kerjean]

Hello,

I try to understand MM1 tacticts, but they seem so intricated to me when i look at code (peano.mm1 for example), i wonder what tools people use to elaborate proofs with tactics, because i guess they are not entirely man-made. I used the vscode plugin, but it did'nt really help to understand the tactics because of the lisp-like syntax/keywords.

[Mario Carneiro]

The short answer is that I wrote both the proofs and the language the proofs are written in myself, so it might be difficult to get up to speed on it as a third party. One resource I can point to to learn the metaprogramming language is:

https://github.com/digama0/mm0/blob/master/mm0-hs/mm1.md#evaluation

which goes over the lisp language syntax and builtin functions. There is also a tutorial here: https://www.youtube.com/watch?v=A7WfrW7-ifw which shows how proofs can be written, although it doesn't go in too much detail on the metaprogramming language. The file is written more or less as shown in the video, using a combination of writing proofs from the outside in with `_` at all the unfinished positions, as well as (focus) blocks once the proof becomes large enough to be difficult to work with. Metaprogramming inside proofs is very rare, but sometimes you will see variable declarations or functions inside a proof when it has a repetitive structure.

On Fri, Nov 14, 2025 at 11:46 AM Sylvain Kerjean <sylvain....@gmail.com> wrote:

Hello,

I try to understand MM1 tacticts, but they seem so intricated to me when i look at code (peano.mm1 for example), i wonder what tools people use to elaborate proofs with tactics, because i guess they are not entirely man-made. I used the vscode plugin, but it did'nt really help to understand the tactics because of the lisp-like syntax/keywords.

--
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 visit https://groups.google.com/d/msgid/metamath/CAC0Jddi-jHk%3DfOm%3DEK59Vtedj_Wne778kBFeSvPNM%2B2i8r5bZQ%40mail.gmail.com.