A Priori Knowledge in an Era of Computational Opacity: The Role of Artificial Intelligence in Mathematical Discovery

Abstract Can we acquire a priori mathematical knowledge from the outputs of computer programs? Although we claim Appel and Haken acquired a priori knowledge of the four-color theorem from their computer program insofar as it merely automated human forms of mathematical reasoning, the opacity of modern large language models (LLMs) and deep neural networks (DNNs) creates obstacles in obtaining a priori mathematical knowledge in analogous ways. If, however, a proof-checker automating human forms of proof-checking is attached to such machines, we can indeed obtain a priori mathematical knowledge from them, even though the original machines are entirely opaque to us and the outputted proofs cannot be surveyed by humans.