theory-proof-sketcher

证明草图绘制器

在尝试完整形式化之前，先将直觉转化为可检验的证明框架。 目标不是伪装成完整证明。
目标是尽早揭示结构、假设和未解决的缺口。

流程

1. 精确陈述目标命题

用数学上可检验的形式写出命题。 包括：

• 量化变量
• 定义域限制
• 渐近范围（如相关）
• 概率限定条件
• 精确结论 避免使用：
• “表现得像”
• “大致”
• “应该收敛”
• “稳定”
• “效果不错” 不佳：

该随机游走很快达到混合。 更好： 对任意连通非二分图 (G)，惰性随机游走满足 [ |P^t(v,\cdot)-\pi|_{\mathrm{TV}} \le \varepsilon ] 对所有 [ t \ge C \gamma^{-1}\log(n/\varepsilon), ] 其中 (\gamma) 是谱隙。

---

2. 定义对象、符号和假设

明确给出以下内容的定义：

• 空间
• 算子
• 矩阵
• 测度
• 范数
• 图族
• 正则性假设
• 独立性假设
• 渐近假设 之后用到的每个符号都必须事先定义。 区分：
• 通常假设
• 临时假设
• 猜想性假设 示例：

Assumption A1.
G is connected, undirected, and non-bipartite.
Assumption A2.
The transition matrix P is reversible with stationary distribution π.

⸻

3. Decompose the Argument

Split the proof into:

* lemmas
* propositions
* reduction steps
* intermediate estimates

Prefer:

Main theorem
├── Lemma 1: spectral estimate
├── Lemma 2: concentration bound
└── Lemma 3: coupling argument

over a single monolithic proof sketch.

Each sub-result should have:

* explicit input assumptions
* explicit output statement
* clear dependency chain

⸻

4. For Each Stage, Specify the Proof Skeleton

For every lemma or stage, include the following fields.

Goal

State exactly what must be shown.

Candidate Technique

Examples:

* spectral decomposition
* coupling
* martingale inequality
* compactness argument
* variational characterization
* induction
* contradiction
* perturbation analysis
* concentration inequality
* optimal transport duality

Dependencies

List:

* previous lemmas
* external theorems
* hidden assumptions
* required estimates

Likely Weak Points

Identify:

* unjustified limit interchange
* missing regularity
* non-uniform constants
* dependence assumptions
* dimension blow-up
* unproved concentration
* unjustified approximation

Do not hide uncertainty.

⸻

5. Mark Gaps Explicitly

Any unresolved step must be labeled as a gap.

Use labels such as:

GAP 1.
Need a uniform lower bound on conductance.
GAP 2.
The coupling argument only works for reversible chains.
GAP 3.
The concentration step currently assumes sub-Gaussian tails.

Never present an unproved step as established fact.

Separate:

* proved step
* heuristic argument
* conjectural extension

⸻

6. Compare Competing Proof Strategies

If multiple approaches exist, compare them briefly.

Example:

Strategy A: Spectral method
- cleaner constants
- requires reversibility
Strategy B: Coupling method
- more probabilistic
- may extend to directed graphs
- weaker quantitative bounds

Do not expand every branch fully.
Focus on the most plausible route.

⸻

7. End with the Minimal Next Action

Conclude with the smallest concrete step needed to advance the proof.

Good:

Next step:
Prove that the random-walk refinement operator is contractive under the chosen diffusion metric.

Bad:

Next step:
Finish the proof.

⸻

Output Format

Use the following structure.

# Target Claim
...
# Assumptions and Definitions
...
# Proof Structure
## Lemma 1
### Goal
...
### Technique
...
### Dependencies
...
### Weak Points
...
## Lemma 2
...
# Gaps
...
# Alternative Strategies
...
# Minimal Next Step
...

⸻

Rules

* Prefer explicit assumptions over implicit context.
* Prefer incomplete honesty over fake rigor.
* Distinguish theorem, heuristic, and conjecture.
* Avoid narrative filler.
* Avoid undefined notation.
* Avoid skipping dependency chains.
* Do not claim a result is “obvious” without stating why.
* Do not compress multiple logical steps into one sentence.
* Keep the scaffold minimal but structurally rigorous.