Comment Re:relax (Score 1) 549
You still have to tell the computer what to prove.
Indeed. Generating proofs is a bit like generating code. I can picture a computer generating proofs or code, but at least in the foreseeable future, I can't see a computer thinking of interesting conjectures (things to prove) or program designs (things to code).
Because most people encounter math as a tidy collection of Big Theorems and their accompanying proofs --- after all, even those who take math at university aren't likely to see anything remotely new unless they're math graduate students --- and because math usually only makes the news papers when someone has solved a really hard problem (like proving Fermat's last theorem), it's easy to get the impression that what mathematicians do is basically trying to come up with proofs for More Or Less Big Theorems. I'm only a budding math major myself, but I get the impression that the problem most mathematicians (well, the researchers anyway) face is rather that of finding interesting things to prove. Software can definitely help, but only as the tool of a mathematician.
Indeed. Generating proofs is a bit like generating code. I can picture a computer generating proofs or code, but at least in the foreseeable future, I can't see a computer thinking of interesting conjectures (things to prove) or program designs (things to code).
Because most people encounter math as a tidy collection of Big Theorems and their accompanying proofs --- after all, even those who take math at university aren't likely to see anything remotely new unless they're math graduate students --- and because math usually only makes the news papers when someone has solved a really hard problem (like proving Fermat's last theorem), it's easy to get the impression that what mathematicians do is basically trying to come up with proofs for More Or Less Big Theorems. I'm only a budding math major myself, but I get the impression that the problem most mathematicians (well, the researchers anyway) face is rather that of finding interesting things to prove. Software can definitely help, but only as the tool of a mathematician.
