#Find a path

##原则

充分利用模型本身能力，这个 agent/harness 的重点在于控制流程和上下文管理。

现在模型的短板似乎是长上下文后注意力涣散，产生幻觉。对于中间过程的 lemma propositions 等，在整体思考时应该只有 statement 进入上下文，而不包括 proof. 命题的颗粒度应该有不同等级，在不同等级下用独立的 subagent

关键设计：

• 递归的分级思维图，节点是 statement
• 代码风格的知识记录形式

##path

仿照寻路算法和迷宫算法

数学推理是一个巨大的图，从起点到终点，每个 statement 是一个地点，一个 imply 是两个地点的道路。 区别是：

• 是在发现道路，而不是一开始就有完整地图，在各个局部类似迷宫
• 起点和终点不唯一，需要多个出发点，到达多个终点
• 最终终点并不清楚，也许在搞完了才知道结果是什么

人类研究数学的一些方式

• 类似寻路和剪枝过程，探索多个思路，某些思路可能性大，所以深入一些
• 有时可能先有大框架，类似于伪代码的巨大的思路直觉，并且不唯一；在思路图里有一些中间结论作为节点
• 在这些的中间结论上，加细推导内容。这会产生一个类似分型或递归的结构，产生不同级别的节点，和不同尺度的图
• 双向探索，从节点看，它能推出什么，它需要什么
• 某个节点“附近”完成后，整体作为黑箱。

##known results

对已知内容的处理，怎样封装各个级别的节点，以什么文件格式供模型使用？ 关键点：

• statement 和 proof 分离
• 某个节点对更细节点的依赖关系
• 合适的黑箱程度

##co-mathematician

人与 AI 分工的界限：在什么尺度下需要人工介入，调控思路和人工验证结果 也许依赖于知识文件格式，分析各级结论的可信度，类似 HINT, WARNING, ERROR 一样对人类做出提醒，由人类介入。 在协同工作时设置中断或提醒的阈值，设置选择人工校验还是新会话/模型/提示词/上下文的机器校验

##Code

当前大模型的主要目的还是编程，没有对数学做特化。如何让这个 harness 最大程度使用模型在编程方面的能力？如何让做数学研究这件事更像写代码，但不是 lean 那样的形式语言？

用类似 C 语言那样的形式去陈述。一些数学论文的格式类似

# introduction
# Prelimary and Notation
# tools
# proof of main theoremcopy

最后一节如同 C 语言的main函数，它使用前面的一堆函数。引用其他论文如同使用各种头文件，Notation如同 Define 宏 用恰当的格式去封装数学命题，或者上述思路图中的节点，让模型像处理代码一样处理数学证明。甚至也许可以开发配套的 Treesitter, LSP 等