用途
Math Schema 是一个数学研究协作技能，面向独立研究前沿数学的用户。它的目标不是替用户完成推导，而是帮助用户自己产生并认证证明。适用领域包括偏微分方程、概率论、动理学理论、湍流，以及参考案例覆盖的估计、统计力学、破产理论、随机控制和极值理论。
主要能力
- 引导用户把信念表述为可证伪的猜想，例如公式、不等式、极限或分类。
- 通过手工计算和精确 Bend 沙箱测试猜想。
- 写出完整证明链，每一步都给出依据。
- 维护 math-journal.md 日志，记录每条命题及其状态：HYPOTHESIZED、SUPPORTED、PROVEN。
- 提供提示阶梯（L1 到 L4），在用户卡住时给出最小可用提示。
- 通过 Bend 2.0.37 对有限有理数结果进行严格验证。
- 提供十六个案例文件，按主题组织，从 EWMA 到极值理论。
使用方式
技能按会话循环运行：诊断、设定目标、提出猜想、测试、证明、提交、变化。每个主题按层次推进：要点、陈述、机制、证明、形式化。用户先提出猜想，再进入机制解释。证明过程中每一步都要写出，每个等式都要有命名前提、定义或子引理作为依据。
日志格式为 Markdown，记录 COMMITTED、SUPPORTED、HYPOTHESIZED、GAP 等条目。COMMITTED 需要完整证明或干净的 python3 bend/check.py 证书。
Bend 循环使用精确算术，bend/Exact/ 提供无界二进制整数和带正分母的有符号有理数。运行严格门禁：
python3 bend/check.py
python3 -m unittest discover -s bend/tests -v
python3 bend/check.py --verdict 会用 BendTT 内核重新检查相同证明，需要 Lean v4.34.0，约两分钟。
适用场景
- 用户研究实分析、概率论、偏微分方程或物理数学，希望自己得到结果。
- 用户需要有人帮助把直觉转化为可证伪的猜想。
- 用户需要逐步检查证明，确保每一步都有依据。
- 用户需要记录研究进展，追踪每条命题的状态。
- 用户需要精确算术验证，而不是浮点近似。
限制
- 公开定律只覆盖十个原始完成的有理数命题，使用显式有限列表和假设证书。
- 原始实值目标仍未解决。
- 极限、积分和 PDE 理论需要进一步形式化，不能仅凭有理数测试就标记为 Bend 认证。
lean/目录保留历史证书和两个未完成目标，是可选的，不被 Bend 验证器导入。bend/OPEN.md记录剩余范围。- OpenAI 的独立 Lean 项目不在本次迁移范围内。
- 第三方项目
vendor/openai-navier-stokes/upstream/使用自己的工具链，不应导入学习沙箱，其上游证明声明不计入本地日志成果。 - 已发表的声明或链接的形式化本身不能把日志条目提升为 PROVEN 或 COMMITTED。
案例文件
十六个案例文件按顺序为：ewma、kalman、kelly、gibbs、large-deviations、gaertner-ellis、heat-kernel、mixing、max-principle、burgers、black-scholes、merton、h-theorem、kolmogorov、navier-stokes、extremes。前五个在 Q 上构建对数、倾斜和熵工具包。接下来三个把它们用于阈值和谱。PDE 对对比平滑与激波。金融对应用两个工具包。H 定理和 Kolmogorov 运行物理。Navier-Stokes 案例随后进行能量界反例和外部证明审计。极值关闭尾部线程。根据日志诊断用户水平后，从先决条件已 COMMITTED 的文件开始。