Graphical tactic state visualization

Stream: general

[Eric Wieser]

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]

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]

That looks really nice! Thanks for the pointers!

[Johan Commelin]

@Bryan Gin-ge Chen also thanks for the link to those slides. I like them