Disclosure of AI tools in PRs

Stream: PrimeNumberTheorem+

[Terence Tao]

It has been pointed out to me that it would be good practice going forward to disclose which PRs of proofs were at least partly AI-generated, and which tools were used, for instance this would help with tagging code as AI-generated or human generated for future training. So I would like to open a discussion on what the best practices on this should be. Is there some way to prompt any PR submitter to either declare that their code is human generated, or to disclose AI usage? We could rely on self-disclosed sentences attached to each PR but it will be all too easy to forget to do such a disclosure.

[Pietro Monticone]

I have documented everything that was formally proven manually vs. formally disproven by Aristotle and fixed manually vs. formally proven by Aristotle and golfed manually, etc. (e.g. see here) but I'm sure there are better and more systematic practices.

[Chris Henson]

I find marking AI as coauthors in git commits a nice practice. Claude can do this automatically, and for Aristotle Mathlib and CSLib have done so manually. You just add Co-authored-by: Aristotle Harmonic <aristotle-harmonic@harmonic.fun> at the end of the commit and this will be recorded on GitHub.

[Pietro Monticone]

I'm adding @Aristotle-Harmonic as co-author too.

[Alex Kontorovich]

These days, I use Claude almost as much as Mathlib Docs, just for theorem name searches, and for help when I forget syntax. I copy the relevant parts of its responses (from the browser) and paste them into VS Code. Does that count as "AI-generated", or is the resulting code still "mine"?

[Andrew Peterson]

It's possible to add a pull request template for a github repository: link

Essentially you put a markdown file at .github/pull_request_template.mdand the text when you create the PR will be originally filled with what's in the markdown file. For example, you can have a checklist to fill out, or a question asking the submitter to describe their AI usage in the PR.

If you wanted to, you could also have a github action to verify that the checkboxes are filled out in the PR, but that would involve some work and probably isn't worth it.

[Eric Vergo]

In the interest of continuing the discussion surrounding best practices:

PR #535 was vibe-proven using Claude code. To allow for easier inspection of that process I used claude-code-log, which generates an interactive html page containing the entire session (prompts, tool calls, etc.). A readme plus all of the relevant files can be found here.

The PR was vibe proven last week at the NYC meetup and after the LLM completed the proof inspecting the logs was informative. People are using a variety of tools, many of which don't enable something like this so I don't think it can be a requirement but I think it's important to try out things like this while you are in the thick of things.

Screenshot 2026-01-16 at 2.28.13 PM.png