Tapering AI Limits with Mathematcial Formalization

Dr. Alex Best, of Harmonic discusses AI's 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, Alex Best says. "Instead of asking for an answer, you ask for an answer and a machine-checkable proof that that answer is correct."