Hi Stan, Your results shortening proofs are very impressive, and very interesting!
I'd be curious to know whether you have to start from existing proofs, or you generate new proofs from scratch. I assume you generate proofs from scratch, but chose to work on existing proofs because they are known to be provable? In addition to existing proofs, would you also work on new proofs? (there are several of them in set.mm, you can find them by searching for " ? $. " or " ? @. "). How would the AI behave if given a statement that cannot be proved? (syntactically, or worse, semantically wrong) BR, _ Thierry -- 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/531b6980-d1ba-e90f-a47d-c0830bc709cb%40gmx.net.
