Isabel and Their Proof Trees

lakesare.brick.do

cross-posted to:
hackernews@lemmy.smeargle.fans

Lean/Coq/Isabel and Their Proof Trees

lakesare.brick.do

armchair_progamer@programming.dev to

Formal Methods@programming.dev · 2 years ago

cross-posted to:
hackernews@lemmy.smeargle.fans

This week we (me & Anton Kovsharov) published Paperproof, a Gentzen-tree-like proof interface for Lean 4. In this post I'll review proof visualisations from o...

You must log in or register to comment.

Chat