 Various so called proof hammers, in the spirit of Isabelle’s Sledgehammer tool, have recently been developed and integrated with modern proof assistants. Prominent examples include HOL(y)Hammer (Kaliszyk &amp; Urban 2015) for HOL Light and a similar hammer (Czaika &amp; Kaliszyk 2018) for the proof assistant Coq. 