Computers Redefining Roots of Math

Not a new thing.  Proof by computer has had a number of famous examples.   Use of formal logic as part of AI has a long history.   Now easier to use programming frameworks have been established. Good, largely non technical description in Wired,   " ... The idea of doing mathematics in a program like Coq has a long history. The appeal is simple: Rather than relying on fallible human beings to check proofs, you can turn the job over to computers, which can tell whether a proof is correct with complete certainty. Despite this advantage, computer proof assistants haven’t been widely adopted in mainstream mathematics. This is partly because translating everyday math into terms a computer can understand is cumbersome and, in the eyes of many mathematicians, not worth the effort. ... "