Hi Freek, > So Hales might have this kind of automation for doing linear > programming proofs, maybe. How would he go about that in > Mizar? Some time ago, I started writing this (it is not an answer to your question, just some suggestions): http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/ComputerAlgebraInMizar Josef