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."