Chinese AI Model Used to Help Prove 3D Ghys Conjecture

The significance here is less the conjecture itself than the workflow: a domain-specific scientific model proposing a proof, with a separate formal-verification framework confirming it. That division of labor — generation on one side, machine-checkable validation on the other — is what makes AI output usable in mathematics rather than merely suggestive. It also signals that Chinese labs are building vertically integrated stacks, model plus verification, rather than competing only on general-purpose capabilities. Whether this collaboration pattern generalizes beyond a single open problem, and whether formal verification becomes the default gate for AI-assisted proof, is the open question worth tracking.