Ai policy and agent instructions#1187
Conversation
|
Thank you for this PR, which will now be reviewed. Please If you want to bring attention to this PR, please write a message on this |
Agent-actionable instructions belong in the conventionally-discovered AGENTS.md file; human policy and accountability obligations remain in AI-POLICY.md. This separation ensures agents can find their instructions without custom discovery logic, while keeping human-facing policy and enforcement rules separate. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Give agents the merge-blocking checks and a definition-of-done so they self-verify before finishing. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Updated the AGENTS.md file to improve clarity and organization of instructions for AI agents contributing to Physlib.
- Remove duplicate section from `AI-POLICY.md` - Remove redundant prefix wording from `AI-POLICY.md` and `AGENTS.md` - Blank space fixups
|
|
||
| - Use `lemma`, not `theorem`, unless the result is well known in the physics literature. | ||
| - Never use the `axiom` declaration. | ||
| - Never use `sorry`. |
There was a problem hiding this comment.
Better to add following too:
Never use structure fields of type True, or theorems returning True.
Never use an existential statement ∃ x, ..., True (any number of quantifiers ending in True).
Never use a scope-level variable hypothesis that assumes the conclusion.
Forbid True-typed structure fields and theorem conclusions, existentials of the form ∃ x, ..., True, and scope-level hypotheses that assume the conclusion. These declarations typecheck while asserting nothing, which defeats the human-certification obligation in AI-POLICY.md. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
I've approved this and will merge it shortly
jstoobysmith
added
the
ready-to-merge
3 participants
AI-POLICY.md: human-facing contract for AI-assisted contributions. Covers author obligations, review process rules, and enforcement consequences.AGENTS.md: instructions for AI agents working on Physlib. Covers content rules, proof structure guidance, the pre-finish checklist, PR scope, commit conventions, and the format for PR descriptions.The two files cross-reference each other and both point to
docs/ReviewGuidelines.md.Reviewer map: There is no Lean code in this PR. Read
AI-POLICY.mdfirst (human obligations), thenAGENTS.md(agent-facing rules). Check that the two files are mutually consistent and that together they cover the governance surface you expect.