Colloquium
Alexey Solovyev
University of Pittsburgh
Monday August 12, 2013
3147 MEB
Lecture 2:00 p.m.
Title: Formal Computations and Methods
Alexey Solovyev
University of Pittsburgh
Monday August 12, 2013
3147 MEB
Lecture 2:00 p.m.
Title: Formal Computations and Methods
Abstract
In my talk, I will present applications of formal methods to mathematical proofs. I will briefly describe the ongoing project on the formal proof of the Kepler conjecture (the Flyspeck project by T. Hales) and my work on a formalization of the computational part of this project. In particular, I will cover formal verification methods and procedures for proving bounds of linear programs and multivariate nonlinear inequalities. Also, I will describe an efficient implementation of interval arithmetic in HOL Light proof assistant.
Return to 2013 Events Calendar
In my talk, I will present applications of formal methods to mathematical proofs. I will briefly describe the ongoing project on the formal proof of the Kepler conjecture (the Flyspeck project by T. Hales) and my work on a formalization of the computational part of this project. In particular, I will cover formal verification methods and procedures for proving bounds of linear programs and multivariate nonlinear inequalities. Also, I will describe an efficient implementation of interval arithmetic in HOL Light proof assistant.
Return to 2013 Events Calendar