Hacker News Reader

We already have commoditised math solvers for any number of (relatively) trivial problems.

What we haven't automated is mathematical creativity, which is a completely different class of problem.

The whole difficulty of the hard complexity questions such as "Is P=NP?" hides in the non-trivial, "corner" cases. Sure, we have SAT solvers that are by many practical standards really good. P=NP would imply that we can relatively easily find polynomially long proofs to many hard propositions, such as the P=NP problem itself! Or many other open mathematical problems.

Creativity is an anthropomorphic, abstract concept, a way of describing human ways to find solutions. What really matters is the proofs.

Reply on news.ycombinator.com