The above poster is correct, I just looked it up. I was thinking of the corresponding optimization problems. Obviously, IANACT.

Didn't read the article, but it's totally bunk. The two dimensional TSP is not NP complete (unless P=NP), it's actually in P. In order for the 2d TSP to be NP complete, you have to allow crossing paths and arbitrary values (not just the euclidean distance between the nodes) for the lengths of the edges.

The variation in human brains is only a very small part of the potential variation in brains containing 100 billion neurons. I'm not saying we can engineer a million line program to grow a human brain, only that we'll never know whether it's possible unless someone actually does it.

"There are lots of very smart people actively trying to simulate human intelligence. While a million lines of code is a fairly large undertaking, it's not an unmanageable amount." There were lots of smart people trying to prove Fermat's last theorem, and it took hundreds of years to succeed. In the end, the proof was only a few hundred pages, which is way less than a million lines of code. Writing million line programs is easy, but you are basically saying we have a good understanding of space of algorithms that can be described in a million lines, which is clearly false. In general, the apparent complexity of a program's output has little to do with how short that program is.

"ANYTHING into 1 bit by using the function that takes that and returns the bit "1" (and which takes anything else and returns "0" + that)" And how many bits do you think it would take to encode that function?

"If it was possible to do in a million lines of code, it would have been done by now." That's a pretty tremendous leap in logic. The only way you could know this for certain is to check every million line program and see if it simulates a brain, which isn't ever going to happen, at least not in this universe.

And that's why internet 2 will just be complicated network of pneumatic tubes.

You don't need additional axioms to define the reals, they are defined using infinite sequences of rational numbers. Oh, and any creative enough theorem prover (mechanized or not) would eventually invent analysis (the study of real numbers)just because it is useful to number theory. Most really hard questions in number theory are difficult or impossible to prove without analysis.