Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add voidful/academic-skills --skill proof-writergit clone --depth 1 https://github.com/voidful/academic-skillsWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/voidful/academic-skills/proof-writer)<a href="https://agentmods.dev/skills/voidful/academic-skills/proof-writer"><img src="https://agentmods.dev/badge/skills/voidful/academic-skills/proof-writer.svg" alt="Measured on agentmods" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00149 | $0.04508 |
| Opus 5 | $0.00075 | $0.02254 |
| Sonnet 5 | $0.00030 | $0.00902 |
| Haiku 4.5 | $0.00015 | $0.00451 |
Grade A, and why
proof-writer scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 8d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 449 lines — stays where its author put it; the contents beside it link to each section on GitHub.
proof-writer：數學證明撰寫技能
概述
本技能專注於學術論文中的數學證明撰寫。涵蓋從主張提取、策略選擇到完整 LaTeX 排版的端對端工作流程。所有解釋使用繁體中文，數學表達式與 LaTeX 代碼使用英文。
流程總覽
證明撰寫分為五個階段，依序執行：
主張提取 → 文獻掃描 → 策略選擇 → 逐步推導 → LaTeX 排版
每個階段有明確的輸入、輸出與品質檢查點。以下逐一說明。
第一階段：主張提取
目的
從論文草稿或用戶輸入中，精確提取需要證明的數學主張。主張必須是形式化的命題， 具備明確的前提條件與結論。
步驟
- 辨識主張類型：判斷是定理 (Theorem)、引理 (Lemma)、推論 (Corollary)、 命題 (Proposition)，還是聲明 (Claim)。
- 提取前提條件：列出所有假設、約束條件與適用範圍。
- 提取結論：明確寫出要證明的等式、不等式或性質。
- 符號確認：確認所有符號的定義與範圍，參照 符號慣例。
- 形式化陳述：將主張寫成標準的數學陳述格式。
輸出格式
主張類型：[Theorem | Lemma | Corollary | Proposition | Claim]
前提條件：
- 條件 1
- 條件 2
- ...
結論：[形式化的數學陳述]
相關符號：[符號清單及定義]
常見問題
- 前提條件不完整：回頭檢查論文中的假設段落。
- 符號未定義：查閱論文的 notation section 或向用戶確認。
- 主張過於模糊：要求用戶提供更精確的形式化陳述。
品質檢查
- 主張是否為可判定的數學命題？
- 所有符號是否已定義？
- 前提條件是否足以推導結論？
- 主張類型是否正確分類？
第二階段：文獻掃描
目的
查找與主張相關的已知定理、引理和結果，為證明建立基礎。這一步決定了我們可以 「站在哪些巨人的肩膀上」。
步驟
- 關鍵詞提取：從主張中提取數學關鍵詞（如 convergence、bound、 concentration inequality 等）。
- 定理匹配：在已知定理庫中搜索相關結果，參照 定理連結方法。
- 相關性評估：評估每個找到的定理與當前主張的相關程度。
- 依賴關係建立：確定哪些定理可以直接使用，哪些需要適度修改。
- 缺口分析：找出已知結果與目標主張之間的差距。
常用定理來源
- 論文自身前文已證明的引理
- 論文引用的參考文獻
- 領域內的經典結果（如 Cauchy-Schwarz, Jensen's inequality 等）
- 標準教科書中的基礎定理
輸出格式
相關定理：
1. [定理名稱] — [簡述] — 相關度：[高|中|低]
2. ...
可直接引用：[定理列表]
需要修改後使用：[定理列表及修改方向]
證明缺口：[需要自行推導的部分]
品質檢查
- 是否遺漏了重要的已知結果？
- 引用的定理前提條件是否滿足？
- 定理的版本是否正確（有些定理有多個變體）？
第三階段：策略選擇
目的
根據主張的結構和可用的已知結果，選擇最合適的證明策略。策略的選擇直接影響 證明的清晰度和長度。
可用策略
本技能支援以下八種證明策略，每種策略的詳細說明見 證明策略參考。
1. 直接證明 (Direct Proof)
從前提條件出發，通過一系列邏輯推導直接到達結論。適用於結構清晰、推導路徑 明確的主張。
適用場景：等式證明、不等式推導、集合包含關係。
2. 反證法 (Proof by Contradiction)
假設結論不成立，推導出矛盾。適用於直接證明困難或結論為否定形式的主張。
適用場景：存在性的否定、唯一性證明、不可能性結果。
3. 數學歸納法 (Mathematical Induction)
對自然數或可良序化的結構進行歸納。包括弱歸納、強歸納和結構歸納。
適用場景：遞迴結構、序列性質、離散數學中的命題。
What ships with it
4 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 8d ago First seen · 449 lines · 149 tokens per session scan A 3ee63ffd1ac7
proof-writer is a skill published in the GitHub repository voidful/academic-skills (126 stars, last pushed 5mo ago), licensed MIT. It adds 149 tokens to every session and 4,508 once invoked, about $0.0007 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
instrument-data-to-allotrope
Convert laboratory instrument output files (PDF, CSV, Excel, TXT) to Allotrope Simple Model (ASM) JSON format or flattened 2D CSV. Use this skill when scientists need to standardize instrument data for LIMS systems, data lakes, or downstream analysis. Supports auto-detection of instrument types. Outputs include full…
exploratory-data-analysis
Perform bounded, local exploratory analysis of explicitly supported scientific files. Use for redacted CSV/TSV/JSON profiles; optional NumPy, HDF5, FASTA/FASTQ, and basic image metadata inspection; missingness/leakage audits; outlier and transformation sensitivity; and rigorous EDA report scaffolds. Other domain…
matlab
Build, review, migrate, and safely plan MATLAB or GNU Octave numerical workflows, including arrays, tabular/time data, tests, projects, graphics, MAT files, and explicit Python interoperability.
phylogenetics
Build and analyze phylogenetic trees using MAFFT (multiple alignment), IQ-TREE 2 (maximum likelihood), and FastTree (fast NJ/ML). Visualize with ETE3 or FigTree. For evolutionary analysis, microbial genomics, viral phylodynamics, protein family analysis, and molecular clock studies.
research-engineer
An uncompromising Academic Research Engineer. Operates with absolute scientific rigor, objective criticism, and zero flair. Focuses on theoretical correctness, formal verification, and optimal implementation across any required technology.
mapping-to-snomed
Maps clinical concept spans extracted by OpenMed to SNOMED CT concepts through a USER-SUPPLIED terminology server (the user's own Ontoserver, Snowstorm, or UMLS/UTS), never a bundled vocabulary. Use when the user wants to code findings, disorders, procedures, body structures, or substances to SNOMED CT, run an ECL…