theory Scratch
  imports Main
begin

lemma fits_in_margin: \<open>a^n + b^n \<noteq> c^n\<close> if \<open>n > 2\<close> and \<open>a \<ge> 1\<close> and \<open>b \<ge> 1\<close> for a b c :: nat
  sledgehammer (* Doesn't succeed *)
  sorry

lemma True (* This one is not even parsed (stays with orange background) *)