希望兔头支持更丰富的形式化证明功能

[azhzx]

如题

现在的形式化证明用途有些局限