For proofs I've been finding the leap into dependent-type theory to be very productive as many provers in this realm also double as practical programming languages allowing the possibility of shipping proof-carrying code.

My two favorites in this area are Lean [0] and Agda [1], the latter of which recently received a nice introductory text from Phil Wadler and Wen Kokke [2].

[0] https://leanprover.github.io/ [1] https://wiki.portal.chalmers.se/agda/pmwiki.php [2] https://plfa.github.io/