Olivetti Club

Luke Serafin
A formally verified proof of the Central Limit Theorem

Tuesday, October 8, 2019 - 4:30pm
Malott 406

The central limit theorem has been known in some form for more than two hundred years, and its precise statement and proof were an early triumph of measure-theoretic foundations for the theory of probability. But could there be a mistake in the proof? Might the theorem even be wrong? The fact that no errors which can't be corrected have been discovered in more than a century, and a highly intricate and coherent collection of results derived from the central limit theorem has arisen without encountering contradiction provides strong empirical evidence that the mathematical community has a correct proof, and hence the theorem is true, but can we do better than empirical evidence?

In the latter half of the 19th century Boole and Frege and others made precise what is meant by a "proof," and by their definition a proof is necessarily correct. However, precise definitions of proofs require working with formal languages and rules which are quite ungainly for a mathematician working intuitively, and so translating an informal, natural-language proof of a significant mathematical result requires such enormous effort that it has rarely been carried out by hand in complete detail. Hence mathematicians find themselves in the awkward position of knowing with mathematical precision what a proof ought to be, but for practical purposes unable to provide truly precise proofs, instead settling for informal arguments that a truly precise proof ought to exist.

In the latter half of the 20th century the development of electronic computers provided a way to overcome this impasse, for electronic computers can carry out low-level formalization of mathematical arguments much faster than humans. This led to automated theorem provers, which take as input a statement written in a suitable formal language and search for a formal proof of that statement. Automated theorem provers are powerful for formalizing proofs of simple results, but don't have access to known proof strategies for a given theorem which may have been developed, and so unsurprisingly often fail to produce a proof of a nontrivial result in a reasonable amount of time. Hence interactive theorem proving, which puts a human and a computer in collaboration with the human providing high-level proof strategies and the computer filling in low-level details, has become the standard method of providing formal proofs of complex mathematics. In this talk we describe automated and interactive theorem proving and its applications to and potential for formalizing mathematics using a formal proof of the central limit theorem produced using the interactive proof assistant Isabelle as a motivating example.

Refreshments will be served in the lounge at 4:00 PM.