I’m fascinated with this visual proof assistant (although, not quite as powerful yet as Coq/Lean): http://incredible.pm/