Considering the topics covered at a conference like STOC, are any algorithm or complexity researchers actively using COQ or Isabelle? If so, how are they using it in their research? I assume most people wouldn't use such tools because the proofs would be too low level. Is anybody using these proof assistants in a way that is critical to their research, as opposed to a nice supplement?

I am interested because I might start learning one of those tools and it would be fun to learn about them in the context of proofs of reductions, correctness, or run time.