AGENTS.md

Stream: Formal conjectures

[Franz Huschenbeth]

I think a lot of PRs to Formal Conjectures are AI assisted. Some unfortunately use it blind, but thats a problem addressed by this PR FC#2163.

My question is if we should make a AGENTS.md, if we "allow" AI assisted contributions anyway. That way we could reduce reviewing time, if the general structure is more correct. Furthermore it would reduce the time spent during assisted formalization, by not having to mention all the important conventions.

I would see it as a sort of extended and more detailed style and conventions. I would love to discuss this or make a first draft in a PR, if this is something that makes sense.

[Felix Pernegger]

Franz Huschenbeth said:

I think a lot of PRs to Formal Conjectures are AI assisted. Some unfortunately use it blind, but thats a problem addressed by this PR FC#2163.

My question is if we should make a AGENTS.md, if we "allow" AI assisted contributions anyway. That way we could reduce reviewing time, if the general structure is more correct. Furthermore it would reduce the time spent during assisted formalization, by not having to mention all the important conventions.

I would see it as a sort of extended and more detailed style and conventions. I would love to discuss this or make a first draft in a PR, if this is something that makes sense.

What would be the contents of this file? I dont quite understand

[Franz Huschenbeth]

Conventions such as, a problem should be in the corresponding folder to which Problem List it fits to (if multiple then duplicate with %type_of, also include example file reference on how that should be done).

1-2 prime examples of how a file with formalized conjectures should look like.

Or each statement should have a category tag. Or each file should have all references at the top of the file, or if a statement has a research open / closed, then the docstring should contain the reference to the source, where the problem was conjectured / solved. If a statement consists of a certain list, then also look at other files of that list to see conventions of that problem list (e. g. Optimization Constants, or we declare conventions explicit for the list where the conventions are important like Erdos Problems).

It would act as the go to source for details on conventions of the repo (for humans and agents alike, but being more detailed for agents). Of course a lot of conventions are also in the README.md, which is why I opened this topic, to also discuss if we should duplicate content or move content.

[Franz Huschenbeth]

One can also just make a AGENTS.md, which says "Read the README.md" and maybe some additional instructions for Agents. And leave the README.md as the only source of conventions / styles.

[Paul Lezeau]

I’ve been meaning to add one for a while! Let me open a PR with what I’ve got

[Franz Huschenbeth]

Paul Lezeau said:

I’ve been meaning to add one for a while! Let me open a PR with what I’ve got

Nice, I will open a PR to add some of my ideas and observations later on then, if needed.

[Paul Lezeau]

Voila: FC#2182 (still WIP as the style guidelines there aren't quite right - feel free to flag other things that are missing or aren't quite right!)