paperproof-validator - Lean 4 形式化证明的可视化与验证
将形式化的 Lean 4 证明转换为直观的纸质化可视化
标签
更新于: 2026-02-11能力
典型输入
典型输出
该技能可以做什么
- 可视化证明结构
- 提取证明元数据
- 验证证明正确性
- 分析策略效果
- 支持多种证明策略
- 导出证明可视化
输入
- Lean 4 定理
- Lean 4 InfoTree
- VS Code 光标位置
输出
- 可视化证明树
- 证明元数据 JSON
- HTML 可视化
- 证明验证结果
要求
- Lean 4 环境
- VS Code 扩展
- Paperproof 库