In my answer to the question about the "Hello World" of proof assistants, the code is very monochromatic:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n
 

The presentation of this code on the Coq Wikipedia page isn't much better, but at least they have used green text for the word fun:

I appreciate that this is probably a longer-term feature request which won't be easy to entertain quickly, but I do think it would be nice if eventually we can get syntax highlighting working for at least the most popular theorem provers such as Coq and Lean.