Lean-GAP

数据集将研究生代数问题形式化以供AI验证

研究人员开发了Lean-GAP，一个包含430个形式化研究生代数问题的数据集，这些问题源自Dummit和Foote的著作《抽象代数》。该过程涉及一个用于PDF到LaTeX预处理和自动形式化为Lean 4的流水线，但人工监督对验证至关重要。这项工作贡献了一个结构化数据集、一种形式化数学文本的方法，以及对将非正式陈述转化为正式语言的挑战的分析，包括对自动形式化模型的比较。