See also: https://coq.inria.fr/

I'm excited about learned search heuristics in theorem space.