大模型驱动的形式化定理证明:综述与展望

胡俊杰, 陈宇杰, 胡义坤, 文成, 曹嘉伦, 马智, 苏杰, 孙纬地, 田聪, 秦胜潮

Formal Theorem Proving Empowered by Large Language Model:Survey and Perspectives

HU Junjie, CHEN Yujie, HU Yikun, WEN Cheng, CAO Jialun, MA Zhi, SU Jie, SUN Weidi, TIAN Cong, QIN Shengchao

计算机科学 . 2026, (4): 1 -23 . DOI: 10.11896/jsjkx.251000067