  Computation is central to contemporary mathematics. Many accept that we can
acquire genuine mathematical knowledge of the Four Color Theorem from Appel and
Haken's program insofar as it is simply a repetitive application of human forms
of mathematical reasoning. Modern LLMs / DNNs are, by contrast, opaque to us in
significant ways, and this creates obstacles in obtaining mathematical
knowledge from them. We argue, however, 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, even though the original machines are
entirely opaque to us and the proofs they output are not human-surveyable.
