Arrow

Rigorous mathematical proof construction and audit for AI agents

Arrow develops, audits, repairs, and clearly presents mathematical proofs without turning uncertainty into confidence.

Why Arrow?

AI proof writing often fails in a predictable way: an argument reaches a difficult step, replaces it with persuasive prose, and reports the theorem as proved. Arrow treats every unresolved step as a first-class proof obligation.

Its central rule is simple:

Never convert a plausible argument, numerical pattern, elegant reduction, or missing lemma into a claimed proof.

Arrow is a portable Agent Skill designed to work with both Codex/GPT and Claude.

What it does

• Tests whether a statement is true before committing to a proof.
• Tracks every load-bearing assumption in an explicit ledger.
• Classifies nontrivial steps as derived, imported, or open.
• Searches through genuinely different proof mechanisms when a problem is difficult.
• Detects equivalent-strength missing lemmas and circular reductions.
• Audits submitted proofs step by step.
• Repairs local gaps without hiding the original failure.
• Separates mathematical correctness from readability editing.
• Reports honest epistemic status: PROVED, CONDITIONAL, INCOMPLETE, REFUTED, or INCONCLUSIVE.
• Uses numerical and symbolic computation as falsification and corroboration, never as a substitute for proof.

Modes

Mode	Purpose
Prove	Construct a rigorous proof or refute the statement.
Audit	Judge a submitted proof as written and locate the first material defect.
Repair	Audit, repair the identified defect, and audit the revision as a new artifact.
Present	Improve the exposition of an accepted proof without changing its mathematics.

Arrow scales its output to the problem: routine facts receive short proofs, while difficult claims receive assumption tracking, proof obligations, and adversarial audit.

Installation

Clone the repository:

git clone https://git.celen.cloud/bogac/arrow.git
cd arrow

Codex and GPT

Codex discovers personal skills under ~/.agents/skills and follows symlinks:

mkdir -p ~/.agents/skills
ln -s "$(pwd)" ~/.agents/skills/arrow

Invoke Arrow explicitly with $arrow, or let Codex select it when a request matches its description. Restart Codex if it does not appear immediately.

Claude Code

Claude Code discovers personal skills under ~/.claude/skills:

mkdir -p ~/.claude/skills
ln -s "$(pwd)" ~/.claude/skills/arrow

Invoke it with /arrow, or let Claude select it automatically.

Claude Desktop and Claude.ai

Upload arrow-claude.zip:

1. Open Customize -> Skills.
2. Select + -> Create skill -> Upload a skill.
3. Choose arrow-claude.zip.
4. Enable Arrow in the skills list.

The Claude package contains only the portable skill instructions and references. OpenAI-specific UI metadata is excluded.

Usage

Construct a proof

Use Arrow to prove that every finite tree with at least two vertices has at least two leaves.
State all assumptions and audit the final proof.

Audit a proof

Use Arrow in audit mode.

Statement: <exact theorem>
Proof: <proof to audit>
Context: <definitions and permitted results>

Arrow classifies each nontrivial step as OK, GAP, ERROR, or UNCLEAR, then reports an artifact verdict:

• PASS
• PASS WITH CAVEATS
• FAIL
• INCONCLUSIVE

The audit verdict judges the submitted proof. It is deliberately separate from the mathematical status of the claim: a failed proof does not imply that the theorem is false.

Repair an argument

Use Arrow to audit and repair this proof. Preserve the original verdict, state whether
the repair is local or substantive, and audit the revised proof independently.

Improve exposition

Use Arrow to improve the readability of this accepted proof without changing its
mathematical content. Run a content-preservation audit afterward.

Proof discipline

Arrow enforces several safeguards that are easy to omit in ordinary prompting:

1. Freeze the contract. Fix the statement, definitions, quantifiers, domains, and edge cases.
2. Run a truth preflight. Seek small or boundary counterexamples before investing in a long proof.
3. Track assumptions. Never introduce a load-bearing condition silently.
4. Track obligations. A conclusion is not proved while an unresolved obligation supports it.
5. Audit adversarially. Check exact theorem match, theorem applicability, signs, inequalities, existence, boundary cases, and circularity.
6. Separate correctness from style. Readability edits occur only after correctness is accepted.
7. Report status honestly. If the proof fails, report the strongest rigorous result and the exact remaining gap.

Repository structure

arrow/
├── SKILL.md                         # Core portable workflow
├── references/
│   ├── analytical-checks.md         # Calculus, inequalities, probability, and computation
│   ├── audit.md                     # Audit classifications, verdicts, and report format
│   └── readability.md               # Post-verification exposition pass
├── agents/
    └── openai.yaml                  # Optional Codex/GPT UI metadata

Validation

Arrow has been forward-tested on:

• valid claims requiring proof;
• plausible but false statements requiring counterexamples;
• polished-looking proofs with hidden logical gaps;
• unsafe requests to improve the prose of an invalid proof;
• repairs that require strengthening the theorem;
• routine claims where a full audit report would be disproportionate.

Scope

Arrow is for a specific mathematical claim, derivation, or proof. It is not a formal proof assistant and does not provide a machine-checkable guarantee of correctness. For a full economics manuscript referee report, use a manuscript-review workflow rather than Arrow.

License

Arrow is released under the MIT License.