Skip to content

Back to Departmental Colloquium: Fall 2021

Departmental Colloquium


Date: Thursday, Nov 11, 2021

Time: 4:00PM

Location: JWB 335


Thomas Hales

University of Pittsburgh

Title

Formal Proof

Abstract

A formally verified proof is a proof that has been checked by software to be free of errors. The software is based on the foundational axioms and rules of logic of mathematics. This talk will give a survey of this field of research, including some of the recent theorems that have been formally verified (such as the Kepler conjecture about sphere packings and the Continuum Hypothesis). I will describe some recent advances in the technology aimed at bringing these tools to a larger mathematical audience.

Number Theory Commutative Algebra

Calendar file