I also think the future of mathematics lies in formal proofs. If there were a database of all known proofs creating new proofs would be much easier and more reliable. It would also reduce duplication of efforts which must happen a lot.
One thing I think is there is probably a network effect issue. Given there are many formal proof systems my guess is one will win out and become the standard and then anyone who is choosing which to use will default to that one because it is the one everyone uses. For that reason I think things like Davids new tutorial video are very powerful for the future of the system. Another is the idea of having a web based editor that is easy to access. -- 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/8c7c93d9-c254-4245-8e69-f5bc34111cd5%40googlegroups.com.
