Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> The existence of closed systems does not imply all systems are closed

I never said they were. Just that we don't know one way or the other.

> P=NP means you can get computers to write their own math proofs.

Yes and no. It means the computer can fill in the technical details of a proposition you've already formalized. But mathematicians only ever sketched those parts in papers anyway.

> Maybe we can start birthing mechanical babies, I don't really know.

You're not making any sense. Try starting with more concrete things before waxing philosophical.



I've read from mathematicians who consider their computer to be a tool, and from others who see the computer as a partner. As a hobbyist who studies automated theorem provers (like coq), there is so much elegance that goes into the computational proofs in order to even construct such a program that allows a mathematician to do their work.

Can you honestly say that it doesn't take an extreme amount of effort to construct the perfect typing system that allows you to even begin to be able to write a proof with a machine? People have to prove that theorem provers are correct with respect to that which what they define. This is no trivial task, it's an entirely different domain of knowledge.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: