On Tue, 8 Sep 2020 10:31:37 +0800, Thierry Arnoux <[email protected]> wrote: > I would be a bit careful with David’s list, some theorems might be high on > the list because they are very relevant, not because they are very easily > formalizable, but it’s still a good reference. > > Even though the basic principles are very simple, it takes skill and mileage > to find which elementary theorem to apply to reach your goal and build a MM > proof. Tools like OpenAI assistant and MMJ will help greatly for that.
I agree. Start with something absurdly simple, so you're not trying to learn too many things simultaneously. I posted some Metamath-related video tutorials on Youtube. You may find them helpful. --- David A. Wheeler -- 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/E1kFU5c-0005Xz-5D%40rmmprod06.runbox.
