BriefGPT.xyz
Sep, 2023
FIMO：用于自动定理证明的挑战性形式化数据集
FIMO: A Challenge Formal Dataset for Automated Theorem Proving
HTML
PDF
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan...
TL;DR
FIMO是一个数据集，包括了国际数学奥林匹克竞赛的正式数学问题陈述，旨在促进IMO水平的高级自动定理证明。初始实验证明了目前方法的局限性，表明在实现令人满意的IMO水平自动定理证明结果之前还有很长的路要走。
Abstract
We present
fimo
, an innovative
dataset
comprising
formal mathematical problem statements
sourced from the
→