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