Until theorem proving is as easy in a programming language as it is in plain old math (last I checked, dependently typed languages were still verbose and cumber

Until theorem proving is as easy in a programming language as it is in plain old math (last I checked, dependently typed languages were still verbose and cumbersome for this purpose), then Yes, math will still be special because it is the proofs that make it special (also, not all proofs use deductive logic).