An AI System Has Autonomously Solved an Open Conjecture in Pure Mathematics

For what appears to be the first time, an AI system has independently solved a long-standing open conjecture in pure mathematics, producing a formal proof verified in the Lean theorem prover.