Automatic Proof Generation
Hi, I've been studying Theory of Computation and one of the things that recently came up was the idea of a function which could generate a mathematically sound proof/disproof given some axiom and statement.
I don't like forums very much, but I've been browsing some math forums and looking for stuff concerning proof generation and I couldn't help but notice a post about the decimal expansion of 1. It got me thinking about what it would mean for a computer to 'accept' a proof, because that seemed to be the point of the argument, though it was in terms of people instead of a machine.
Clearly it would be nice to have proof/disproof for classic problems like P = NP, the Riemann hypothesis, the Goldbach conjecture, and the factoring problem. The thing is though, as far as I know, generating the proof could be the same problem as one of these problems. Anyway, I'd love to get some discussion on this, otherwise I'm gone.
Edit: Proof in the context of mathematics (definite yes/no - algorithmic proof process) versus proof in the context of human understanding (agree or disagree - is it convincing)? At the base line, math is math because we say it is math. We made math, it is ours, it is perfect, and yet it only gets us close to understanding the universe, not all the way there. Math is like rational numbers while the universe is like irrational numbers..imagination somewhere in between.