未明确提及

本项目旨在积累和开发用于半自动化翻译非正式与正式数学文本的数据集，以支持统计机器翻译方法。数据集主要来源于HOL Light、Mizar/MML库以及ProofWiki和PlanetMath等资源，涵盖了数学理论的正式与非正式表述。创建过程中，通过自动化工具和人工标注相结合的方式，对文本进行对齐和注释，以提高数据集的质量和可用性。该数据集的应用领域主要集中在数学文本的自动翻译和理解，旨在解决数学知识在计算机处理中的语义化问题，提高数学理论的自动化处理能力。

This project aims to collect and develop a dataset for semi-automated translation between informal and formal mathematical texts, to support statistical machine translation methods. The dataset is primarily sourced from resources including the HOL Light, Mizar/MML libraries, ProofWiki and PlanetMath, covering both formal and informal representations of mathematical theories. During the dataset construction, texts are aligned and annotated via a combination of automated tools and manual annotation to enhance the dataset's quality and usability. The main application domains of this dataset focus on automatic translation and understanding of mathematical texts, aiming to resolve the semanticization issue of mathematical knowledge during computer processing and improve the automated processing capabilities of mathematical theories.