While mathematics "can" be reasoned about from first principles, the history of math is chock-full of examples of professional mathematicians convinced by unsound and wrong arguments. I prefer the clarity of performing math experiments and validating proofs on a computer.
Yes, but a C or Python program that “implements” a proof and which you test by running it on a few inputs is very different from a program in a interactive theorem prover like Rocq or Lean. In the latter, validity is essentially decided by type-checking, not execution
