Last year, I set out on a journey to automatically prove some properties about floating-point computations in a whole host of different proof assistants. Eventually, I ended up writing Schmitty, which integrates Agda with SMT-LIB. In this talk, I’ll give an overview of the problems you’ll face integrating your favourite proof assistant with an external solver, and how different proof assistants chose to resolve – or not resolve – them.