The second online preliminary of the human–AI collaboration track (AI-assisted track) of the second theorem proving competition took place on October 10, 2026, from 19:00 to 21:00. 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 second preliminary
The contest featured five problems. Across the two platform tracks, 26 participants submitted solutions, and 12 solved all five problems.
Just 2 minutes and 25 seconds into the contest, fyrsta made the first successful submission, solving Problem A at 19:02:25 using CStar. At the half-hour mark, one participant had solved four problems and four participants had solved three. At 19:32:33, mongo, using QCP, became the first participant to solve all five problems, completing the set in 32 minutes and 33 seconds.
Ranked by their final successful submission times across both tracks, the top five were mongo, guodk, caoyichuan, tsuki, and look. All five completed every problem. Congratulations to the participants!
The problems are available on the QCP contest page for the second online preliminary.
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.
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.
See you at the final in Tianjin
Both online preliminaries of the human–AI collaboration track have now concluded. The in-person final will take place on the morning of November 8 at ChinaSoft in Tianjin. Prizes will be awarded to top-ranked participants in both the online preliminaries and the in-person final.
We invite you to keep practicing on the QCP online verification platform and the CStar online judge to prepare for the final. We look forward to meeting you in Tianjin!