> > 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.
