Abstract
Linear programming is a basic mathematical technique for optimizing a
linear function on a domain that is constrained by linear inequalities.
We restrict ourselves to linear programs on bounded domains that involve only
real variables. In the context of theorem proving, this restriction makes it
possible for any given linear program to obtain certificates from external
linear programming tools that help to prove arbitrarily precise bounds for the
given linear program. To this end, an explicit formalization of matrices
in Isabelle/HOL is presented, and how the concept of latticeordered rings
allows for a smooth integration of matrices with the axiomatic type classes of
Isabelle.
As our work is a contribution to the Flyspeck project, we demonstrate that via
reflection and with the above techniques it is now possible to prove bounds
for the linear programs arising in the proof of the Kepler conjecture
sufficiently fast.
BibTeX  Entry
@InProceedings{obua:DSP:2006:435,
author = {Steven Obua},
title = {Proving Bounds for Real Linear Programs in Isabelle/HOL},
booktitle = {Mathematics, Algorithms, Proofs},
year = {2006},
editor = {Thierry Coquand and Henri Lombardi and MarieFran{\c{c}}oise Roy},
number = {05021},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/435},
annote = {Keywords: Certified proofs, Kepler conjecture}
}
Keywords: 

Certified proofs, Kepler conjecture 
Seminar: 

05021  Mathematics, Algorithms, Proofs 
Issue Date: 

2006 
Date of publication: 

17.01.2006 