I · Learning Retreat
学习型回退
失败不是简单重试。lessons.md 累积死路、已验证子结论、陷阱与修订理解——只增不减，下一轮显式引用，从更高认知起点重来。
Workflow Loop
工作流是循环而非单向管道：形式化编译失败时进入反思（Reflection），更新 lessons，再退回理解、探索或策略等更早阶段——迭代上限通常为 8 轮。
每个阶段有独立 prompt 与产出物；进入阶段前应先读对应指引，并通读当次运行的 lessons.md。
澄清命题、符号与背景——先理解问题，不急于证明。
结构探索、手算小例子，建立对结论的直觉。
至少三条不同视角的路径规划，并与 lessons 对照。
完整自然语言证明草图，作为形式化的蓝图。
翻译为 Lean4，对接 Mathlib；真实编译，禁止臆断成功。
失败时追加 lessons，声明下一轮 Mode，选择回退深度。
编译与公理审计通过后：复盘、归档至 Problems/，沉淀可复用引理。
Three Pillars
I · Learning Retreat
失败不是简单重试。lessons.md 累积死路、已验证子结论、陷阱与修订理解——只增不减，下一轮显式引用，从更高认知起点重来。
II · Structured Planning
Strategy 阶段产出固定 schema：问题定位、≥3 条不同视角路径、路径选择与 lessons 对照。禁止视角重复凑数，创新度需诚实标注。
III · Adaptive Temperature
Mode A 保守（1–2 轮）· Mode B 探索（3–4 轮）· Mode C 重构（5+ 轮）。可提前升级模式，不可降级；Reflection 需声明下一轮 Mode。
Trust, not vibes
编译通过 ≠ 证明有效。 需拦截 axiom、sorry 与非常规公理依赖；必要时进入引理补全：先确认 Mathlib 确无，再建 Dependency DAG（深度 ≤4），自底向上证明 private lemma。
lean_helpers /
Knowledge Base
资料经 MinerU 与索引管线生成 outline.json 与 methodology.md。 仅在 Mode A 的策略阶段查询；Mode B/C 不调用，以免保守检索压制探索。
kb_helpers: import_sources · search_outline · search_methodology · fetch_section
knowledge_base/
raw/ ← 原始 PDF / DOCX / MD sources/ ← 统一 Markdown outlines/ ← outline.json（精确行号） methodologies/ ← methodology.md（怎么做） master_index.json · master_topics.md
Workspace
运行时写入 ~/math-agent-workspace/（Scratch.lean、runs/、Problems/）；Skill 本体轻量驻留在 skills 目录，二者分离。
Contact & Collaboration
我们欢迎与您在形式化数学与 AI 证明智能体方向开展交流。若您希望与我们共创调优，或申请产品与管线试用，请通过下方邮箱与我们联系
本产品仍在不断优化中，正在适配更多数学研究分支。如果您对与围绕形式化数学、Lean4 / Mathlib、定理证明智能体、Math Thinking Flow方法论 等主题感兴趣或有所见解，或希望本模型对您所研究的数学课题角度进行专属调优，欢迎您与我在邮件中沟通。
若您希望体验 GaussAI / Math Thinking Flow 管线、了解开发过程内测与部署、或讨论定制化知识库接入与运维方式，欢迎来信。请在邮件中注明机构或个人名称、大致使用场景（如教学、科研课题、内部工具）、期望试用周期与联系人方式；我们将在评估需求后与您沟通下一步安排。
从结绳计数到算筹再到计算机
我们将生产力一步步解放，也诞生了一个个奇迹
可今天，当人工智能让我们可窥见彻底摆脱计数者的身份、
平静地交付那些我们曾经引以为傲的推导的未来时
无数人却不寒而栗
硅基智能能以相较于人成千上百万的速度淌过每一条河。
速度很快，快到我们窒息
当我们在这里反复确认人的生态位时，我们就已经在向技术低头了。
未来如何，你我皆不知，可我们知道：
技术，它只是一面镜子，照见我们真正擅长的事。
它丈量星辰的数量，而我们，负责为星空命名。
北航的玉兰花开了，开得那么美。
檐下的雨，一滴一滴，落在花瓣上，落在石阶的同一个凹痕里。
石阶不说话，只是慢慢变薄。