Is it common/reasonable to write proofs directly? I am in a similar situation as Stanislas and have proved a good handful of propositional calculus results along with 2p2e4.
This has given me a decent handle on finding relevant theorems using metamath's search facilities, and for the short proofs I have been working with so far, this somewhat austere setup has been quite nice. However, with longer proofs what problems can I expect to encounter that mmj2 and friends aim to solve? Jon P <[email protected]> wrote: > Hi Stanislas, > > Getting into metamath can be quite hard so keep asking for help if you need > it, more people is always nice! > > Not sure how far you have got but I suggest you get MMJ2 proof editor and > then work on these problems in Filip's mathbox. Try not looking at the > proofs and the producing a proof by yourself. That is a good way to start > with the actual mechanics I think. > > http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b > > Here are some tutorials for MMJ2, > https://www.youtube.com/watch?v=87mnU1ckbI0&list=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC > > and it can be found here, http://us.metamath.org/#mmj2 -- 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 on the web visit https://groups.google.com/d/msgid/metamath/2QV1HUGO6GQQ5.2JS6D6KCGYK3R%40wilsonb.com.
signature.asc
Description: PGP signature
