I am happy to announce an online seminar series "Every proof assistant" about proof assistants. The first semianr will be given by Valery Isaev about the Arend proof assistant. For further information see math.andrej.com/2020/04/28/eve
4
49
132
Conversation
This Tweet is from a suspended account. Learn more
I will let you push the boundaries by inviting you to present a proof assistant of your own. Even if it's just an Emacs mode. Actually, I would be delighted if you presented a proof assistant implemented as an Emacs mode.
1
3
This Tweet is from a suspended account. Learn more
I would absolutely love a seminar on Epigram 2, and I mean that seriously. I don't care if it doesn't exist.
1
This Tweet is from a suspended account. Learn more
I have enjoyed looking through some of the tests on this archived version in the past github.com/mietek/epigram - would be very interested to know some of the ideas you had been thinking about, even if you never got around to finish working on them!