Paperproof：为每个 Lean 定理生成可视化证明图

Paperproof 是一款免费开源的 Lean 4 VSCode 扩展，把 Lean 证明从一串 tactic 列表转成数学家纸笔草图式的完整证明图。它用三种方框表示假设、目标和 tactic，颜色区分事实类型、位置显示来源，随输入实时渲染。安装扩展后打开任意 .lean 文件即可在面板中查看证明结构。