Apriori Knowledge in an Era of Computational Opacity: The Role of AI in Mathematical Discovery

TL;DR

The paper investigates whether apriori mathematical knowledge can be derived from computer outputs and argues that transparency of the computational process is key. It analyzes traditional computer-assisted proofs like Appel–Haken's 4CT and contrasts them with opaque DNN/LLM outputs, proposing a two-pronged pathway: direct apriori knowledge only when the computer's reasoning is transparent, and indirect apriori knowledge via a transparent proof-checker verifying stored proofs. The contributions include articulating Main Claim 1 and Main Claim 2 and illustrating with the 4CT and Cap Set examples, along with a formal mechanism for proof-checking to recover apriori knowledge from opaque systems. This has practical implications for mathematical discovery and suggests extending the approach to general scientific reasoning through transparent verification.

Abstract

Can we acquire apriori knowledge of mathematical facts from the outputs of computer programs? People like Burge have argued (correctly in our opinion) that, for example, Appel and Haken acquired apriori knowledge of the Four Color Theorem from their computer program insofar as their program simply automated human forms of mathematical reasoning. However, unlike such programs, we argue that the opacity of modern LLMs and DNNs creates obstacles in obtaining apriori mathematical knowledge from them in similar ways. We claim though that if a proof-checker automating human forms of proof-checking is attached to such machines, then we can obtain apriori mathematical knowledge from them after all, even though the original machines are entirely opaque to us and the proofs they output may not, themselves, be human-surveyable.