> As for intuitionistic logic, I was interested in how well the model trained > on set.mm would transfer its skills to iset.mm. Also many theorems from > iset.mm have their set.mm counterparts, so theoretically you could contribute > to iset.mm by trying to prove some existing set.mm results in the > intuitionistic setting.
Very interesting. Arguably higher level theorems proofs would eventually become ~~ similar? > Basic arithmetic results are interesting since you can easily generate many > "theorems" of the form "12 + 29 = 41" and you can even roughly estimate > the amount of steps such theorems should require. Proving these identities is > a purely mechanical task (as far as I remember, Mario even wrote a program to > do that), so it's interesting to know whether your model can learn to perform > such a feat. We have and leverage proof generators for a number of these tasks :+1: > As for Tarskian geometry, results in that section use a relatively small > subset of set.mm theorems and have an underlying geometric intuition. In my > opinion it's interesting to evaluate if your system performs better on > geometry theorems rather than on propositional calculus/set theory results. > Also, elementary geometry section has a collection of results with statements > but without proofs (marked by "? @" and "? $.", as mentioned by Thierry). Good to know, thanks for that! -stan On Tue, Mar 31, 2020 at 12:27 PM savask <[email protected]> wrote: >> >> How large are the quantum logic and intuitionistic logic databases? >> What would be the main value of applying our proves on them out of >> curiosity? > > > Quantum logic database is ~560KB, intuitionistic logic database is ~3.7MB. > Trying out your prover on the quantum logic would be interesting because of > how different it is from usual logic. Also typical proofs in that database > seem to be smaller than in set.mm, so perhaps your algorithm has a higher > chance of coming up with proofs in quantum logic. > > As for intuitionistic logic, I was interested in how well the model trained > on set.mm would transfer its skills to iset.mm. Also many theorems from > iset.mm have their set.mm counterparts, so theoretically you could contribute > to iset.mm by trying to prove some existing set.mm results in the > intuitionistic setting. > >> Do you believe the community would be interested in an online tool to >> discharge goals? > > > I think others are in a better position to comment on this, since I haven't > formalized anything in quite a while. Personally, I would really like to see > a Metamath Solitare kind of tool which would autosuggest you steps based on > your model, just to explore how well it works in pair with a human operator. > >> The model is capable to prove some of the prime number theorems, but >> proofs sizes do grow very fast. I believe we already proved 17 as an >> example. Out of curiosity, why are you specifically interested in >> these two classes of theorems? > > > Basic arithmetic results are interesting since you can easily generate many > "theorems" of the form "12 + 29 = 41" and you can even roughly estimate > the amount of steps such theorems should require. Proving these identities is > a purely mechanical task (as far as I remember, Mario even wrote a program to > do that), so it's interesting to know whether your model can learn to perform > such a feat. > > As for Tarskian geometry, results in that section use a relatively small > subset of set.mm theorems and have an underlying geometric intuition. In my > opinion it's interesting to evaluate if your system performs better on > geometry theorems rather than on propositional calculus/set theory results. > Also, elementary geometry section has a collection of results with statements > but without proofs (marked by "? @" and "? $.", as mentioned by 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/10f37787-f926-4989-9adf-a3daf972acdd%40googlegroups.com. -- 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_0xSMQKYXBXsVMSYzkJJf0ELrYaLx_s79jZyjZ%3DwLa1YuQ%40mail.gmail.com.
