Using AI to formalize mathematics may help close gaps in AI's ineffective reasoning capabilities.

Math formalization is a recent concept. Around 1666, German polymath Gottfried Wilhelm Leibniz imagined a characteristica universalis, a precise language of symbols to express math and science concepts consistently and unambiguously. With works like Principia Mathematica (1910), mathematicians standardized the logic and symbols of math. This "formalization" made research more objective and eventually enabled engineers to perform and inspect complex math with artificial intelligence.

"You could have a computer teach itself mathematics," said mathematician Alex Best, who develops artificial intelligence for formalization at the startup Harmonic. Now, he said, formalization may catapult computers' math abilities to levels once believed impossible — performing math better than humans can.

It's a lofty goal. AI struggles with technical and ethical limitations like uninterpretable methods and a lack of diverse datasets make facial recognition and medical software dangerously biased. If algorithms output answers without little explanation, how can one trust those results?

Interpretability is a prerequisite to replace the work of human researchers. But using AI for formalizing mathematics offers some mitigation, Best said. "Instead of asking for an answer, you ask for an answer and a machine-checkable proof that that answer is correct." Beyond error-checking proofs, formalization algorithms conjure new proofs to unsolved math problems.

Such algorithms will require high-quality data, like proofs from disparate fields of mathematics — some quantitative and some more abstract. By carefully teaching computers this way, computers may one day teach us.