Title: Parameter space analysis and automatic theorem proving in SageMath

Abstract: A metaprogramming trick transforms algebraic programs for testing a property for a given input parameter into programs that compute semialgebraic descriptions of the input parameters for which the property holds. Our implementation of this trick is for the Python-based computer algebra system SageMath. We borrow techniques from global optimization for simplification of semialgebraic sets. We investigate practical representations of proof cells and efficient strategies that lead to shorter proofs. We illustrate it with an application to the theory of integer linear optimization, the automatic discovery and proof of certain cutting plane theorems in integer programming.