论文标题
定理中的结构证明：分析和改善正式证明的伊莎贝尔档案
Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
论文作者
论文摘要
在过去的几年中，伊莎贝尔（Isabelle）正式证明的档案已增长到很大的规模。它弥补了令人印象深刻的研究，这可以使定理中各个方面的多种统计方法证明，并且尚未详尽利用。但是，不断增长的规模也带来了一些挑战：材料变得越来越难以找到，可重复使用和易于理解变得更加重要。本文摘要总结了我对这些主题的研究计划，并简要介绍了初步结果，这表明存档的依赖关系图的节点在无标度的分布遵循。
The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet been utilized exhaustively. However, the growing size also poses some challenges to address: Material becomes increasingly harder to find, reusability and ease of understanding become more important. This thesis abstract summarizes my research plans on those topics and briefly touches on preliminary results, which indicate that the node in-degree of the dependency graph of the archive follows a scale-free distribution.
