Formally Verified Mathematics.

The article presents information on the current technology and its motivations, some recent advances and the prospects for the future. It set aside hardware and software verification deliberately and refers to Donald MacKenzie's book "Mechanizing Proof: Computing, Risk and Trust16." It is stated tha...

Full description

Bibliographic Details
Published in:	Communications of the ACM Vol. 57; no. 4; pp. 66 - 76
Main Authors:	AVIGAD, JERMEY, HARRISON, JOHN
Format:	Article
Published:	Association for Computing Machinery Apr2014
Subjects:	Technology Technological progress Mechanizing Proof: Computing, Risk & Trust (Book) Jordan curves Prime number theorem MacKenzie, Donald Computer software Computer input-output equipment Mathematics theorems
Online Access:	View this record in EBSCOhost

Description
Summary:	The article presents information on the current technology and its motivations, some recent advances and the prospects for the future. It set aside hardware and software verification deliberately and refers to Donald MacKenzie's book "Mechanizing Proof: Computing, Risk and Trust16." It is stated that due to developments in computer science it is possible to achieve formalization in practice. Several important theorems have been verified including the prime number theorem, the Jordan curve theorem, and the Brouwer fixed-point theorem.