The first online preliminary of the human–AI collaboration track (AI-assisted track) of the second theorem proving competition took place on September 20, 2026, from 19:00 to 21:00. The second online preliminary will take place on October 10, from 19:00 to 21:00. Registration is open! Participants in this track may use QCP and CStar to solve program verification problems with AI assistance. Both the QCP online verification platform and the CStar online judge are available for practice so that participants can become familiar with the tools and submission process. All times below are China Standard Time (UTC+8).
Results of the first preliminary
The contest featured five problems. Across the two platform tracks, 29 participants submitted solutions, and 10 solved all five problems. Ranked by their final successful submission times across both tracks, the top five were 沧海梦, look, guodk, cyy, and pineapple. All five completed every problem. Congratulations to the participants!
The problems are available on the QCP contest page and the CStar contest page.
Meet in Tianjin for the second theorem proving competition
The first theorem proving competition was held at ChinaSoft last year; its format is described on the official page for the inaugural competition. This year's second competition will take place in person at ChinaSoft in Tianjin. We welcome everyone interested to register!
This year's competition has two tracks:
No-AI track: afternoon of November 7
The no-AI track follows the format of the inaugural competition. Participants compete individually, bring their own computers, and complete proofs within a fixed time after the problems are announced on site. Problems cover basic proofs, algorithm proofs, mathematical proofs, and program verification, with points assigned by difficulty. The inaugural competition used a set of 6–12 problems.
Participants may use Rocq (Coq), Isabelle/HOL, or Lean. Local, offline documentation and manuals are permitted, but online searches and all AI tools are prohibited. Rankings are determined first by total score, with submission time used to break ties.
Human–AI collaboration track: morning of November 8
Participants may choose AI tools to assist their proofs and use QCP or CStar to solve program verification problems. This track consists of two online preliminaries and an in-person final at the conference. Rankings depend on the number of problems solved and submission times. Preliminary results contribute to the final ranking under the rules below.
To take part, complete the registration form. You are also welcome to scan the QR code below to join the competition discussion group for announcements and preparation tips.
This QR code was valid until September 27. Please look out for an updated code.
Scoring in the human–AI collaboration track
In each online preliminary, participants are ranked first by the number of program verification problems they complete. Ties are broken by the time of the last successful submission: earlier completion ranks higher.
The online preliminary results also contribute to the in-person final. The final likewise ranks participants first by the number of problems completed. For a tie, the following value is compared, with a lower value ranking higher:
Minutes from the start of the final to the last successful submission + preliminary rank ÷ 2.
The preliminary rank is the better of the participant's two online preliminary rankings. Participants who do not take part, or whose rank is below 40th, are assigned rank 40. For example, a participant who places 8th and 19th in the two preliminaries and finishes their final successful submission 85 minutes into the final has a tie-breaking value of 85 + 8 ÷ 2 = 89. The official ChinaSoft website and pinned announcements in the competition group take precedence for the detailed rules.
The second preliminary takes place on October 10
The second online preliminary of the human–AI collaboration track is scheduled for October 10, from 19:00 to 21:00. Prizes will be awarded to top-ranked participants in both the online preliminaries and the in-person final.
We invite you to practice on the QCP online verification platform and the CStar online judge, join the second online preliminary, and meet us at the final in Tianjin!