[dselsam]

> Its always funny to realize how "easy" beating human-intelligence is (Chess AI, Go AI, even Mathematical Proofs), but how hard beating human-simple behaviors are.

This is the baseless myth that won't die. We are nowhere near rivaling humans in mathematical proving. Even after a human has proved a theorem, it can be an astronomic amount of work to even explain the proof to a machine after the fact (i.e. to construct a machine-checkable version of the proof), even when using suites of sophisticated software tools developed solely to facilitate this process. Progress has been glacially slow since the field began in the 1950s. Deep learning has had zero impact.

We will have robots that can grasp competently way before we have machines that can rival humans in mathematical proving.

[dragontamer]

True: automated mathematical proving is strictly limited to certain domains right now. First order logic (and other higher forms of logic) are outside the scope of machines, although machines can somewhat solve logic puzzled correctly stated in first-order form (its a semi-decidable problem, so "somewhat solve" is basically the best we can ever hope for).

But move down to boolean logic and symbolic computation... the stuff that translates statements in Verilog or VHDL into pure logic statements for small LUTs in FPGAs or logical NAND gates of hardware synthesis??

Oh yeah, machines are way better than humans. People pretty much rely upon automatic synthesis for circuit design and boolean logic these days. Proof is in the pudding.

Perhaps it isn't the same kind of math you were thinking about. But Boolean algebra is still math, logic, and proofs. Of course, in practice, humans use these tools to build larger structures... but I'd argue that the machine handles a lot of the rote proof stuff (optimally figuring out the minimum number of NAND gates to represent a certain truth table).