用视觉模型的类比匹配法，在不同数学领域间迁移证明策略，成功生成4个新可验证定理。
Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
- 通过跨领域战术模式匹配，将概率论的证明思路迁移到表示论。
- 10次尝试中生成4个零漏洞的Lean验证新证明，成功率40%。
- 核心是分离通用与专用部分，让通用部分在不同领域自由迁移。
Project Yanasse 提出一种方法，通过从结构差异大的数学领域转移证明策略模式（如 Lean 4 的战术调用模式），发现新定理的证明。系统分析了 Mathlib 中 27 个顶层领域的 217,133 个证明状态，计算 z 值识别源领域高频而目标领域稀有或缺失的战术；利用 GPU 加速的 NP-hard 类比匹配（在 MacBook Air 上通过 Apple MPS 后端运行），匹配源与目标证明状态；随后由 AI 推理代理语义适配而非符号替换源战术模式。第一部分研究聚焦于概率论 → 表示论，10 次尝试中生成 4 个经 Lean 验证的新证明（成功率 40%），且编译无 sorry 声明。关键发现：战术模板可分解为头（领域特定，难迁移）和修饰符（领域通用，易迁移）——例如，filter upwards 的头在表示论中因缺乏 Filter 结构而失败，但其 [LIST] 与 ω 修饰符可干净地转化为 ext1 + simp [LIST] + rfl。至关重要的是，底层匹配引擎（deep vision lib.py）完全领域无关：同一优化代码既可匹配国际象棋局面，也可匹配 Lean 证明状态，无需知晓具体领域；仅关系提取器为领域相关。
原文摘要 · Abstract (English)
Project Yanasse presents a method for discovering new proofs of theorems in one area of mathematics by transferring proof strategy patterns (e.g., Lean 4 tactic invocation patterns) from a structurally distant area. The system extracts tactic usage distributions across 27 top-level areas of Mathlib (217,133 proof states), computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area, matches source and target proof states via GPU-accelerated NP-hard analogy (running on a MacBook Air via Apple's MPS backend), and then asks an AI reasoning agent to semantically adapt--not symbol-substitute--the source tactics invocation pattern to the target theorem. In this first part of the study, the method is applied to the pair Probability -> Representation Theory, producing 4 Lean-verified new proofs out of 10 attempts (40%). The proofs compile with zero sorry declarations. The key finding is that tactic schemas decompose into a head (domain-gated, rarely transfers) and a modifier (domain-general, often transfers): filter upwards's head fails in representation theory (no Filter structure), but its [LIST] with ω modifier transfers cleanly as ext1 + simp [LIST] + rfl. Crucially, the underlying matching engine--deep vision lib.py--is entirely domain independent: the same optimization code for an NP-hard matching that matches chess positions by analogy matches Lean proof states by analogy, without knowing which domain it is processing. Only a relation extractor is domain-specific.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。