Formal proofs and global optimisation are two research areas that have been heavily influenced by the arrival of computers. This article aims to bring both further together by formalising a global optimisation method based on Taylor models: a set of functions is represented by a polynomial together with an error bound. The algorithms are implemented in the proof assistant Coq's term language, with the ultimate goal to obtain formally proven bounds for any multi-variate smooth function in an efficient way. To this end we make use of constructive real numbers, interval arithmetic, and polynomial bounding techniques.