The first Theorem Proving Competition, sponsored by CertiK and organized by the Formal Methods Committee of the China Computer Federation (CCF), officially opened on November 29. The competition invites students and researchers from universities and research institutions to take on challenges spanning logic, algorithms, mathematical theorems, and program verification. The event aims to cultivate the next generation of formal verification talent and strengthen the broader research community.

OpenMath: The World’s First Mathematical DeSci Platform

OpenMath takes center stage as a key technical supporter of the competition. Jointly developed by Shentu Chain and CertiK, OpenMath is the world’s first mathematical decentralized science (DeSci) platform. Its development draws on the strengths of both organizations: Shentu Chain, built on the Cosmos SDK, provides the underlying blockchain infrastructure, while CertiK, the world’s largest Web3 security company and a global leader in formal verification, supports the platform’s core mathematical verification technology. This collaboration advances the integration of blockchain and formal verification within mathematical research.

Through OpenMath, researchers and verifiers can collaboratively propose and solve mathematical problems, using Rocq-based formal verification technology to validate solutions with mathematical-level rigor. Participants who successfully complete verification receive token rewards, combining transparent workflows with effective incentive mechanism.

OpenMath records the research process on-chain to ensure data integrity, transparency, and traceability. Its two-phase submission mechanism also protects the intellectual property of provers while encouraging open participation from researchers worldwide.

Collaboration and Innovation in Research

OpenMath redefines how mathematical research is conducted through its collaborative workflow, verification processes, and incentive model. Researchers can submit tasks, decompose problems, and work jointly on solutions, using Rocq or Lean for formal verification. Each proof is published on-chain and made immutable, while verification results can be independently reviewed. The global community collectively contributes to determining which theorems merit further exploration.

OpenMath is emerging within a rapidly evolving DeSci landscape that aims to reshape how scientific knowledge is produced, funded, and disseminated. Unlike traditional research models that rely on centralized institutions and closed systems, DeSci leverages Web3 technologies to promote open collaboration, transparent funding, and direct incentives for contributors.

Recent Updates

To further ensure fair attribution and verifiable knowledge transfer, OpenMath has launched a theorem citation feature. Researchers can publish and prove theorems, once verified are recorded on-chain, forming an open, reusable, and composable foundation of mathematical knowledge. This reduces duplication of effort while ensuring proper credit for original authors.

Recently, OpenMath expanded support from Rocq to also include Lean. Rocq (formerly Coq) is historically established and widely used in formal verification, while Lean is a rapidly developing next-generation proof assistant with an active and growing ecosystem. The addition allows researchers to submit proofs using multiple mainstream formal languages, lowering collaboration barriers and promoting the construction and sharing of verifiable knowledge systems.

An Open, Verifiable, and Traceable Ecosystem

The OpenMath ecosystem, built around principles of community-driven governance, verifiability, citability, and traceability, provides a fair and efficient collaborative environment for mathematical researchers worldwide. Every step of the research process is recorded, ensuring that results are both independently verifiable and long-term citable. This creates a reliable foundation for the advancement of formal verification and the broader mathematical DeSci movement.

Looking ahead, OpenMath will continue enhancing its support and collaboration mechanisms, building a more open and interoperable DeSci infrastructure for mathematics. The platform aims to foster knowledge sharing and innovation, providing strong support for developing formal verification talent and expanding the trusted computing ecosystem.

Learn more about OpenMath here.

Learn more about the Theorem Proving Competition here.