We discuss the topic of unsatisfiability proofs in SMT, particularly with\nreference to quantifier free non-linear real arithmetic. We outline how the\nmethods here do not admit trivial proofs and how past formalisation attempts\nare not sufficient. We note that the new breed of local search based algorithms\nfor this domain may offer an easier path forward.\n