Eric Wieser (Oct 24 2020 at 06:48):
This looked quite interesting - it would be cool if a lean tactic state could be translated automatically into an input for it: https://penrose.ink/siggraph20.html
Bryan Gin-ge Chen (Oct 24 2020 at 07:18):
I heard about this a few years ago; it's nice to see that they've released a longer paper! Even though their page says it's not ready, they do have quite a bit of code and documentation in their repo.
Off-topic: these talk slides "Proof assistants as a tool for thought" by the lead author, Katherine Ye, might also be of interest to folks here.
Johan Commelin (Oct 24 2020 at 07:37):
That looks really nice! Thanks for the pointers!
Johan Commelin (Oct 24 2020 at 08:09):
@Bryan Gin-ge Chen also thanks for the link to those slides. I like them
Last updated: May 15 2021 at 22:14 UTC