3 ms·True, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)by chriswarbo 5y agoTrue, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)