Min Cheol Seo

You may have come across a headline claiming that ‘AI is automating mathematical proofs’ in recent years. When reading such a headline, we first need to ask what is meant by ‘automation of mathematical proofs’ and what it is taken to imply. We provide an overview of various technological advances under the umbrella of ‘proof automation,’ which often seek heterogeneous aims. What, then, should we make of such advances labeled as ‘proof automation’? We introduce three philosophical perspectives that disagree about the status of ‘mathematical understanding’ with regard to mathematical proofs, and illustrate the impact of ‘proof automation’ on each perspective. Finally, we consider how ‘proof automation’ ties in with the general trend of ‘science automation.’