This post refers to a current debate about the possibility of ``mathematicians being replaced by AI'', which is pivoted at a claim asserting that most (if not all) theorems that are of interest to the mathematical community will be solved in the future by AI. That is, the debate seems to be pivoted at the question of whether or not AI can prove theorems better than ordinary mathematicians (let alone ones that are experts in the corresponding areas).
I think this is the wrong question, and it is based on a wrong interpretation of what are mathematicians. The issue is not what machines can prove, but rather what humans can understand. The confusion between these two notions is rooted in an instrumental perception of humans as machines that perform certain tasks (for the benefit of others (indeed, who?)). But humanists know better: To them, humans are the aim (e.g., making humans understand theorems is an aim), not the means (e.g., using humans to prove theorems).
More concretely, I distinguish two aspects of the utility of a proof: (1) convincing us of the validity of a claim, and (2) providing us with an understanding of the claim itself (e.g., why is the claim true). Specifically, for mundane claims (and, more generally, for claims that use as tools while having no real interest in their contents per se), aspect (1) suffices. For example, we don't care to understand the claim $\sqrt{5} \approx 2.2360679775$ but rather get the answer from a computer and use it for whatever we do care about. But when we talk about mathematical theorems, we are always interested in understanding them (i.e., aspect (2)) rather than in merely being convinced in their validity (i.e., aspect (1)).
Now, saying that ``I object to the purported proof of the Four-Color Theorem whose validity is no longer based on firm belief that derives from the understanding of a mathematical situation, but rather on the trust that one is willing to put in a machine lacking a capacity to understand'' or that ``I don't believe in a proof done by a computer [...]. I believe in a proof if I understand it, if it's clear'' confuses these two aspects. It is one thing to say that one has no interest in a proof that teaches them nothing (beyond the validity of the claim), which refers to aspect 2, and another to say that one one cannot be convined of the validity of a claim unless one understands the claim (i.e., that aspect 1 is based on aspect 2). Nevertheless, both assertions may apply regardless if the proof is generated by a computer or by a human. Let me elaborate.
Both quotes equate the two aspects, or rather assert that the only way to be convinced of a claim is understanding its proof. I doubt any human conducts their life based on trhe latter maxim. Furthermore, while I did hear a mathematician claiming that they act according to this maxim when researching, I even doubt that. For sure, most mathematician utilize (within their own research) many claims that they don't really understand. So the valid way of stating the objection to the proof of the Four-Color Theorem is either saying that one has no interest in this proof because it fails to deliver understanding or saying that the purported proof leaves an unproved gap as outlined next.
The point is that standard computer-generated proofs suffer from gaps, which are not inherent (i.e., these gaps can potentially be bridged). Here I refer to gaps between the specification of the computational problem that is supposedly solved by the computer and the actual solution provided. Specifically, the issues at hand are typically the following
I see no valid objection to the use PAs, let alone that it is nobody's business how provers found the proofs they offer us; we should only care about how the proof is presented to us (i.e., can we verify it? do we really understand it?). Indeed, for some decades now, we have been using such PAs for doing mundane calculations of various forms and for getting simplified forms of algebraic expressions (which we can verify by ourselves). Better AI can extend the scope of such PAs, and I believe we should welcome such a possibility. This will allow us to focus more on the essence of mathematics, which is understanding its actual contents (an understanding that also leads to new questions that are aimed at improving this understanding farther).
Acknowledgements: I am grateful to Assaf Kfoury for encouraging me to write this brief text and for commenting on earlier versions of it.
[August 2025]