> 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?
These shortened proofs were indeed noticed as part of applying our prover on the test split we created from set.mm as we continuously evaluate the performance of our systems. In that set up we only have access to the statements. > 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 " ? @. "). This is a great idea. > How would the AI behave if given a statement that cannot be proved? > (syntactically, or worse, semantically wrong) We check the syntax of submitted statements against the wff grammar. If the statement can't be proved, the system would simply search until it reaches a timeout. -stan On Sun, Mar 29, 2020 at 10:59 AM Thierry Arnoux <[email protected]> wrote: > > 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. -- 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/CACZd_0woYBLcMB3Xem4JvXRziedcu_Q3n%3DeWKvpKo8ccOdkdoA%40mail.gmail.com.
