Re:Computational Knowledge and the Future of Pure Mathematics
by Someone on Tuesday August 12, 2014 @05:07PM
(#8170188)
There is at least one thing Wolfram skimps over:
"So in principle one can imagine having a system that takes input and generates “interesting” theorems about it."
I can imagine having a spaceship that goes faster than light, too. It is more than slightly harder to actually build it.
Generating theorems is easy (it may even be possible to generate all theorems in order of increasing length of their proof and not get stuck into generating evermore longer proofs of theorems encountered earlier, but I am not sure of that)
However, we have only very faint ideas about what constitutes an interesting theorem (are theorems even dull or interesting independent of their known proofs? if one finds a new interesting proof for a theorem that previously only had a dull proof, I think the theorem can become less dull), and certainly do not know how to programmatically discriminate them from dull ones.
"So in principle one can imagine having a system that takes input and generates “interesting” theorems about it."
I can imagine having a spaceship that goes faster than light, too. It is more than slightly harder to actually build it.
Generating theorems is easy (it may even be possible to generate all theorems in order of increasing length of their proof and not get stuck into generating evermore longer proofs of theorems encountered earlier, but I am not sure of that)
However, we have only very faint ideas about what constitutes an interesting theorem (are theorems even dull or interesting independent of their known proofs? if one finds a new interesting proof for a theorem that previously only had a dull proof, I think the theorem can become less dull), and certainly do not know how to programmatically discriminate them from dull ones.