ATP ITP 之间 PL Jul 03, 2024 Jeremy Avigad 有给过一个很personal的talk https://github.com/avigad/arwm Leo De Moura 17 年的 talk SledgeHammer, CoqHammer, LeanAuto F* 在其中究竟算啥? Lean早期其实是想做 F* 的customized solver [出处] PREVIOUSStagingNEXTAlgebraic Effects