On Wednesday, June 9, 2021 at 4:45:08 PM UTC-4 di.gama wrote: > On Wed, Jun 9, 2021 at 11:21 AM Jon P wrote: > ...
> Is it true that any AI system built on metamath will need these same >> foundations? For instance it will need a parser for the database, a >> verifier and also it will need a function which: for any statement returns >> the possible substitutions/theorems which could be applied. >> > > No. The brute force search method just described is not practical above > about 15 steps or so. It has been used for parts of > http://us.metamath.org/mmsolitaire/pmproofs.txt but it runs out of steam > even before the end of that list. > ... Actually the proofs there with up to 21 steps are the shortest possible. All possible proofs up to this length were exhaustively generated and their final theorems compared to the list. This was about 30 years ago, using a BASIC+ program running on a VAX for several days. Today's computers might be able to go a little further. The number of possible proofs to generate and test is the Catalan number of the number of D's (modus ponens applications), multiplied by 3^([number of D's]+1) since there are 3 possible axioms to try at each non-D step. Many of these will abort early because unification will not be possible, e.g. D23 is a valid proof, D32 is not. The program drule.c mentioned there will let you play with this: "./drule D23" will return ">>>~P~QQ>>~P~QP" (Polish notation) and "./drule D32" will return "?Error: Proof is invalid". Proofs with more than 21 steps there were originally found by hand (me), with shorter ones found for many of them over the years by various clever people. I've thought that pmproofs.txt might be interesting for some kind of AI experiment due to its simplicity, but AFAIK nothing has been tried. There was a "genetic algorithm" experiment by George Szpiro in 2018 that found 3 shorter proofs automatically. I think all other shorter proofs were basically found by hand, sometimes assisted by a custom program. The proof for *2.16 was mentioned here: https://codegolf.stackexchange.com/questions/161172/ and was the shortest (59 steps) of the ones that people there found. Norm -- 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/62a68360-05b8-4ea7-9b99-dc6cee3218fan%40googlegroups.com.
