近日，在2025年CCF中国软件大会期间举办的首届定理证明竞赛中，深圳河套学院博士研究生赵雨扬凭借出色表现，斩获一等奖第二名。

颁奖现场

赛事速览：

国内首届定理证明竞赛

本次竞赛由中国计算机学会（CCF）形式化方法专委会主办，TPChina定理证明开放社区、浙江大学与上海交通大学联合承办，旨在通过竞赛形式促进国内定理证明领域的人才培养和技术发展。

定理证明作为形式化方法的核心技术，能够将程序与系统的正确性转化为可严格推导的数学命题，可突破传统测试方法的局限，为复杂系统提供可靠验证。当前，从澳大利亚团队验证的seL4微内核到法国INRIA的CompCert可信编译器，再到美国耶鲁大学的CertiKOS多核操作系统验证，全球多项重要系统验证成果均建立在此技术基础之上。随着计算机系统在各领域的深入应用，软硬件可靠性已成为关键挑战，定理证明技术的重要性和应用前景也日益凸显。

此次竞赛为个人赛，共设置6-12道试题，涵盖基本证明、算法证明、数学证明与程序验证四大类型。选手需在规定时间内完成尽可能多的题目，组委会将依据总分评定奖项，总分相同者按提交时间决定最终名次。

竞赛现场

赵雨扬同学在比赛中展现了扎实的功底与稳定的发挥。在竞赛中的基础证明环节，只有他和另一位选手获得了满分，其他选手的平均得分不到70%。这得益于他长期参与Lean开源社区建设所积累的实践经验——自2021年起，他已为mathlib贡献了数百个Pull Request。本次成绩，是他在深圳河套学院提供的开放科研平台上，将个人兴趣与前沿探索结合的又一体现。

量身定制：

赵雨扬同学拥有着过硬的编程、数学建模推导能力和扎实的算法基础。他自高中阶段便高中曾取得国家信息学竞赛（NOI）银牌第62名，本科期间，他积极参加国际大学生程序设计竞赛（ICPC）和中国大学生程序设计竞赛（CCPC）并多次取得金牌前列的好成绩。

2025年粤港澳大湾区国际编程大赛中，赵雨扬获全场第三名

2025年，他在由香港中文大学（深圳）主办的粤港澳大湾区国际编程大赛中脱颖而出，荣获所在组季军，并由此获得了深圳河套学院和香港中文大学（深圳）的博士入学资格。

陈靖邦教授与赵雨扬的合影

在深圳河套学院，赵雨扬同学获得了罗智泉教授与陈靖邦教授的共同指导。

陈靖邦教授作为赵雨扬同学的导师，对其表现给予了高度评价：“赵雨扬同学在定理证明领域有长期的热情和积累。学院为他这样的学生提供了将兴趣转化为深度研究的平台。很高兴看到他在完成系统科研训练的同时，能在专业竞赛中取得佳绩。期待他在人工智能与形式化方法的交叉领域继续探索，产出有影响力的成果。”

智启湾区拓新径

深圳河套学院作为立足粤港澳大湾区核心区的人工智能拔尖创新人才培养试验区，其核心理念正是为每一位具有特殊潜质的学生提供量身定制的成长路径。在这里，学院通过灵活而富有挑战性的培养方案，为那些在特定领域展现非凡才华的人才破除传统束缚，打造自由探索的科研舞台。

学院不只提供顶尖的科研资源与国际化平台，更构建了鼓励创新、包容多元的学术生态，通过深港联动、产学融合的独特优势，为不同类型的人才提供最适宜的发展土壤。

未来，深圳河套学院将持续继续通过编程大赛、联合培养等多元方式，拓宽人才选拔与培养的路径，吸引并培育更多心怀梦想、能力突出的青年学子，在人工智能的时代浪潮中书写属于自己的卓越篇章。