3 ms·
Math research shares those qualities, except small input size if you include the body of all the already-known theorems as an input. I don't know if we'll see m
by abecedarius 9y ago
Math research shares those qualities, except small input size if you include the body of all the already-known theorems as an input. I don't know if we'll see much smarter proof assistants soon, but it doesn't seem absurd to me as a possible development.
- dane-pgp 9y agoActually, just converting all the already-known theorems into a form that can be computationally verified (not just convince a skilled human) would be an interesting starting point. This would really help the metamath project, and perhaps make peer review of mathematical research papers easier: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html