普林斯顿大学 发布 Ineq-Comp 数据集, 应用在 数学证明、形式验证 领域

普林斯顿大学 本次发布的数据集 Ineq-Comp, Ineq-Comp数据集是一个用于评估形式定理证明器在代数不等式中的组合推理能力的基准。它由75个种子问题组成，这些问题是使用AM-GM、Cauchy-Schwarz、Jensen不等式等基本工具解决的奥林匹克数学问题，并附有Lean 4的验证证明。从这些种子问题出发，Ineq-Comp通过简单的代数和组合变换生成更多的问题，分为两个类型的变换：Type I和Type II。此外，还包括50个来自数学竞赛和教育资源的真实世界不等式问题，以增强基准的多样性和评估合成构建之外的一般化能力。

查看Ineq-Comp

README 内容： 

关于 普林斯顿大学 , 普林斯顿大学是一所位于美国新泽西州的顶级私立研究型大学，以卓越的教学和科研实力闻名于世。

关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。