Computerized Math, Formal Proofs and Alternative Logic
March 16, 2013 3:33 PM Subscribe
Using computer systems for doing mathematical proofs - "With the proliferation of computer-assisted proofs that are all but impossible to check by hand, Hales thinks computers must become the judge."
Three years ago, Vladimir Voevodsky, one of the organizers of a new program on the foundations of mathematics at the Institute for Advanced Study in Princeton, N.J., discovered that a formal logic system that was developed by computer scientists, called "type theory" could be used to re-create the entire mathematical universe from scratch. Type theory is consistent with the mathematical axioms, but couched in the language of computers. Voevodsky believes this alternative way to formalize mathematics, which he has renamed the univalent foundations of mathematics, will streamline the process of formal theorem proving. Voevodsky and his team are adapting a program named Coq, which was designed to formally verify computer algorithms, for use in abstract mathematics.also btw, speaking of mathematical revolutions, from a historical perspective, check out The Man of Numbers: Fibonacci's Arithmetic Revolution - "Before the 13th century Europeans used Roman numerals to do arithmetic. Leonardo of Pisa, better known today as Fibonacci, is largely responsible for the adoption of the Hindu–Arabic numeral system in Europe, which revolutionized not only mathematics but commerce and trade as well. How did the system spread from the Arab world to Europe, and what would our lives be without it?"
This thread has been archived and is closed to new comments