SIAM News Blog

2018 I. E. Block Community Lecture: How Paradoxes Shape Mathematics and Give Us Self-Verifying Computer Programs

The I. E. Block Community Lecture is given each year at the SIAM Annual Meeting and is free and open to the public. Students, teachers, professionals, and all other members of the local community (Portland, OR this year!) are encouraged to attend. The lecture highlights a relatable application of mathematics to help foster appreciation and excitement for the vitality of science.

I. E. Block Community Lecture: How Paradoxes Shape Mathematics and Give Us Self-Verifying Computer Programs

Wednesday, July 11, 6:15 PM - 7:15 PM
Oregon Convention Center
Room: Oregon Ballroom 202/203
Chair: Nicholas J. Higham, University of Manchester, United Kingdom

Dr. Thomas Hales of the University of Pittsburgh will present the 2018 I. E. Block Community Lecture entitled "How Paradoxes Shape Mathematics and Give Us Self-Verifying Computer Programs." 

A paradox is a seeming contradiction.  The liar's paradox is one of the best known:  "This statement is false."  If the statement is true, then it is false; if it is false, then it is true.

Paradoxes can be so amusing that we might think that paradoxes are nothing more than a game.  However, paradoxes triggered a crisis in math a century ago when a paradox similar to the barber paradox was found: "A barber named Bertie shaves exactly those who do not shave themselves."  Does Bertie shave himself?  If he does, then he doesn't; if he doesn't, then he does.

Other clever paradoxes show us the disturbing limits of computation and mathematics.  These results are mathematical bombshells.

Today, we design computer programs that check that other computer programs have no bugs.  Can computer programs be fed into themselves to check their own correctness?  Or does paradox stop us in our tracks?  And can we know that beneficial artificial intelligence will not turn evil when it starts to modify its own computer code?

Dr. Hales is the Andrew Mellon Professor of Mathematics at the University of Pittsburgh, where he works in formal verification, representation theory, and discrete geometry. He proved the centuries-old Kepler Conjecture in 1998, and went on to confirm the Honeycomb Conjecture the following year. His Kepler Conjecture proof relied significantly on extensive computer calculations, which led him to investigate to what degree computers may be used to prove other difficult theorems.

For more information, and to view the full conference program, click here.

blog comments powered by Disqus