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...

Descripción completa

Detalles Bibliográficos
Publicado en:	Communications of the ACM Vol. 57; no. 4; pp. 66 - 76
Autores principales:	AVIGAD, JERMEY, HARRISON, JOHN
Formato:	Artículo
Publicado:	Association for Computing Machinery Apr2014
Materias:	Technology Technological progress Mechanizing Proof: Computing, Risk & Trust (Book) Jordan curves Prime number theorem MacKenzie, Donald Computer software Computer input-output equipment Mathematics theorems
Acceso en línea:	Ver este registro en EBSCOhost

Descripción
Sumario:	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.