ATP ITP 之间

Jeremy Avigad 有给过一个很personal的talk https://github.com/avigad/arwm

Leo De Moura 17 年的 talk

SledgeHammer, CoqHammer, LeanAuto

F* 在其中究竟算啥？

Lean早期其实是想做 F* 的customized solver [出处]