More AI "Calculemus!": Leibniz believed calculation would be the key to settling all human disagreements. A famous attempt was Godel's 1970 ontological argument, which was puzzled over and discussed by philosophers for decades, until 2013 when an AI-based theorem prover discovered an inconsistency that has been confirmed by a proof verifier (Isabelle I think). https://www.ijcai.org/Proceedings/16/Papers/137.pdf
An AI paper under review is https://openreview.net/pdf?id=BJxiqxSYPB that "advances the state of the art of automated theorem proving in Metamath." I don't know who wrote it. Norm On Wednesday, January 15, 2020 at 7:14:02 AM UTC-5, fl wrote: > > > > > https://twitter.com/ylecun/status/1217177049346916352 > > -- > FL > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7f9c0458-56dc-4bdc-b1af-e7b2487824fa%40googlegroups.com.
