Human skepticism and formal verification

Benjamin Friedman, postdoctoral fellow at Université du Québec à Montréal (UQÀM)

Introduction

On October 6, 2026, the artificial intelligence company OpenAI released a github repository containing 722 articles claiming new results across a large variety of mathematical disciplines. According to OpenAI, their models worked for an average of three hours to achieve each of the results.

Of note here is the decision to list the author of each article simply as “OpenAI”. It is highly unusual in mathematical scholarship for a company to be considered the author of an article. The decision to have the mathematicians hired by OpenAI generate these results anonymously is clearly intentional, since the idea is to show off the creative powers of the company’s product.

More troubling is the idea that these problems are already considered “solved” the same day that they are released to the public, well before the mathematical community has had any opportunity to verify the solutions. Many of these articles were accompanied by Lean scripts, with the implicit justification that so long as the statement in the article corresponds to the type instantiated in the Lean script, the results are to be seen as true.

I argue in this piece that formal verification, including Lean, is a mechanized implementation of a skeptical posture that is essential to mathematical practice, but that a certificate of formal verification is an unsatisfying substitute for human skepticism. I conclude the essay by advocating for methodological skepticism as a practice that will help keep our field grounded amid the tumultuous changes brought about by AI systems.

Skepticism as a mathematical method

Before we can describe how Lean mechanizes skepticism, and why a Lean certificate on its own is not satisfying, we must first understand the role of skepticism in mathematical practice. The role of skepticism in mathematics is methodological. The titular method in Descartes’ influential 1637 work Discourse on the method of rightly conducting one’s reason and of seeking truth in the sciences is a methodological skepticism, in which one advances carefully towards truth, never accepting any fact unless entirely convinced of its veracity. Descartes likens knowledge without a firm foundation to a building “built on mud or on sand”. One might imagine a skeptical attack of one’s purported knowledge as analogous to a “stress-test” of the building’s stability. Is this claim really established beyond all doubt? Let me shake it and see whether it stands, or whether it all comes crashing down! Thus, in the Cartesian view we can be certain only of those matters which stand up to the highest degree of skeptical attack.

This degree of skepticism is much too stringent to be practical in most contexts. Indeed, Descartes points out that since our knowledge of the world is factored through sensory experiences, which may be compromised by an elaborate deception, we cannot apply this methodological skepticism to most worldly matters. However since our objects of inquiry are abstract, mathematicians have the rare luxury among thinkers of being able to apply Cartesian-level skepticism to achieve substantial results.

In his book Mathematica, the mathematician and writer David Bessis draws on the writings of Descartes, Grothendieck, Thurston and others to show that mathematical practice consists of two layers: an “official” mathematics, in which we use formal logic to deduce facts about abstract mathematical objects, and a “secret” mathematics, which is an imaginative mode of thought, in which one develops mental pictures and intuitions for mathematics. According to Bessis, one develops mathematical knowledge through interrogating and correcting one’s intuitions about mathematical objects, leading to greater understanding. Thus, methodological skepticism is directed inwardly in order to sharpen the clarity of one’s mental pictures.

To illustrate this, Bessis makes a geometric claim: A straight line can intersect a circle in at most two distinct points. By employing a modest degree of visual imagination, one can attempt to refute the claim by trying to visualize a line intersecting a circle in three distinct points. However in this attempt at refutation, one will become convinced of the claim.

This also explains why experienced mathematicians can seem to their junior colleagues like they have supernatural abilities. A couple of years ago I had the distinct fortune of getting to meet a famous and influential mathematician in my field. I was explaining to him a problem that I was working on at the time, and he very quickly isolated certain hypotheses that would be required. My advisor and I had in fact come to the same conclusion, but over the course of several months instead of over the course of one conversation. The remarkably quick, seemingly effortless realization is very impressive. It was certainly not, however, a result of him rapidly performing formal deductive arguments or symbolic manipulations in his head. Rather, if we accept Bessis’s model of mathematical practice, then the explanation would be that he has developed a deep intuition for these sorts of problems through sustained mental habits – namely the creation of mental pictures paired with the skeptical interrogation and refinement of those pictures – over many years.

There is another account of skepticism that is important in order to understand the role of formal verification. The philosopher Catarina Dutilh Novaes argues in her book The Dialogical Roots of Deduction that deductive reasoning is structured around a dialogue between a prover, who seeks to establish a claim, and a skeptic, who resists belief in the claim unless compelled. Despite being on opposing sides of the dialogue, both roles are essential to establishing an air-tight deductive argument.

This dialogue is core to mathematical practice. Sometimes the dialogue is implicit, such as when a mathematician writing down a proof anticipates the objections of a skeptical reader. At other times, the dialogue is explicit, such as when a colleague at a seminar presents an objection to a mathematician’s argument, to which that mathematician is now obliged to respond to the colleague’s satisfaction.

A routine part of my training as a mathematician has been defending claims I wanted to make against the challenges of my teachers. Did my teachers really disbelieve the claims that I was making? Maybe in those rare cases in which my claims were entirely original, or in which I was making a claim about a more obscure result. But my teachers’ skepticism was present even when I was presenting results from well within the canon of my field. It would be ridiculous to imagine that the Hodge decomposition theorem, a standard theorem of differential geometry, is doubted by any expert. Rather, this skepticism is methodological on the part of my teachers, these interrogations serving as probes of my understanding. This is in line both with Bessis’s account of skepticism as sharpening one’s intuitions, as well as with Dutilh Novaes’ dialogical model, in which they are playing the skeptical role in a dialogue.

Dialogue between humans, and in particular the application of skepticism, has been the basis by which mathematical truth has been established for thousands of years, until the advent of:

Formal verification

Lean 4 is a proof assistant, meaning that it does not generate proofs, but only checks a proof’s validity. The basic concept behind this verification is something called the Curry–Howard correspondence, or “proofs as programs”. The Curry–Howard correspondence is related to the branch of computer science known as type theory. A theorem corresponds to a type, while a valid proof of the theorem corresponds to an instance of the type. This is more complicated than the type theory that one would typically encounter in an introductory computer science class, in which one would learn that $0$ and $613$ and $-7$ are instances of the type $\mathrm{int}$, but it is the same idea.

The idea behind formal verification, that a mathematical proof can be presented as a computer program whose successful compilation corresponds to the proof’s validity, was somewhat unsavoury to me at first, perhaps because I was unsettled at the idea of human skepticism being replaced by a mechanized process. Nevertheless, I was reassured to find that the proponents of Lean were not arguing to replace human skepticism with formal verification, but instead arguing that Lean could serve as a strong additional test of a theorem’s validity.

Using Lean can be thought of as a technological implementation of the prover-skeptic dialogue, in which the user assumes the role of prover, while the skeptic role is mechanized. To illustrate this, here is some Lean code attempting to formalize the famous proof that there exists no rational number $q$ such that $q^2 =2$, a proof by contradiction:

The intro tactic on line 4 introduces, by way of contradiction, a rational number $q$ satisfying hq, which states that $q^2=2$. This is followed by my attempt at convincing Lean that we can substitute $q = \frac{a}{b}$ with $a,b$ in lowest terms into the equation $q^2=2$. This is all code that I wrote, so we are seeing only the “prover” side of the dialogue. Let’s see Lean’s response at line 11:

This “tactic state” describes Lean’s understanding of the proof at line 11, beginning with a list of statements which I have convinced Lean to accept, namely

• that we have a rational number $q$,
• that we have $q^2=2$ (this is called hq),
• that there is an integer $a$ equal to the numerator of $q$ and a natural number $b$ equal to the denominator of $q$, and
• that we can substitute $q=\frac{a}{b}$ into the equation $q^2=2$.

Since this is a proof by contradiction, the goal, which is the statement appearing after the $\vdash$ symbol, is the statement False.

So far, so good. If I was presenting this proof in a lecture hall, then Lean would be an audience member who is following my reasoning and is satisfied by my argument up to this point. But when we get to line 14, where I attempt to show that the greatest common divisor (GCD) of $a$ and $b$ is equal to $1$, an error message shows up:

Remember that theorems in this context are types, so when the error message says that there is a “type mismatch”, this means that the statement I claim to be proving is not accepted by Lean as being entirely justified. Returning to the lecture hall, we can imagine the audience member raising a hand and objecting.

“Benji,” I hear this audience member say. “You promised to prove to us that the GCD of $a$ and $b$ is equal to $1$, but instead you proved that they are coprime! Thus, I don’t accept your line of reasoning!”

This scenario is absurd, because real life humans know well that two integers are coprime if and only if their GCD is $1$. In fact, most people take this to be the definition of “coprime”. Lean takes a more general definition encoded in Mathlib: two elements $a, b$ of a ring $R$ are said to be coprime if the sum of the ideals generated by $a$ and $b$ is the entire ring:

$$\langle a \rangle + \langle b \rangle = R.$$

So if I wanted the error message to go away (that is, if I wanted to respond to the audience member’s objection to their satisfaction), I would have to prove that these two ways of looking at coprimality are equivalent in the ring of integers. This would not be difficult to do, but the point is that Lean gets hung up on these sorts of things all the time. The example here is a minutia with which no human mathematician would ever be bothered, but the argument put forth by proponents of Lean is that the process of formalizing a proof in Lean can sometimes result in important gaps being caught.

So we have seen that Lean is very good at being skeptical. This degree of skepticism is precisely the point of Lean, and why a Lean certificate grants a mathematical result a high degree of credibility.

OpenAI’s rapid advances are due to a mechanized prover-skeptic dialogue

Let us return now to the 722 results claimed by OpenAI. The spectacular rapidity with which the anonymous mathematicians at OpenAI have progressed is due to both roles in the prover-skeptic dialogue being mechanized. Lean on its own does not generate new proofs, so some generative program (i.e. a large language model) is required. On the other hand, without Lean performing the necessary skeptical role, there would be no way to verify the claims made by a large language model, at least not without an expenditure of human effort that OpenAI has neither the resources nor the interest to pursue.

Furthermore, formal verification using programs like Lean can be used to improve large language models, since the large language model can use feedback supplied by Lean to correct itself.

However, almost all headlines about AI progress in math have focused on the AI systems acting as the prover, and not nearly as much on Lean, which plays an unsung but equally essential skeptic role. As an aside, I am skeptical that other fields will see the same degree of progress made by AI in the near future, because verification of the output of generative AI systems cannot yet be efficiently mechanized in other fields. For example, there is no equivalent of Lean for oncology, so I believe that we are unlikely to see significant developments in cancer research being made by AI systems in the near future.

Why is a Lean certificate unsatisfying?

As I explained above, Lean is ridiculously good at being skeptical. Is a Lean certificate then to be taken as an infallible confirmation of a mathematical result? While there have been concerns raised about possible Lean kernel bugs, let us be generous and assume that a Lean certificate is an infallible confirmation of a theorem’s truth. That is, we will assume that if a type corresponding to a mathematical result has been instantiated in Lean, then the result is certainly true.

Even then, if a mathematician is seriously interested in a mathematical result, a Lean certificate on its own is unsatisfying. As explained above, it is an essential part of the methodology of mathematics to consider mathematical claims with skepticism, and this applies even if one believes the claims to be true.

This is in some ways a strange way to evaluate truth, and it is at odds with more everyday justifications for belief. For example, even though I have never studied its proof, I don’t really doubt Fermat’s Last Theorem in any practical sense, since its proof has been scrutinized by many experts in number theory. However, my belief in Fermat’s Last Theorem is justified only by an appeal to authority, so within a methodologically skeptical framework I do not know it to be true at all!

Thus practicing methodological skepticism sometimes involves make-believe. I will pretend not to believe in a theorem (even though I do believe it), in order to give myself the opportunity to be compelled to believe it. The process of being compelled to believe is what allows me to understand the theorem.

So sure, on some level I believe mathematical claims that are verified in Lean, even if I have not studied their proofs, but this is also basically an appeal to authority. From the perspective of methodological skepticism, I do not know that the results claimed by OpenAI are true until I have studied them and personally convinced myself that they are true.

Perhaps more substantially, it is impossible for a Lean certificate on its own to replace the role of skepticism explained by Bessis – skepticism as a process of interrogating and correcting one’s intuitions. Since a computer does not have access to our internal mental intuitions, there is no technological shortcut here. I am reminded of the famous statement attributed to Euclid, that “there is no royal road to geometry.” In one of many likely apocryphal stories about mathematicians from antiquity, it is said that he was responding to King Ptolemy’s question about whether there is an easier way to learn mathematics.

Recommendation

My recommendation is something that most mathematicians already practice: we should strive to use methodological skepticism to evaluate mathematical claims. This means that one should not believe a claim about mathematics unless personally convinced of its truth.

To be clear, this is an ideal from which I frequently fall short. Many mathematicians, including me, have a habit of using results “out of the tin” without understanding their proofs. However, I recognize that when I do this I am missing the mark. I tell myself that I will come back later and study the proofs of the results that I am using, and sometimes I actually follow through on that.

Since the coming of generative AI, we have seen large language models and Lean make progress in mathematics at a rate that is difficult or impossible to keep up with. Perhaps in the near future new and unbelievable mathematical results will be claimed that sound like they were lifted out of science fiction. These claims may be backed up by Lean certificates. Under these circumstances, it is important that we do not lose our heads. The practice of skepticism, of being able to say “I don’t know this to be true” will keep us grounded.

Acknowledgements

The author thanks Laurestine Bradford, Thomas B. Friedman, Anshula Gandhi, Patricia Marino, Yuveshen Mooroogen, as well as the editors at Proofs and Prompts for helpful comments on an earlier draft of the essay.

---

Received 28 October 2026, revised 1 November 2026.