AI policy

[felixpernegger]

Also see #1623.

The wiki or something should have an AI policy (in whatever way). Obviously right now we are only a handful of people, so this isnt immediately crucial, but important to have for the long term in my opinion.

Realistically there are a few options:

• Allow AI in general, but reporting you use it is mandatory (this seems to be the most common approach)
• Disallow it completely (iirc Wikipedia does this)
• Allow it for typos etc., but not for mathematical content

What do you think is best?

@prabau @StevenClontz

[StevenClontz]

I agree this is an important thing to decide upon as a community.

I tried the copilot PR review process once out of curiousity. It wasn't super helpful for that PR at least. #1479 (review)

My general take on LLMs (which is probably the specific AI we're considering here) for generating mathematics is that they might be fine as long as humans are responsible at the end of the day for the veracity of the content (at least until we have formalization tools to verify proofs). This is different than (say) my opinion on AI-generated art, though I still have concerns over inappropriate use of copyrighted IP (mathematical facts cannot be copyrighted, but the particular presentation of a mathematical proof as prose can be).

[felixpernegger]

My general take on LLMs (which is probably the specific AI we're considering here) for generating mathematics is that they might be fine as long as humans are responsible at the end of the day for the veracity of the content (at least until we have formalization tools to verify proofs). This is different than (say) my opinion on AI-generated art, though I still have concerns over inappropriate use of copyrighted IP (mathematical facts cannot be copyrighted, but the particular presentation of a mathematical proof as prose can be).

By the way, I really wanna start formalising the theorems in pi-base seriously and systematically soon. I set up a minimal working example (+ about 80ish definitions not formatted properly) at https://github.com/felixpernegger/pibase-lean. It would be very nice if we can link to that on the website (similar as in the erdos problems website).
(linking to a seperate repo and not mathlib directly has several advantages)

[felixpernegger]

Maybe we can just use the AI policy from mathlib:
https://leanprover-community.github.io/contribute/index.html#use-of-ai

seems reasonable to me

[prabau]

The examples you gave in #1623 are all pretty trivial, nearly at the level of an enhanced spell checker. I don't see a problem with that particular PR, and mentioning AI does not even seem important in this case.

The main thing is that anything written in a PR must be checked and completely understood by a human. And contributors should take the AI output as a starting point, feeling free to modify it further as needed.

[prabau]

It would be interesting to see a more substantial use of AI than just fixing typos.
(Personally I tried ChatGPT a few times to check questions in mathematics, and it often spews a lot of nonsense, even ChatGPT 5. Depending on how you ask the question, it can tell you different contradictory things. Admittedly, it was the free version via google.)

[StevenClontz]

I'm working on a grant proposal on math databases and AI with a colleague at Kentucky (regretably we didn't get it together for this year's call). Currently, at least for general topology, Gemini and ChatGPT both are quite unreliable for producing math. Gemini Pro did better when I gave it a specific paper and asked it to extract pi-Base style data, but still needed a lot of hand holding.

I think I like @felixpernegger's suggestion that we adopt the mathlib community's AI policy as an existing policy associated with a robust open math research project. If we find reason to deviate in the future, we can discuss at that time.

[StevenClontz]

Here's my proposal to add to https://github.com/pi-base/data/wiki/Contributing

AI Policy

The $\pi$-Base community has chosen to adapt from mathlib the following AI policy:

Using artificial intelligence tools to generate code is becoming more and more common. While this can be practical, their use also poses ethical, ecological, legal and social concerns. We recognise that there are strong differences in opinion on this topic, and do not enforce a strict ban. That said, while individual action alone will not address these concerns, we ask you to consider the effects of your AI use and if it is truly necessary.

If you use artificial intelligence (such as, by using github's copilot mode, asking an LLM like ChatGPT or using an agent like Codex, Claude or Gemini), please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors.

It is essential that you can vouch for all content submitted in a PR, and understand all the content written by an AI. If you don't, then it is possible that the PR actually has negative value to the community, and you are expecting others to do the real work for you!

[felixpernegger]

It would be interesting to see a more substantial use of AI than just fixing typos. (Personally I tried ChatGPT a few times to check questions in mathematics, and it often spews a lot of nonsense, even ChatGPT 5. Depending on how you ask the question, it can tell you different contradictory things. Admittedly, it was the free version via google.)

I suspect at the very least finding traits for sparsely populated spaces should work. Although I doubt an AI would choose the most efficient traits to prove. I can try it out with the Claude Pro model if you have something in mind

[felixpernegger]

Here's my proposal to add to https://github.com/pi-base/data/wiki/Contributing

AI Policy

The
π
-Base community has chosen to adapt from mathlib the following AI policy:
Using artificial intelligence tools to generate code is becoming more and more common. While this can be practical, their use also poses ethical, ecological, legal and social concerns. We recognise that there are strong differences in opinion on this topic, and do not enforce a strict ban. That said, while individual action alone will not address these concerns, we ask you to consider the effects of your AI use and if it is truly necessary.
If you use artificial intelligence (such as, by using github's copilot mode, asking an LLM like ChatGPT or using an agent like Codex, Claude or Gemini), please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors.
It is essential that you can vouch for all content submitted in a PR, and understand all the content written by an AI. If you don't, then it is possible that the PR actually has negative value to the community, and you are expecting others to do the real work for you!

looks good to me!

[prabau]

Not sure how to phrase this exactly, but shouldn't we mention something to the effect that output generated by AI tools should never be blindly copied into a PR, but rather taken as a starting point to be further analyzed and modified by the author of the PR as necessary?

[Moniker1998]

Personally I'm completely opposed to using AI in my work, or reviewing work done by AI, but I am not opposed to it if someone wants to check/publish such changes.

[StevenClontz]

I suspect at the very least finding traits for sparsely populated spaces should work. Although I doubt an AI would choose the most efficient traits to prove. I can try it out with the Claude Pro model if you have something in mind

I highly doubt you'll have much luck, especially if you want it to produce references. All my experiements created "hallucinations" for incorrect traits and the references for correct or incorrect traits.

[StevenClontz]

Not sure how to phrase this exactly, but shouldn't we mention something to the effect that output generated by AI tools should never be blindly copied into a PR, but rather taken as a starting point to be further analyzed and modified by the author of the PR as necessary?

I think that's what this paragraph (copied from mathlib) is getting at:

It is essential that you can vouch for all content submitted in a PR, and understand all the content written by an AI. If you don't, then it is possible that the PR actually has negative value to the community, and you are expecting others to do the real work for you!

But I think in mathlib it's more acceptable to leave an AI-generated result as-is (if it validates), while we probably never want AI output that hasn't been edited at least somewhat since we're writing for humans.

[StevenClontz]

Here's another edit (see final paragraph) to address this:

AI Policy

The $\pi$-Base community has adopted the following policy on the use of AI/LLMs (adapted from mathlib's policy):

Using artificial intelligence tools to generate code is becoming more and more common. While this can be practical, their use also poses ethical, ecological, legal and social concerns. We recognise that there are strong differences in opinion on this topic, and do not enforce a strict ban. That said, while individual action alone will not address these concerns, we ask you to consider the effects of your AI use and if it is truly necessary.

If you use artificial intelligence (such as, by using github's copilot mode, asking an LLM like ChatGPT or using an agent like Codex, Claude or Gemini), please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors.

In particular, submissions that are the unedited output of an AI tool will be closed without review. These tools should be used only to provide a starting point for a contribution, or possibly to help with editing. However, contributions should ultimately be the work of a human who understands and can vouch for their work.