If you are a collaborator working with me on a research project, it's critical that you understand my position on how you can and can't use AI.
The very short, simple, and memorable version of my policy is: You may not use AI tools except when we have express prior agreement. All the words there—especially “not”, “express”, and “prior”—are critical.
The key reason I have this policy is because when we do research together, if we produce results, people must be able to trust them. Trust is very easy to lose and very hard to build. As my collaborator, you benefit from the trust I've built up over decades. You have an obligation to not torch it. Of course, AI is not unique: humans have been making errors for as long as we have existed. But those are errors against which I have built up good defenses. In contrast, AI makes whole new kinds of errors that we do not properly understand, so we have to treat its use with extra caution.
Therefore: if you violate this policy, I may warn you at most once, depending on how egregiously you violate it; but no matter what, after two violations, I will terminate working with you.
If you don't like any of the above, think I'm just too old-fashioned, etc., that's fine. Just let me know, and we will not work together. I wish you luck in your future collaborations.
With that out of the way, here's my policy in more detail. Note that this is written just after mid-2026. Things could be different a year from now! If in doubt, just ask me—but please don't presume.
This can be a very good or very bad use-case, depending on the purpose. In addition, even when it makes sense, I need to understand what mechanisms you have in place for validating the correctness of what gets produced. My (fairly significant) experience with AI coding is that it does routine tasks exceptionally well. However, whenever tasks fall “outside distribution”, its quality varies. Furthermore, it can be misleadingly reassuring: generating correct-looking code, writing lots of documentation, producing voluminous tests, etc. All these mask numerous failure modes that I have experienced personally. Therefore, no AI coding until I understand your background and practices.
This can be a pretty good use. But that depends on a lot of things.
First of all, you need to understand that the primary value of formal methods is not actually proof, it's understanding. You get that by wrestling with the specification and proof. If you try to automate that, you will lose both the primary benefit (understanding your problem better) and the secondary benefit (of actually obtaining a proof). The former may strike you as vaguely true in the abstract, but surely the latter is utterly false?
Actually, no, it's not. If you use the same input to generate both the specification and the properties checked against the specification, then you run into the serious risk of correlated failure. (This is, of course, also true of code and tests.) This is why I do not believe in “autoformalization”. It's vital that your properties, especially, be carefully vetted by hand. Use tools like PICK if you'd like!
This can be a very good use of AI tooling. First we agree on what diagram we want: sketched by hand on paper or computer. Once we've agreed, then AI can be very helpful for conversion to our formats, especially some code libraries. Make sure you triple-check that the output captures what we asked for. If it doesn't, and it's proving hard to get it right, talk to me instead of just assuming I'd be fine with the output.
I make a real distinction here between “diagrams” and ”images” more broadly, like pictures. Many people feel a deep revulsion towards AI-generated artwork. Irrespective of how you feel about it, we should not use it. When needed, we can pay to hire an artist.
Most of all: no AI-generated prose. None.
I'm not going to repeat everything that has already been said about how writing is thinking, etc. Nor go into a lot of detail about how if I wanted the output of AI, I can just prompt a model myself. Of course, all those things are true. I just hope I don't have to repeat them.
What I will add is this: Over the decades, I've learned how to read student writing closely to figure out what they are thinking, where they might be making mistakes, etc. I can only do that if I read your own prose. Every filter or transformation you apply to it obscures your thought, and makes it harder for me to feel confident about our collaborative research.
Therefore, I want to be clear that this is non-negotiable. If you have lost the ability to write (already!), please find someone else to work with. I do not need you to write well; that's something I know how to teach you. You just have to be willing to put in the hard yards of writing yourself.
Note that there are some clear corner-cases here. I would like you to use a spell-checker. Especially if you are not a native speaker, I am happy to have you use a grammar checker that makes small, local corrections. Discuss these things with me.
But having AI write all the prose, or writing a draft and having AI extend or fill it out, or pasting your draft into AI and having it just rewrite the prose for you and pasting the output into material I see—these are all absolutely unacceptable.
You can guess what I'm going to say. AI summaries are not a substitute for reading a paper. In my experience, they often miss critical details. They get things wrong. They also focus on the “easier” parts—the background, shared knowledge, etc.—that is represented well in their training sets, and do poorly on the novelty (which is ill-represented), which is usually the whole point of the paper.
If you have a particularly good use-case, talk to me about it. Let's discuss it. Help me understand your practices and, in particular, your safeguards. As with all of the rest of the above, proceed only after that.