由中国计算机学会(CCF)形式化方法专委会主办的首届“定理证明竞赛”，将于11月29日正式开幕。CertiK作为赛事独家赞助方，为推动形式化验证人才培养和科研生态建设提供技术支持。

　　CCF中国软件大会是中国计算机学会主办的软件领域年度盛会，是国内软件科学与工程领域参会人数多、影响范围广、内容全面的核心交流平台。此次定理证明竞赛是2025届CCF中国软件大会的专题竞赛，聚焦形式化方法核心技术，旨在为我国软硬件系统安全保障方面的发展积聚年轻的力量。

　　OpenMath将作为重要技术支持，亮相赛事现场。OpenMath是全球首个聚焦数学领域的去中心化科学(DeSci)平台，由CertiK与Shentu链联合研发。平台建设依托双方在各自领域的专业优势：CertiK作为全球最大的Web3安全公司、形式化验证的国际领军者，为平台提供数学验证核心技术;Shentu链基于Cosmos SDK构建，为OpenMath提供底层链上基础设施。这一合作实现了区块链技术与形式化验证在数学研究场景中的融合与应用。

　　通过OpenMath，研究者和验证者可协作提出并解决数学问题，并借助基于Rocq的形式化验证技术对解答进行逻辑验证，以数学级精度确保推理的严谨与准确。成功完成验证的参与者可获得代币奖励，实现研究过程的公开透明与激励机制的有效结合。

　　OpenMath将研究过程以数据形式记录在区块链上，确保信息不可篡改，使整个过程公开透明，打破机构壁垒，保障每项研究成果可追溯。平台采用“双阶段提交机制”，在保护验证者知识产权的前提下向全球研究者开放参与权限，同时支持零知识证明，研究者可在保持内容隐私的前提下完成链上验证。

　　功能升级，OpenMath再添两大亮点

　　为进一步完善数学知识的公平溯源与协作共享，OpenMath近期迎来重要功能更新：

　　1. 定理引用功能上线，构建可复用知识体系

　　新增的定理引用功能，支持研究者发布并证明定理，经验证后上链，形成开放、可复用、可组合的数学知识基础设施，既能降低重复计算成本，又能保障原作者收益。

　　2. 新增Lean证明器支持，降低协作门槛

　　在原有Rocq的基础上，OpenMath新增对Lean的支持。Rocq(原Coq)历史悠久、严谨性广受认可，已被广泛应用于形式化验证;Lean作为新一代证明器，发展势头迅猛且生态高度活跃。这一功能扩展让研究者可根据自身研究习惯，选择多种主流形式化语言提交证明，降低协作门槛，进一步推动可验证知识体系的建设与共享。

　　构建开放、可验证、可追溯的数学生态

　　OpenMath的生态体系以“社区主导、可验证、可引用、可追溯”为核心，为全球数学研究者提供公平、高效的协作平台。每一步研究过程都被记录在区块链上，确保成果既可验证，又可长期引用，为形式化验证和数学DeSci的发展提供可靠基础。

　　未来，OpenMath将持续完善多语言支持和协作机制，打造更加开放、兼容的DeSci数学基础设施;CertiK也将继续深耕形式化验证核心技术，共同为形式化验证人才培养与可信计算生态建设提供支持。