Lean, Coq and other proof assistants | 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...

Powered by BroadcastChannel & Sepia