I’ve recently been taking part in a conversation on the Lean Zulip about what to do when a conjecture is resolved using AI and a proof assistant (in this case Lean). The conversation can be found here. This is my take and conclusion from the discussion there, and is an extension of one of my posts. I frame this as an open letter to anyone who finds themselves having resolved a conjecture with very little human input using AI and a proof assistant.

Dear Reader,

So, an AI (under your guidance) has shown an open conjecture is true or false using a proof assistant. Let’s start by saying what this is. It is an advancement in human understanding and in human knowledge. Now, let’s say what it isn’t: it isn’t a proof of that result in the traditional sense of the word. That means a motivated, human-written and human-readable argument that convinces a human that something is true or not. So let’s suggest another word for what you found. Let’s call it a ‘warrant’ for that conjecture; something that licenses a belief without supplying understanding.

You can think of finding a warrant as similar to digging in a field and finding a dinosaur bone. Such a discovery requires no expertise on your part. It is just luck that you were digging in the right place and that no one had dug there before you. Finding a dinosaur bone obviously doesn’t make you qualified to say anything about why the dinosaur was there, what dinosaur it belonged to, the age of the bone, etc. The same holds for finding a warrant. Just because you found a warrant doesn’t mean that you have any expertise in the mathematical area it was found. It doesn’t necessarily mean you have any expertise to turn that warrant into a fully-fledged proof in the traditional sense. The situation described here is essentially “serendipity” and such serendipity has often been the driving force of science.

Of course, you can increase your chances of being lucky and finding a dinosaur bone by hiring a digger and a dumpster truck to help you move more dirt. Though people may look at you and question why you spent so much money on trying to find dinosaur bones in such a way when that money could have been better spent on understanding the bones that we’ve already got or paying for more experts to find more interesting bones. And in doing so, you may have destroyed the evidence pointing to why that dinosaur bone was there in the first place, or trails pointing to more interesting dinosaur bones making them harder for others to find.

So, with the dinosaur metaphor in mind and assuming you’ve already spent that money finding a warrant, what do you do with it?

I think there isn’t a single well-defined answer to this question, but this shouldn’t surprise us because there isn’t a single well-defined answer to the same question applied to a traditional proof in mathematics. If I come up with a proof of a result in mathematics in the traditional sense, and I ask people what I should do with that proof, I’m going to get different answers: some people will say that I should make it public right away; some will say I should hold off till it’s published in a journal; some will say I should put it on the arXiv; some might say it’s not even worth that, and I should just put it on a blog post.

The thing that resolves this conundrum in practice is “academic judgment”. As academics we put our trust in one another to make the best decision we can based on the evidence we have and the values we hold. There is no absolute right or wrong here just the need to do one’s best in the situation one finds oneself in. That means exercising academic judgement in a way that can be justified on rational grounds, and one which is motivated by the pursuit and dissemination of knowledge and fairness rather than self-interest. When you make an academic judgement the thing at risk is your reputation and the health of the discipline.

Everyone involved in academic pursuits either as a citizen scientist or professional academic has to exercise some level of academic judgment. Let’s go back to the analogy of dinosaur bones. If, as an amateur hobbyist, you find something that looks like a dinosaur bone, you must use your judgment about what to do with it. That judgment can be guided by things like the internet, books, guides, or just common sense, but eventually a decision must be made. If you think you have actually found a dinosaur bone, you may contact the relevant paleontologists to take a closer look, or send it to a local museum so it can be stored and cataloged. If you keep going to paleontologists with things that are, in fact, fun-shaped rocks rather than dinosaur bones, then people are going to stop trusting you and replying to your messages. Your reputation will be diminished.

It’s easy to mistake the equivalence of a fun-shaped rock for a warrant in mathematics. When an AI produces a warrant, it’s important to check that the warrant actually resolves the conjecture you think it does: that the statement of the conjecture is correct, and that no additional axioms are introduced, or hypotheses are added. Again, the thing on the line here is your reputation.

So, I’m not going to prescribe exactly what I think you should do with your warrant. That is down to you based on your own academic judgment. What I am going to outline is what I think we want the desired outcome of such academic judgment to be.

To me, the desired outcome should contain two aspects. Firstly, the warrant of the conjecture should be made public, and the relevant areas of the community should be made aware of its existence. This is taking a kind of purist view that a warrant is mathematical information, and our job should be to increase the mathematical knowledge that humanity has. To not release a warrant and to not make it public seems like a disservice in this respect. It would be great if, every time you found a warrant, you also happened to be an expert in the corresponding area and the corresponding mathematics that are used in the proof, so that you could write a human-digestible proof of it. But in most cases, this is not going to be true. To me, the answer to that should not be just to ignore the existence of the warrant, but rather to disseminate it in a way that makes those facts clear. Naturally, in cases where you can understand the proof, there is probably going to be some expectation that you write some sort of digest of it (or that you make some sort of effort to make it accessible for those reading it). But even if you have an understanding of the theorem, it’s not necessarily true that you’ll have an understanding of the underlying mathematics that forms the proof.

Given that I believe that the warrant of the conjecture should be made public, the second point is to take the social view of mathematics as a discipline rather than just as a body of knowledge. In this viewpoint, the second aspect of the desired outcome is that the dissemination of the warrant of the conjecture does not adversely affect progress towards a traditional proof of that conjecture, nor the resources and credit given to such an endeavour. There is no magic solution for how to do this, and in the long term, it is likely going to require a change in perspective, which ripples throughout the whole community. Those who hold warrants, and publish them, are where that shift in perspective will spread from first.

So, serendipity has been on your side. You found a warrant to an open conjecture. You should be very pleased that this is an advancement of knowledge. Now it’s time to use your academic judgment and decide what to do with that. I wish you the best of luck.

Best wishes, Joseph.

Acknowledgments

Recently I have engaged in many intresting discussions that have formed my opinion on this topic. While the views here are solely my own, I thank those who have contributed to these discussions. In particular, I thank all those that took part in the Lean zulip discussion linked to above, especially Alex Meiburg and Laura Monk for helping extend the dinosaur analogy. I also thank Thomas Powell, Andy Smith, and Alex Zughaid for their valuable input and feedback.