> > Why on earth anybody would be interested in Metamath which is even more > obscure than Coq or Lean? > > Is it? I've heard of Lean, vaguely, but not really. I've looked at > Coq, and would probably pick it up if I needed to formally prove a > program, but nothing beats the Metamath website for sheer promise from > a mathematical perspective. Maybe in a academic setting, the others > are well-known, but to a general audience interested in mathematics, I > don't see any real alternative to Metamath. >
What's the most surprising in such discussions is how little people in the field know about each other. If you look at Coq's community they know very little about Lean and vice versa, and both know almost nothing about Metamath. It looks like the best way to dispel superstitions is to post about Metamath on Hacker's news where they are discussing some Lean related talk. And I think David and Mario deserve much credit for popularizing Metamath on different forums. -- 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/188b848e-5de5-42e9-a475-34d4128572d7%40googlegroups.com.
