On August 12, 2020 2:01:43 PM EDT, Stef O'Rear <[email protected]> wrote: >This is one of many reasons I'm uncomfortable with metamath's recent >"pivot to AI"
I, for one, welcome our new artificial intelligence overlords :-). To be fair, there have been metamath efforts using artificial intelligence for years. Artificial intelligence has been involved in theorem proving for many many decades. I don't think there's anything to be uncomfortable about. Humans still need to decide what the axioms are & what is worth proving. Perhaps the lesson is that if we want certain conventions to be followed, we need to express them so that they can be automatically enforced. The "discouraged" marks, for example, can help do this. I think that is entirely in keeping with the overall approach of metamath.. everything to be explicit and automatically verified. --- David A.Wheeler -- 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/73515BC9-364D-4FF3-9CCA-C8361751C2A5%40dwheeler.com.
