Lancern's Treasure Chest
11:40 · Sep 22, 2023 · Fri
Lean, Coq and other proof assistants: Visualising proofs as trees
https://lakesare.brick.do/lean-coq-isabel-and-their-proof-trees-yjnd2O2RgxwV
lakesare.brick.do
Lean/Coq/Isabel and Their Proof Trees
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 ot...
Home
Powered by
BroadcastChannel
&
Sepia