Very interesting work, Stanislas! Great to see the cooperation between classical AI (in the form of theorem provers) and modern machine learning.
I have several questions which I hope you could comment on. 1. Is your algorithm able to eventually prove any provable result given enough time? In other words, is the proof search exhaustive? 2. Does it work for any metamath database or only for set.mm? 3. Does your prover use facts it learned from the training set or it uses theorems from the database? I.e. if you were to change all theorem names in the database so they are different from ones used in the training set, would the model still work well? What if you "jumble" theorems (say, change order in conjunctions of clauses), will the model work better than a usual search or it will be ineffective? 4. Related to previous questions, can you transfer skills the model learned from one database to another? For instance, can it learn to prove intuitionistic theorems faster if it was first trained on classical logic? 5. Do you get (or hope to get) some sort of discriminative/generative model as a byproduct? For example, given a trained model, can you evaluate the probability that some proposition is true? Can you autosuggest possible theorems/steps to use based on your model? Clearly this question has proof assistants in mind :-) I would also like to suggest some theorems for a test: if the answer to question 2 is positive, you could try your algorithm on quantum logic (see http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see http://us2.metamath.org:88/ileuni/mmil.html). As for set.mm, it would be interesting to see how it behaves on calculational proofs like, for example, proofs that certain numbers are prime (see http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another interesting topic is proofs in the Tarskian geometry section (see http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly use propositional calculus and Tarski axioms, which reduces the search space. Geometric proofs also have some sort of "geometric intuition" behind them which may (or may not) be helpful for finding proofs. -- 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/353a6707-14fd-4c08-a6e6-611972c84916%40googlegroups.com.
