Chinese AI framework solved a 10-year-old math problem by Dan Anderson in 80 hours.
System uses two AIs: one for natural language reasoning, one for formal proof verification.
AI approach automates mathematical research, reducing human effort while ensuring proof accuracy.