76.2 万条结构化定理/命题/证明，7 种类型，1851 万条依赖关系。

不是简单的定理列表，而是结构化的定理知识图谱，定理间有明确的依赖关系。

1)    7 种类型：公理、定义、定理、引理、推论、猜想、定律，覆盖数学定理的全类型。

2)    1851 万条依赖关系：定理间有明确的依赖关系，形成完整的知识图谱。

3)    77.2 万条证明步骤：每个定理的证明都有详细的步骤记录。

4)    419 万条逻辑推理步骤：完整的逻辑推理过程记录，可追溯每一步推理。

5)    结构化存储：定理的条件、结论、证明均结构化存储，支持精确查询。

138 万道数学题，覆盖 15 个学科子类，6 种题目类型。

不是简单的题目文本，而是条件、目标、路径均结构化存储的智能题库。

1)    15 个学科子类：代数、几何、数论、组合、微积分、概率、逻辑、竞赛、训练等。

2)    6 种题目类型：选择题、填空题、计算题、证明题、应用题、开放题。

3)    结构化存储：条件、目标、路径均结构化存储，支持智能组卷和推荐。

4)    中英双语：所有题目中英文双语，满足国际化需求。

5)    难度标注：每道题有难度标注，支持按难度筛选和推荐。

211 万条逻辑公式，4 种渲染格式，公式不存文本，从数学结构组合渲染。

不是存储公式的文本表示，而是存储数学结构，按需渲染为不同格式。

1)    Unicode 渲染：渲染为 Unicode 字符，适合控制台和纯文本环境。

2)    LaTeX 渲染：渲染为 LaTeX 格式，适合 KaTeX/MathJax 等渲染引擎。

3)    OpenMath 内容树：渲染为 OpenMath 内容树，支持双向精确映射。

4)    中文自然语言：渲染为中文自然语言描述，适合非专业用户理解。

5)    结构化存储：公式不存文本，从数学结构组合渲染，确保数学正确性。

5 种意图识别，中英文双语，零幻觉设计，确定性知识查询。

不是让 LLM 自由生成答案，而是从知识库中精确查询，零幻觉。

1)    5 种意图识别：prove（证明）、find（求解）、explain（解释）、verify（验证）、render（渲染）。

2)    中英文双语：支持中文和英文自然语言提问。

3)    零幻觉设计：确定性知识查询加精确实体解析，不依赖 LLM 生成答案。

4)    三区布局：候选区、证明步骤区、验证状态区，清晰展示问答结果。

5)    DeepSeek SSE 协议兼容：支持 DeepSeek 的 SSE 流式输出协议。

5 种伪证明标志检测，三态验证结果，反例支持。

不是简单的接受或拒绝，而是多维度验证证明的正确性。

1)    5 种伪证明标志：sorry、admit、abort、unreachable、unresolved_metavar，检测伪证明。

2)    三态验证结果：passed（通过）、unverified（未验证）、failed（失败），精确表达验证状态。

3)    反例支持：验证失败时可提供反例，帮助理解证明的错误。

4)    逐步验证：可逐步验证证明的每一步，定位错误位置。

知识掌握度评估、答题记录与解题步骤追踪、智能推荐。

面向教学场景，提供完整的学习训练能力。

1)    知识掌握度评估：基于 IRT 和贝叶斯模型评估学生的知识掌握度。

2)    答题记录：记录学生的答题记录，支持学习过程分析。

3)    解题步骤追踪：8 种步骤类型，追踪学生的解题过程，识别学习困难。

4)    智能推荐：4 种推荐类型，根据学生情况推荐合适的题目和学习路径。

9 个 LLM 供应商，7 个数学专用代理，4 种数学工具，Odoo 原生集成。

数学知识引擎与 AI 代理深度集成，提供智能化的数学服务。

1)    9 个 LLM 供应商：支持 9 个 LLM 供应商，灵活选择。

2)    7 个数学专用代理：7 个针对数学场景优化的 AI 代理。

3)    4 种数学工具：4 种数学工具注册为 function calling，AI 代理可调用。

4)    Odoo 原生集成：与 Odoo 系统原生集成，无需额外部署。