> 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. >
I wonder if you have CS or math background. In my experience, the language is a defining factor for most programmers, especially familiar with functional programming. And they should feel right at home using dependently typed programming languages vs. set theory. Although, there is Lisp, of course, but it has abstract syntax at least. For me, the ad-hoc syntax which uses Metamath is the biggest obstacle and tactics come after that. The whole experience reminds me programming in assembler language which is nice in simple cases, but becomes annoying when it is too complex. The irony is that while Metamath is trying to be faithful to traditional mathematical notation, mathematicians are adopting programming languages, like Lean (or even APL like Iverson) at the same time. My first motivation which turned my attention to Metamath was a desire to look at all the gory details of a proof. But soon I found out that I don't really need them all. What I needed instead was a confidence in a proof verifier and the level of details that is "just enough" to understand full argument. Too much technical details actually distracts me from the ideas and I can't see the forest for the trees. And while I can fold the proofs on the web it is still boring to use mmj2 for that. But that's just me, of course. All people are different. -- 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/ad4366e8-6ddc-488f-b17a-b9d4d1848b46n%40googlegroups.com.
