Yanasse：从深度视觉的类比中发现新证明（第一部分）

本项目提出一种方法，通过将结构遥远领域的证明策略模式（如 Lean 4 战术调用）迁移至目标领域，以发现新的数学定理证明。系统提取 Mathlib 中各领域的战术分布，利用 GPU 加速的 NP 难类比匹配源与目标证明状态，并驱动 AI 推理代理进行语义适配而非符号替换。在概率论到表示论的迁移实验中，成功生成了四个经 Lean 验证的新证明。关键发现是战术模式可分解为特定领域的“头部”和通用的“修饰符”，且底层匹配引擎完全独立于领域。