Comment: Re:Fermat & Poincaré (Score 1) 400
It does seem pointless to me to use a computer to create a proof,
I believe the poster you're responding to meant something different.
Say you have some complicated ("chaotic", maybe) formula which determines the behavior of a system. Say just to make it easy the system is a single particle moving under various influences. Now say you know where it is now (it's a big particle like a planet or something, so ignore Heisenberg and such) and you want to know where it will be 500 seconds later. Many systems currently require iterating through all 500 steps or other time intensive tasks in order to find that answer due to only having approximate methods with which to solve the system. An analytic solution as the OP was using it would be more like a function where you plug in 500 and get your answer. If you plugged in 500 Billion, you'd find that answer in more or less the same amount of time as for 500.
So computers can potentially make taking the wetware time to find an analytic solution to an equation (system of differential equations, optimization problem etc.) less valuable in some of the meanings of the word, if in practical applications you can get say 10 decimal places closer to the answer than you need in microseconds.
Computers proving theorems is a different thing. The Four Color Problem is the most common example of that I'm aware of. I think it's cool that people managed to do that, but it's unsatisfying in that it doesn't really add much in the way of understanding. Some theorems people have come up with are similarly unsatisfying.
Existence theorems which demonstrate that a certain thing must exist in some given circumstances yet provide no clue whatsoever as to how to actually find it would fit. Also, brute force methods in general (which is what the four color proof is, only done via computer to save time) tend to leave mathematicians satisfied that the given fact is true yet still looking for a more elegant solution that provides greater understanding.
Andrew Wiles's proof of Fermat's Last Theorem is fundamentally different in that it did (eventually) provide a huge degree of insight showing unsuspected ties between disparate branches of mathematics. Technically, Wiles didn't prove Fermat's Last Theorem, he proved the Taniyama Shimura conjecture (demonstrating a deep relationship between elliptic curves and modular forms) which someone else had proven would imply FLT if true.