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).
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).