Skip to content

Commit be54c78

Browse files
committed
docs(agents): separate gap diagnosis from admission
1 parent 0db39a2 commit be54c78

3 files changed

Lines changed: 29 additions & 2 deletions

File tree

.agents/skills/learn-from-math-agent-trajectories/SKILL.md

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,14 +124,27 @@ postcondition with typed inputs and an exact, incomplete, or unknown result. It
124124
must not encode the motivating conjecture, prescribe a proof strategy, or
125125
claim an asymptotic theorem that still requires model reasoning.
126126

127+
Separate gap diagnosis from public-operation admission. First decide whether
128+
the trajectory establishes a reusable missing mathematical postcondition on
129+
the inspected surface. Recording that gap does not assert that the result
130+
belongs in the agent-visible catalog. Then report the admission evidence
131+
separately: it may support public consideration, suggest a native-only helper,
132+
or leave the disposition unresolved. Public-admission concerns such as weak
133+
leverage over ordinary Python or a cheap projection can change the eventual
134+
disposition without erasing an otherwise well-evidenced gap. Conversely, an
135+
absent convenience is not an operation gap unless the missing postcondition is
136+
independently canonical or reusable.
137+
127138
## Turn observations into repository learning
128139

129140
Choose the smallest durable action supported by the evidence:
130141

131142
- update a repo-local skill for a reusable agent decision rule;
132143
- improve discovery metadata when an existing operation was hard to find;
133144
- repair an operation contract when a selected tool was hard to call or use;
134-
- propose a new operation for a repeated, stable bounded postcondition;
145+
- record an operation gap for a repeated, stable bounded postcondition, and
146+
propose public admission only when the separate admission evidence supports
147+
it;
135148
- update product documentation only for a public contract or durable product
136149
behavior that users need outside agent instructions;
137150
- preserve a trajectory as an evaluation when it has a frozen input,
@@ -163,6 +176,9 @@ Lead with what the trajectory teaches, not a chronological replay. Include:
163176
actions; and
164177
- unresolved mathematical work that still requires proof or human judgment.
165178

179+
For each operation-gap finding, state the gap verdict and the admission posture
180+
separately. Do not make a reader infer one from the other.
181+
166182
Keep confirmed facts, plausible hypotheses, and open questions visibly
167183
separate. The retrospective succeeds when another agent or maintainer can
168184
verify the lesson from the original artifacts and decide on a bounded next

.github/ISSUE_TEMPLATE/math-gap.md

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ assignees: []
1515
<!-- What custom code, external library call, solver encoding, or manual work was needed? -->
1616

1717
## Gap classification
18-
<!-- Check one. Only a genuine operation gap normally proceeds to admission. -->
18+
<!-- Check one. An operation gap records a missing postcondition; it does not pre-admit a public operation. -->
1919
- [ ] representation
2020
- [ ] interoperability
2121
- [ ] discovery
@@ -24,6 +24,9 @@ assignees: []
2424
- [ ] operation
2525
- [ ] reasoning
2626

27+
## Admission posture (operation gaps only)
28+
<!-- State whether the evidence supports public-catalog consideration, suggests native-only support, or leaves disposition unresolved. Public admission is a later decision. -->
29+
2730
## Existing math.find queries
2831
<!-- Queries already tried and what they returned. -->
2932

docs/explanation/executable-mathematical-vocabulary.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,14 @@ Not every failed attempt reveals a missing operation.
102102

103103
Only a genuine operation gap normally motivates a new public operation.
104104

105+
Gap diagnosis and public-operation admission are separate decisions. A focused
106+
issue may record a reusable missing postcondition even when the available
107+
evidence does not yet establish enough leverage for the agent-visible catalog,
108+
or when the eventual disposition may be `NATIVE_ONLY`, `SPLIT`, or `DROP`.
109+
Admission gates decide that later disposition; they should not suppress an
110+
evidence-backed gap record. Conversely, recording an operation gap does not
111+
pre-admit a catalog operation.
112+
105113
## What tends to be useful
106114

107115
Useful operations usually turn substantial computation or mathematical

0 commit comments

Comments
 (0)