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