Sunday, May 31, 2015
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. ... "
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment