You are probably ready to try out one or more prover systems (or keep
trying out in the case of lean) rather than collect more opinions, but
I'm pretty sure either Lean or methamath set.mm would be suitable in
terms of being able to do things with functions, relations, integers,
etc (and not have to start from scratch on everything). Hope it isn't
intimidating to post the tables of contents of their math libraries, but
it is https://leanprover-community.github.io/mathlib-overview.html for
lean and http://us.metamath.org/mpeuni/mmtheorems.html for set.mm - I
post this just to show that either one of these systems formalizes a
bunch of different areas of mathematics.
Personally, I dabbled in trying to learn the type theory based systems
(coq and isabelle in my case, I suppose it would be lean today) and I
kept coming back to metamath (or now-defunct metamath-like systems). But
this could be as much happenstance (in terms of which ones I encountered
first or first had a reason to get proficient in) as anything which
would have made it difficult for me to learn the others.
On 2/5/22 06:03, Andrew Lubrino wrote:
Wow this is all good advice. Thank you both for the responses. So do
you both think I should go back and continue working with Lean and try
to figure out my problems?
Also, when I say abstract math, I think I’m really just looking to
learn the topics in an introductory discrete math course. I want to
learn about set theory, which includes Cartesian products, families of
sets, functions, and relations. I ultimately would like a system that
I could use to verify proof problems from a graph theory or algorithms
text. I’m pretty sure what I’m looking to learn might actually be
formal logic. Does this change your opinion about what I should be using?
I have a lot to think about, but it does seem like Lean might still be
my best bet. I’ll have another go at it, but I think I’ll still
experiment with mm since it’s so dead simple anyway. Thanks!
On Sat, Feb 5, 2022 at 6:26 AM vvs <[email protected]> wrote:
Hi Andrew,
I think the problem with Lean for a beginner is that it makes
heavy use of tactics, which obscures what's actually happening
in the proof. I'm interested in mm because it's very simple
and tactics aren't part of the system. It would be hard to get
bogged down with lots of technical detail.
I would argue, that using tactics is an advantage for a beginner.
This is exactly because they should hide many boring technical
details which are exposed by a term style proofs. Metamath is good
for verifying and studying existing proofs but has little support
for their synthesis.
I'm sorry if this is a stupid question, but if I learn math
with mm, will I be learning the "right" math?
As Kevin Buzzard frequently said, you should not attempt to learn
math and formal logic at the same time and he is an expert. It's a
double burden and you /don't need/ one to learn the other. I'd
recommend to learn them sequentially and not in parallel.
1. If I do use mm, is there a good way to go about
systematically learning the math content? This evening, I
started with the first theorem in set.mm <http://set.mm>
and proved about the first 5 or 6 theorems. Should I just
try to sequentially prove every theorem in set.mm
<http://set.mm>? Or is this way too much? What's a better
strategy?
There are some people out there who reproved many MM theorems from
scratch, but I don't know their level of proficiency in
mathematics. Mario Carneiro is one of the best professionals in
the field so don't try to compare with him :)
But take any advice with a grain of salt because all people are
different.
--
You received this message because you are subscribed to a topic in
the Google Groups "Metamath" group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/metamath/lO3PPEkLet0/unsubscribe.
To unsubscribe from this group and all its topics, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/CAOcJWNHe7rsHLf2t-qh1LyUghxCx3G9%3DMDcndFyFT-kbpQZcdA%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAOcJWNHe7rsHLf2t-qh1LyUghxCx3G9%3DMDcndFyFT-kbpQZcdA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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/978f67a5-b1e8-914c-235c-abde0cf93a0d%40panix.com.
