如果大型数学模型有效（到目前为止似乎是这样），那么会很奇怪，许多以前未解决的定理被证明，而可能没有任何人能够阅读模型-Lean-ese 证明，实际上知道这些证明是如何工作的。

这已经有点像这样工作了。

@_joshd 如果摘要模型也能生成与原始内容类型相同的精简证明，这可能会有效。