Led by Great Bay University professor Xu Disheng, the researchers worked with Shanghai Artificial Intelligence Laboratory’s Shusheng-S2 model. Across seven rounds of reasoning, the model explored multiple routes and generated detailed arguments. Researchers identified promising ideas, rejected dead ends and guided the next round of exploration.

A separate Peking University team translated the paper’s four main theorems into computer-checkable form. The proofs passed Lean, a system that checks mathematical reasoning step by step. Experts also confirmed that the formal statements matched those in the paper.

The research has been posted as a preprint on arXiv, and the verification code is publicly available, allowing others to examine the work.