CertiK贊助CCF定理證明競賽，助力培養形式化驗證人才

　　由中國計算機學會(CCF)形式化方法專委會主辦的首屆“定理證明競賽”，将于11月29日正式開幕。CertiK作為賽事獨家贊助方，為推動形式化驗證人才培養和科研生态建設提供技術支持。

CCF中國軟件大會是中國計算機學會主辦的軟件領域年度盛會，是國内軟件科學與工程領域參會人數多、影響範圍廣、内容全面的核心交流平台。此次定理證明競賽是2025屆CCF中國軟件大會的專題競賽，聚焦形式化方法核心技術，旨在為我國軟硬件系統安全保障方面的發展積聚年輕的力量。OpenMath：全球首個數學DeSci平台

　　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也将繼續深耕形式化驗證核心技術，共同為形式化驗證人才培養與可信計算生态建設提供支持。