[deadbeef57]

In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice.

The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.

[chriswarbo]

One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting).

(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)

Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.

[ganzuul]

Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.