Putnam-2025-b3 证明树
b3
b3-0
b3-1
b3-0-0
b3-0-1
b3-0-2
b3-0-3
b3-0-4
b3-0-4-0
b3-0-4-1
b3-0-4-2
b3-0-4-3
b3-0-4-4
b3-0-4-5
b3-0-4-6
b3-0-4-7
b3-0-4-1-0
b3-0-4-1-0-0
b3-0-4-1-0-1
b3-0-4-1-0-1-0
b3-0-4-1-1
b3-0-4-1-2
b3-0-4-1-2-0
b3-0-4-1-2-0-0
b3-0-4-2-0
b3-0-4-2-1
b3-0-4-2-2
b3-0-4-2-2-0
b3-0-4-2-2-1
b3-0-4-2-3
b3-0-4-2-3-0
b3-0-4-2-4
交互说明
- 单击节点：为该节点添加视觉高亮，便于对比和定位。
- 双击节点：在右侧侧栏打开该节点的完整 Lean 证明。
- 关闭侧栏：按 Esc 键或点击侧栏外部即可关闭。
证明解释
- Prover首先会尝试直接证明定理。
- 当证明存在问题时，Sorrifier会将错误的证明块用“sorry”占位。
- 每个占位块会被提取成为一个子定理，即证明树上的一个子节点。
- Prover会递归地尝试证明这些子定理，当一个定理的所有子定理都被证明时，该定理也被证明，通过将“sorry”替换为“apply?”来完成 Lean 编译