> I've been using metamath lamp to formalize the proofs, and I've been sometimes wondering if its proof searching utility is missing some short arguments. I haven't tried comparing it with metamath.exe's improve command, though.
I don't know about metamath lamp, but the search power of the metamath.exe 'improve' command is very minimal. For the most part, I use it in the form of 'improve last /depth 1' to fill in some basic propositional logic steps. It isn't really much useful beyond that (it has more options which can be consulted by typing 'help improve', although they considerably slow down the proof search and I rarely have success with them). I'd say that the minimizer is probably the most advanced piece of automation that metamath.exe has (I put the minimized proof of Day 20 in adv2025.mm <https://github.com/GinoGiotto/set.mm/blob/adv2025/adv2025.mm>). The thing I like metamath.exe isn't automation, but rather that it's fast to create proofs once you get confident with the commands. Since it's a CLI, you avoid many mouse movements, and so far I've preferred this design over editor-based proof assistants. > they have an automatic prover for GL https://link.springer.com/article/10.1007/s10817-023-09677-z Maybe in the worst case one could try to extract the proof from this utility, though I'm not sure if it's possible. Depending on the decidability of GL (which I don't know), one could attempt writing tactics in Rumm as well. However, the resulting proofs would likely be longer than the ones done by hand (and they might need work variables <https://github.com/digama0/mmj2/blob/master/doc/WorkVariables.html>, which Rumm doesn't have). > Thanks! I haven't been able to find this proof anywhere in the literature, so this might be a useful reference for some other people as well. Perhaps I can explain my way of thinking a bit, since sources for a proof of Day 20 seem to be scarce (spoilers start here): Statement of Day 20: |- ( []. ( ( []. ph -> ph ) -> -. []. []. F. ) -> []. []. F. ) In general, when I approach propositional logic statements, I reduce them to what's called 'implicational normal form'. It doesn’t seem to be as popular as the conjunctive and disjunctive counterparts, but it's probably more efficient for statements that already use primitive symbols. In case someone is interested in learning this strategy, I made a propositional theorem prover that uses it https://groups.google.com/g/metamath/c/Dlc-Lf7MF1A (it can also be used as a SAT solver). Any pure propositional logic statement can be reduced to a set of statements in implicational normal form, and while it does not guarantee success when we go beyond that, it's still worth trying in some cases. The first step of this strategy is to attempt to "split" nested hypotheses, in this case we have ( ( []. ph -> ph ) -> -. []. []. F. ) which can be split into a conjunction of two expressions ( ( -. []. ph -> -. []. []. F. ) /\ ( ph -> -. []. []. F. ) ). Such step is equivalent to applying ~jaob, but using implication instead of disjunction. We also know that the box operator distributes over conjunction (theorem ~distrconj), so we can fully split the hypothesis of Day 20 into two simpler ones: |- ( []. ( -. []. ph -> -. []. []. F. ) -> ( []. ( ph -> -. []. []. F. ) -> []. []. F. ) ) With ~axk4 and ~ax-distrb we can change the second hypothesis to: |- ( []. ( -. []. ph -> -. []. []. F. ) -> ( []. ( []. ph -> []. -. []. []. F. ) -> []. []. F. ) ) Why did I do this to the second hypothesis? Two reasons: the first is that we now have '[]. -. []. []. F.', which is an instance of '[]. -. []. ph'. The latter is known to be "strong" because we can prove any other boxed expression from it. This property is expressed by ~kurbis, and for Day 20 we use the equivalent variant: |- ( []. -. []. ph -> []. ps ). Of course, gaining strong hypotheses is something we usually want to see in our proof developement. The second reason is that we get '[]. ph' on one hypothesis and '-. []. ph' on another, which could be combined to obtain a contradiction (ending with ~luk-3) if we manage to pair them together. Now we reduce the goal to a set of statements in implicational normal form. The straightforward way of doing it would be to apply ~ex and ~monimpconj to first eliminate external boxes: |- ( ( ( -. []. ph -> -. []. []. F. ) /\ ( []. ph -> []. -. []. []. F. ) ) -> []. F. ) And then split hypotheses with ~ja to get 4 statements in implicational normal form: |- ( -. -. []. ph -> ( -. []. ph -> []. F. ) ) ----> ~com12 and ~luk-3 |- ( -. -. []. ph -> ( []. -. []. []. F. -> []. F. ) ) ----> ~a1i and ~ kurbis |- ( -. []. []. F. -> ( -. []. ph -> []. F. ) ) ----> ???? |- ( -. []. []. F. -> ( []. -. []. []. F. -> []. F. ) ) -----> ~a1i and ~ kurbis Unfortunately, one of those four statements cannot be proved (all of them need to be provable), so something went wrong. This was the step that took me the longest to figure out, but the basic principle is that we need to insert another step before arriving at the implicational normal form. The fix is to apply ~syl and ~ax-gl to the conclusion before applying ~monimpconj. The reason of doing that is that we gain another hypothesis (which is []. []. F.): |- ( ( []. ( -. []. ph -> -. []. []. F. ) /\ []. ( []. ph -> []. -. []. []. F. ) ) -> []. ( []. []. F. -> []. F. ) ) We apply ~monimpconj to eliminate external boxes: |- ( ( ( -. []. ph -> -. []. []. F. ) /\ ( []. ph -> []. -. []. []. F. ) ) -> ( []. []. F. -> []. F. ) ) And finally, we split the hypotheses with ~ja: |- ( -. -. []. ph -> ( -. []. ph -> ( []. []. F. -> []. F. ) ) ) -----> ~com12 and ~luk-3. |- ( -. -. []. ph -> ( []. -. []. []. F. -> ( []. []. F. -> []. F. ) ) ) ----> ~a1i, ~a1d and ~kurbis. |- ( -. []. []. F. -> ( -. []. ph -> ( []. []. F. -> []. F. ) ) ) ----> ~ a1d, ~com12 and ~luk-3. |- ( -. []. []. F. -> ( []. -. []. []. F. -> ( []. []. F. -> []. F. ) ) ) -----> ~a1i, ~a1d and ~kurbis. All statements in implicational normal form are now provable, so we have a proof of Day 20. -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/c33599e2-e244-4f31-8d14-8e812c362c6en%40googlegroups.com.
