Recently, at the inaugural Theorem Proving Competition held during the 2025 CCF China Software Conference, PhD student Yuyang Zhao from the Shenzhen Loop Area Institute delivered an outstanding performance, securing first place and second prize overall.

(Image: Award Ceremony)

Competition at a Glance:

China's Inaugural Theorem Proving Contest

Organized by the Formal Methods Technical Committee of the China Computer Federation (CCF) and co-hosted by the TPChina Theorem Proving Open Community, Zhejiang University, and Shanghai Jiao Tong University, the competition aimed to promote talent cultivation and technological development in the field of theorem proving within China.

As a core technology of formal methods, theorem proving transforms the correctness of programs and systems into rigorously derivable mathematical propositions. It can overcome the limitations of traditional testing methods, providing reliable verification for complex systems. Major global system verification achievements, from the seL4 microkernel verified by an Australian team, to the CompCert certified compiler from France's INRIA, and the CertiKOS multicore OS verification from Yale University in the US, are all built upon this foundational technology. As computer systems become more deeply embedded across various fields, the reliability of software and hardware has become a critical challenge, increasingly highlighting the importance and application prospects of theorem proving.

This individual competition featured 6 to 12 problems covering four main types: basic proofs, algorithm proofs, mathematical proofs, and program verification. Participants had to solve as many problems as possible within the time limit. The organizing committee awarded prizes based on total scores, with ties broken by submission time.

Contest Site

Yuyang Zhao demonstrated solid expertise and steady performance throughout the contest. In the basic proof section, only he and one other contestant achieved a perfect score, while the average score for other participants was below 70%. This success is attributed to the practical experience he gained from long-term involvement in the Lean open-source community—since 2021, he has contributed hundreds of pull requests to mathlib. This achievement is another reflection of how he combines personal interest with frontier exploration on the open research platform provided by the Shenzhen Loop Area Institute.

Tailor-Made Support:

Providing a Breakthrough Stage for Talent

Yuyang Zhao possesses exceptional programming skills, mathematical modeling and deduction capabilities, and a solid foundation in algorithms. In high school, he won a silver medal (62nd place) in the National Olympiad in Informatics (NOI). During his undergraduate studies, he actively participated in the International Collegiate Programming Contest (ICPC) and the China Collegiate Programming Contest (CCPC), achieving top gold medal results multiple times.

Yuyang Zhao placed 3rd overall in the 2025 Greater Bay Area International Programming Contest

In 2025, he stood out at the Guangdong-Hong Kong-Macao Greater Bay Area International Programming Contest hosted by CUHK-Shenzhen, winning third place in his group. This achievement subsequently earned him a PhD admission offer from both the Shenzhen Loop Area Institute and CUHK-Shenzhen.

Professor Jingbang Chen with Yuyang Zhao

At the Shenzhen Loop Area Institute, Yuyang Zhao receives co-supervision from Professor Zhiquan Luo and Professor Jingbang Chen.

Professor Chen, his primary supervisor, offered high praise for his performance: Yuyang Zhao has long-held passion and accumulated expertise in theorem proving. The Institute provides a platform for students like him to transform their interests into deep research. It is gratifying to see him achieve excellent results in a professional competition while completing systematic research training. We look forward to his continued exploration at the intersection of artificial intelligence and formal methods, yielding impactful outcomes.

Inspiring the Bay Area, Forging New Paths,

Nurturing Excellence Through Personalized Education

As a pilot zone for cultivating top innovative AI talent located in the core area of the Guangdong-Hong Kong-Macao Greater Bay Area, the Shenzhen Loop Area Institute operates on a core philosophy: providing a tailor-made growth path for every student with special potential. Here, through flexible and challenging training programs, the Institute removes traditional constraints for those who demonstrate extraordinary talent in specific fields, creating a stage for free exploration in research.

The Institute provides not only top-tier research resources and an international platform but also fosters an academic ecosystem that encourages innovation and embraces diversity. Leveraging its unique advantages of Shenzhen-Hong Kong synergy and industry-academia integration, it offers the most suitable developmental ground for various types of talent.

Looking ahead, the Shenzhen Loop Area Institute will continue to broaden the pathways for talent selection and cultivation through diverse means such as programming contests and joint training programs. It aims to attract and nurture more ambitious and outstanding young students, empowering them to write their own exceptional chapters in the era of artificial intelligence.