2026 年 9 月 20 日 19:00–21:00，第二届定理证明竞赛人与 AI 协作赛道（AI 辅助赛道）第一场线上初赛举行。第二场线上初赛将于 10 月 10 日 19:00–21:00 举行，欢迎大家报名参加！ 本赛道允许选手使用 QCP 和 CStar 程序验证工具，在 AI 的辅助下完成程序验证问题。两个工具的在线评测网站——QCP 在线验证平台和 CStar 在线评测平台——已开放试用，方便参赛者熟悉工具与提交过程。
首场初赛结果
本场比赛设置了 5 道题目。两个赛道共有 29 人提交，其中 10 人通过全部题目。综合两个赛道的最终通过时间，本场初赛前五名依次为 沧海梦、look、guodk、cyy、pineapple，五位选手均通过了全部 5 道题目。祝贺各位选手！
本场比赛的题目可以在 QCP 赛事页面和 CStar 赛事页面中查看。
相约天津：第二届定理证明竞赛
去年，第一届定理证明竞赛在 ChinaSoft 大会上举办，具体赛制可参阅首届竞赛官方主页。今年，第二届定理证明竞赛将在天津的 ChinaSoft 大会现场举行，欢迎大家报名参加！
今年的竞赛分为两个赛道：
无 AI 赛道：11 月 7 日下午
无 AI 赛道沿用首届竞赛的模式，由选手个人参赛，自备计算机，在现场公布试题后，于规定时间内完成证明。试题涵盖基本证明、算法证明、数学证明和程序验证四大类，按难度赋予不同分值；首届竞赛的题量设置为 6–12 道。
选手可以使用 Rocq（Coq）、Isabelle/HOL 或 Lean 完成证明。比赛允许查阅本地、离线的文档和手册，不允许联网搜索，全程禁止使用 AI 工具。排名首先比较总得分，得分越高越靠前；总分相同时，依据提交时间确定名次。
人与 AI 协作赛道：11 月 8 日上午
参赛者可以在定理证明过程中自行选择使用 AI 工具辅助，借助 QCP 或 CStar 完成程序验证类的定理证明问题。本赛道设置两场线上初赛和大会现场的线下决赛，按完成题数与提交时间排名，初赛成绩将按下文规则折算后带入决赛。
有意参赛的爱好者可通过报名问卷报名，也欢迎扫描下方二维码加入赛事交流群，了解比赛安排、交流备赛经验。
本二维码有效期至 9 月 27 日前，请留意更新。
人与 AI 协作赛道计分规则
人与 AI 协作赛道线上初赛首先按完成的程序验证问题数量排名，完成题数越多，排名越靠前；完成题数相同时，则比较最后一次成功提交的时间，越早完成的选手排名越靠前。
按照赛事安排，两场线上初赛的成绩将折算后带入线下决赛。决赛同样优先比较完成题数；题数相同时，比较以下数值，数值越小，排名越靠前：
决赛最后一次成功提交距开赛的分钟数 + 初赛排名 ÷ 2。
其中，“初赛排名”取两次初赛中较好的一次，未参加初赛或名次低于第 40 名的，按第 40 名计算。例如，某选手两次初赛分别位列第 8 名和第 19 名，在决赛开赛后 85 分钟完成最后一次成功提交，则用于同题数比较的数值为 85 + 8 ÷ 2 = 89。具体规则以 ChinaSoft 官方网站及赛事群置顶通知为准。
第二场初赛将于 10 月 10 日举行
人与 AI 协作赛道第二场线上初赛定于 10 月 10 日 19:00–21:00 举行。线上初赛与线下决赛均将为排名前列的选手颁发奖金。
欢迎大家提前使用 QCP 在线验证平台和 CStar 在线评测平台熟悉工具、练习题目，参加第二场线上初赛，并在天津的线下赛场相聚！