Zulip Chat Archive

Stream: general

Topic: Graphical tactic state visualization

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: Aug 03 2023 at 10:10 UTC