proof-readability

Name: proof-readability
Author: morankor

57stars19forks

How to install proof-readability?

morankor/theorist-toolbox/proof-readability

$npx -y skills add morankor/theorist-toolbox --skill proof-readability

Installs into the current project.

Summary

Polish verified mathematical proofs without changing their mathematical content. Use after a proof has been accepted by the user, a reviewer, Lean, or a co-math review cycle; or when asked to improve proof exposition, readability, signposting, notation, references, or grammar whi

Files · 1

View on GitHub

SKILL.md

1	# Proof Readability
2
3	Edit only proofs whose correctness has already been accepted. This is an exposition pass, not a proving pass.
4
5	Prime invariant: never change the mathematics. Do not strengthen, weaken, replace, or silently repair an argument. If you find a real gap, stop editing that proof and report the gap precisely.
6
7	## Preconditions
8
9	Before editing, confirm one of:
10
11	- the user says the proof is already verified,
12	- a co-math workstream has an approval file,
13	- a Lean build or other formal check accepted the statement,
14	- the task is explicitly limited to readability comments rather than direct edits.
15
16	If correctness is not established, offer a `math-proof` or `codex-math` verification pass first.
17
18	## Six-Layer Pass
19
20	Work in this order:
21
22	1. Architecture: restate deferred results, add proof sketches where appropriate, make theorem/lemma roles clear, close composite proofs explicitly.
23	2. Signposting: add proof openers, named steps, exhaustive case labels, assumption open/close markers, and goal statements before algebra.
24	3. Line-level justification: add reasons for inequalities, signs, substitutions, citations, and relation chains.
25	4. Notation hygiene: define symbols before use, recall object types, stabilize names, check argument order, and avoid notation dumps.
26	5. Intuition: add short "in words" or intuition paragraphs outside the formal proof. Keep every intuition sentence literally defensible.
27	6. Sentence and formula grammar: make formulas part of grammatical sentences, avoid starting sentences with symbols, replace logical shorthand in prose, and run read-aloud checks.
28
29	## Safe Edits
30
31	- Add signposts and roadmap sentences.
32	- Expand an algebraic step already implicit in the proof.
33	- Move definitions earlier when the definition itself is unchanged.
34	- Fix references, labels, theorem names, punctuation, and prose grammar.
35	- Add intuition after the proof or outside the formal argument.
36
37	## Contested Edits
38
39	Propose these in a report; do not apply them without explicit approval:
40
41	- replacing a contradiction proof with a direct proof,
42	- merging or splitting lemmas,
43	- changing standing assumptions,
44	- changing theorem statements, quantifiers, bounds, or conclusions,
45	- reordering an equality or inequality chain when the new order itself needs proof.
46
47	## Banned Phrases
48
49	Remove or replace:
50
51	- clearly,
52	- obviously,
53	- it is easy to see,
54	- straightforward,
55	- similar argument omitted,
56	- by inspection,
57	- this dominates that,
58	- follows naturally.
59
60	Replace each with the actual reason, a precise reference, or a flagged gap.
61
62	## Report
63
64	When done, summarize:
65
66	- edits by layer,
67	- any suspected gaps that were not edited,
68	- any derived intermediate lines that need correctness spot-checking,
69	- contested edits proposed but not applied,
70	- remaining unresolved references or undefined symbols.

People who liked this also viewed

6 picks

Type

proof-readability

57stars19forks

View on GitHub

How to install proof-readability?

morankor/theorist-toolbox/proof-readability

$npx -y skills add morankor/theorist-toolbox --skill proof-readability

Installs into the current project.

Summary

Files · 1

View on GitHub

SKILL.md

1	# Proof Readability
2
3	Edit only proofs whose correctness has already been accepted. This is an exposition pass, not a proving pass.
4
5	Prime invariant: never change the mathematics. Do not strengthen, weaken, replace, or silently repair an argument. If you find a real gap, stop editing that proof and report the gap precisely.
6
7	## Preconditions
8
9	Before editing, confirm one of:
10
11	- the user says the proof is already verified,
12	- a co-math workstream has an approval file,
13	- a Lean build or other formal check accepted the statement,
14	- the task is explicitly limited to readability comments rather than direct edits.
15
16	If correctness is not established, offer a `math-proof` or `codex-math` verification pass first.
17
18	## Six-Layer Pass
19
20	Work in this order:
21
22	1. Architecture: restate deferred results, add proof sketches where appropriate, make theorem/lemma roles clear, close composite proofs explicitly.
23	2. Signposting: add proof openers, named steps, exhaustive case labels, assumption open/close markers, and goal statements before algebra.
24	3. Line-level justification: add reasons for inequalities, signs, substitutions, citations, and relation chains.
25	4. Notation hygiene: define symbols before use, recall object types, stabilize names, check argument order, and avoid notation dumps.
26	5. Intuition: add short "in words" or intuition paragraphs outside the formal proof. Keep every intuition sentence literally defensible.
27	6. Sentence and formula grammar: make formulas part of grammatical sentences, avoid starting sentences with symbols, replace logical shorthand in prose, and run read-aloud checks.
28
29	## Safe Edits
30
31	- Add signposts and roadmap sentences.
32	- Expand an algebraic step already implicit in the proof.
33	- Move definitions earlier when the definition itself is unchanged.
34	- Fix references, labels, theorem names, punctuation, and prose grammar.
35	- Add intuition after the proof or outside the formal argument.
36
37	## Contested Edits
38
39	Propose these in a report; do not apply them without explicit approval:
40
41	- replacing a contradiction proof with a direct proof,
42	- merging or splitting lemmas,
43	- changing standing assumptions,
44	- changing theorem statements, quantifiers, bounds, or conclusions,
45	- reordering an equality or inequality chain when the new order itself needs proof.
46
47	## Banned Phrases
48
49	Remove or replace:
50
51	- clearly,
52	- obviously,
53	- it is easy to see,
54	- straightforward,
55	- similar argument omitted,
56	- by inspection,
57	- this dominates that,
58	- follows naturally.
59
60	Replace each with the actual reason, a precise reference, or a flagged gap.
61
62	## Report
63
64	When done, summarize:
65
66	- edits by layer,
67	- any suspected gaps that were not edited,
68	- any derived intermediate lines that need correctness spot-checking,
69	- contested edits proposed but not applied,
70	- remaining unresolved references or undefined symbols.

People who liked this also viewed

6 picks

Type