开放的 AI FOR MATH 项目

从公理出发，
让数学自己生长。

从零构建一个自主探索的数学体系。
让 AI 寻找证明，让每一步推理都经得起验证。

探索我们的理念亲手验证一个证明

+从最小的起点，走向无限的可能。

一条可追溯的推理路径FIG. 001

每一个结论，都有一条回到起点的路径。

LEM Q.E.D.OPEN SOURCE. OPEN POSSIBILITIES.↓

∅从零构建↗自主探索⊢独立验证∀开放协作

01 / 我们的理念

数学的下一章，
由推理写下。

我们相信，数学可以拥有一种新的生长方式。

Lemqo 的长期目标是构建一个完全不依赖人类数学家介入的自主数学体系。从明确的公理与推理规则开始，由 AI 提出定义、探索命题、生成证明，再由独立验证器逐步检查。

人类不必为每个结论背书，但每个人都可以检查、复现和参与体系的构建。

01∅

从零开始

把公理、规则与依赖放在明处。从最小的形式化起点构建知识，让每个结论都可追溯。

02⊢

证明可以验证

一个看似合理的答案，还需要一份明确的证明。我们要求每一步推理都能被独立检查和重放。

03∀

数学向所有人开放

开放代码、规则与讨论。数学爱好者、研究者、开发者，都可以在这里留下自己的贡献。

02 / 体系如何生长

自由探索。
严格验证。

生成证明与验证证明，是两件不同的事。
AI 可以大胆探索，结论必须回到明确的规则。

⊙01→

明确起点

公理与规则

公开体系采用的假设、定义与推理规则。

↗02→

自主探索 · 愿景

AI 寻找证明

探索命题、构造推导，输出明确的证明证书。

≡03→

记录推导

证明证书

保留每一步结论、所用规则与前提依赖。

✓04

独立检查

可重放的验证

检查每一步，并绑定到指定命题及其假设。

信任来自公开的规则和可复现的检查。

阅读验证规范

03 / 看见一个证明

别只相信结论。
检查它的每一步。

选一个命题，重放它的推导。
也可以篡改一步，看看验证器会如何回应。

⊢证明实验室在你的浏览器中运行

待验证命题

P → P

假设 P 成立，再解除这个假设，得到 P 蕴含 P。

步骤	结论	推理规则
01	P	引入假设	·
02	P → P	蕴含引入	·

篡改最后一步

查看证书 JSON+

{
  "format": "lemqo-proof-v1",
  "logic": "ipl",
  "formulas": [
    [
      "atom",
      "P"
    ],
    [
      "imp",
      0,
      0
    ]
  ],
  "steps": [
    [
      "assume",
      0
    ],
    [
      "imp_intro",
      1,
      0
    ]
  ],
  "root": 1
}

证明证书↓命题文件↓

本演示重放仓库中的命题逻辑示例。完整验证与输入检查，请使用开源验证器。

本地运行指南

04 / 从今天走向未来

一个宏大的方向。
一个可审计的起点。

自主数学体系是我们的长期愿景。
今天，Lemqo 从透明的证明验证基础开始。

当前版本 · v0.2

先把“可验证”做扎实。

命题逻辑验证内核

10 条固定的自然演绎规则，检查蕴含、合取、析取与假命题的推导。

查看规范

实验性 Lean 证书路径

限定语料中的 3 个选定主定理已有独立检查记录；这一流程仍处于实验阶段。

查看验证记录

下一步 · 研究方向

让信任的基础更坚实。

01
社区审计与独立实现
共同审阅规则与代码，探索不同语言的第二个验证器。
02
形式化规范与可靠性
研究规范、实现与健全性之间的可检查联系。
03
更丰富的数学表达
在验证基础稳固后，探索量词、定义与更完整的数学体系。

阅读完整路线图

05 / 一起从零开始

数学属于每一个
愿意追问的人。

不论你是数学爱好者、数学家、AI 研究者，还是开发者。
带着好奇心来，一起把想法变成可以验证的推理。

在 GitHub 上参与阅读贡献指南

热爱数学

运行示例，提出问题，分享你想探索的命题。

研究推理

审阅公理与规则，研究可靠性与形式化表达。

动手构建

改进验证器、工具、文档与开放协作体验。