文章总结： 本文作者计划开发一个面向数论题的严谨推理程序，核心思想是将启发式探索与形式化验证分离。程序旨在通过严格规则库确保每一步推理可追溯、可验证，从而减少AI幻觉并生成可信证明链。作者主张先从小范围题型（如整除、同余题）入手，采用分层架构（表达层、推理层、搜索/启发层），初期以人工设计启发策略为主，优先实现可验证再追求更聪明。 综合评分： 0 文章分类： 其他

---

我准备公开做一件事：做一个面向数论题的“严谨推理”程序

原创

Uysieot Uysieot

简单读写

2026年4月20日 13:04 四川

在小说阅读器读本章

去阅读

我准备公开做一件事：做一个面向数论题的“严谨推理”程序

这篇文章，不是招商，不是招募，也不是喊口号。

就是想认真说一件我准备慢慢做的事。

我想做一个程序。更准确地说，是想做一个面向部分数论题的、用严格推理来完成证明的程序。

它不靠“看起来像会了”的语言，不靠一段顺滑但中间可能跳步的话术，而是尽量把每一步都落到可以检查、可以追溯、可以回看的推理上。

这件事，我不怕别人知道。

谁做出来了，都是在推进数学、推进数学教育、推进数学工具本身的一步。不是说非要谁独占，非要谁藏着掖着，非要谁先立一个山头。这个方向如果真的能往前走，不管最后是谁做得更完整、谁做得更漂亮、谁做得更早，都算是在往前推。那就是好事。

所以我决定把这件事公开说出来。

我会慢慢做。可能一年，两年，谁知道呢。也可能中间会绕路，会推翻，会重来。但我准备开始做，而且会尽量持续地记录。

一、我为什么会想做这个方向

这些年大家都看到了，AI 在很多地方都很厉害。

会写，会说，会总结，会模仿人的表达，很多时候甚至能把话说得比人还像那么回事。

但数学这个地方，有一个很根本的问题：

“像对的”不等于“真的是对的”。

一段数学解答，语言顺不顺，表述漂不漂亮，和它是不是真的成立，是两回事。

尤其是证明题。中间只要偷偷跳一步，或者默认了一个没有证明的结论，或者把某个对象的条件看错了，整篇东西看起来再顺，也可能是假的。

这也是为什么，很多人一边觉得 AI 很强，一边又总觉得它做数学不太让人放心。不是它完全不会，而是它很容易在“最需要严谨”的地方，给你来一点看起来不明显、但其实很关键的幻觉。

我自己越来越觉得，真正更有希望的一条路，不是让 AI 直接在那里一本正经地“表演会证明”，而是：

让它负责提供想法，让系统负责严格验证。

也就是说，启发可以不那么死，搜索可以不那么死，猜测可以不那么死；但最后被接受的东西，必须是一步一步能查回去的。

这个思路对我触动很大。

因为人做数学，其实很多时候也是这样的。

先有感觉：这里可能要取模，那里可能要设一个最大公因数，这里可能要看阶，那里可能要上 LTE，或者可能先拆因式。

这些“想到什么方向”本身，带有很强的经验性、直觉性、启发性。

但一旦你真正开始写证明，你还是得老老实实把逻辑落下来。每一步从哪里来，为什么能用，前提是什么，结论是什么，都要能说清楚。

所以我想做的，不是一个“会聊天的数论 AI”。

我更想做的是一个：

能把启发式想法和严格证明分开处理的数论程序。

二、这个事情的核心，不是“更会说”，而是“更能验”

我想做的这类程序，核心不是让机器直接输出一大段自然语言，然后希望它碰巧是对的。

核心是：

1. 先把题目翻译成机器可处理的形式；
2. 再由系统去做规则层面的严谨推理；
3. 如果中间需要搜索思路，就把“搜索”控制在候选生成层；
4. 最后只有那些真的能被规则系统推出的东西，才算数。

这和很多人想象里的“AI 自动做题”不太一样。

它不是靠最后那段话像不像标准答案。

它依赖的是：

每一个结论，是否真的能由前面的条件和规则推出。

这件事一旦做起来，有几个非常重要的意义。

第一，能大幅减少幻觉

不是说从此完全没有错误，而是说，错误更容易被限制在“候选阶段”，而不是“最终证明阶段”。

比如系统可以尝试很多方向：

• 试模 2
• 试模 4
• 试模 8
• 看能不能拆因式
• 看能不能引入 gcd
• 看能不能用同余改写整除

但试完以后，只有那些能真的走通的，才会被保留下来。走不通的，就丢掉。

这和直接让模型一本正经输出一篇解答，风险是很不一样的。

第二，能留下可追溯的证明链

这点我觉得非常重要。

很多时候，不只是“对不对”的问题，而是“你怎么得到的”。

如果一个系统最后能把证明链完整保留下来，那么它不只是一个“答案生成器”，它还是一个可回放、可分析、可教学的工具。

学生能看，老师能看，研究者能看，做系统的人自己也能看。

第三，它更接近真正可积累的数学工具

如果只是自然语言输出，很多东西其实不可积累。

今天这道题这么说，明天那道题那么说，表面上都挺像回事，但底层没有统一结构。

而如果你是规则、对象、状态、依赖关系这些东西都搭起来了，那每推进一点，都是实打实的积累。

规则库在增长，题型覆盖在增长，搜索策略在增长，证明表达在增长。

这种东西才有“慢慢做大”的可能。

三、为什么我想先从数论做，而不是做一个“全能数学程序”

因为我很清楚，数学太大了。

你要说“做一个能自动证明数学题的系统”，这句话太大，太虚，也太容易沦为口号。

我不想这么说。

我更想做的是：

先做一部分，先做能落地的一部分，先做我自己真正关心、也确实有竞赛和教学价值的一部分。

而数论，尤其是竞赛初等数论，有一个很有意思的特点：

它一方面非常依赖灵感； 另一方面，它又有大量非常适合形式化处理的局部规则。

比如：

• 整除
• 同余
• 奇偶性
• 最大公因数
• 模若干小数的讨论
• 质因子分解
• 阶
• 赋值
• 一些典型恒等变形

这些东西，本来就有很强的“规则性”。

难点往往不在于规则本身不存在，而在于：

什么时候该用哪条规则，什么时候该换视角，什么时候该引入中间对象。

这恰恰就很适合做成“启发 + 验证”的结构。

也就是说：

• 规则系统负责保证每步合法；
• 搜索系统负责提出可能值得尝试的方向；
• 最后留下来的，是能真正闭合的证明链。

我觉得这条路是可以走的。

当然，我也不天真。我知道数论并不好做。

因为和几何不同，数论里的“辅助构造”不是画一条线、补一个点这么直观的东西。数论里的辅助对象，可能是：

• 取一个模数
• 设一个最大公因数
• 引入一个质因子
• 取一个 p 进赋值
• 定义一个阶
• 换一个等价表达
• 把式子因式分解
• 把结论拆成若干子结论

这些动作比几何中的辅助线更抽象，空间也更散。

所以我不会把这件事说得很轻松。

但正因为难，所以值得慢慢做。

四、我准备怎么做：不是一口吃成胖子，而是分层推进

我现在的想法非常明确：

第一阶段，不做“通用数论证明器”，只做少数题型。

先从最适合形式化的一批题开始，比如：

• 整除题
• 同余题
• 用模论或奇偶性做反证的题

这一阶段的目标，不是通杀，而是把最基本的框架搭起来。

这个框架大概包含几层：

1. 表达层

先把题目里的对象和结论翻译成统一形式。

比如把“a 整除 b”“a 与 b 模 m 同余”“gcd(a,b)=d”这些都变成统一的内部表示。

这样系统处理的就不是一句中文或一段自然语言，而是一套结构化对象。

2. 推理层

把一些数论里常见的合法推理做成规则。

比如：

• 同余可以转整除
• 整除可以推出线性组合仍被整除
• 互素和 gcd 之间如何转换
• 某些同余如何传递
• 某些奇偶性如何传播

这一层是整个系统“严谨性”的底座。

这一层放的，是严格规则库。

也就是说，系统不是靠“感觉差不多对”，而是靠一条一条合法规则往前推。

每一步都必须能说清楚：

• 前提是什么
• 用的是哪条规则
• 推出了什么新结论

如果这一步说不清楚，那就不能算。

比如在第一期里，我会优先考虑把下面这些规则逐步整理进去：

Coprime(a,b) => gcd(a,b)=1gcd(a,b)=d => d|a and d|ba≡b (mod m), b≡c (mod m) => a≡c (mod m)a≡b (mod m) => m | (a-b)a|b, a|c => a | (xb+yc)gcd(a,m)=1 => a has inverse mod mord_m(a)=r => a^r ≡ 1 (mod m)a≡b (mod m) => a^k≡b^k (mod m)

这些只是例子，不是说第一期就把所有东西一口气塞完。

但思路就是这样：

把数论里那些本来就有明确前提和明确结论的推理，尽量整理成机器可调用的规则。

从结构上看，这一层其实就相当于几何系统里的 rules.txt。

当然，数论里的规则和几何也不完全一样。

几何里很多关系比较“图形化”，而数论里有很多规则会带来表达式膨胀，所以这里还得再分一下：

第一类是基础闭包规则。

这种规则适合自动跑，因为它们相对稳定、相对局部、不会一下把状态炸开。

比如：

• 同余的传递
• 整除与同余的互换
• gcd 推出整除
• 奇偶性的基本传播

第二类是生成性规则。

这种规则虽然合法，但不能无脑全展开，否则搜索空间会很快失控。

比如：

• a|b, a|c => a | (xb+yc) 里，x,y 其实有很多种可能
• a≡b (mod m) => a^k≡b^k (mod m) 里的 k 也不是随便乱取
• 某些因式分解、引入阶、引入赋值，也都会显著扩大搜索空间

所以这部分不能只是“有规则就全用”，而要配合后面的启发层。

换句话说，推理层负责的是：

只要某一步被采用，它就必须是真的。

至于“现在该不该采用这一步”，那是下一层的事情。

3. 搜索 / 启发层

这一层不直接“证明”，它只负责猜方向。

也就是说，它不负责拍板“这步成立”，而是负责提出一些候选动作，再把这些动作交给规则系统去验证。

比如面对一道题，它可能会猜：

• 该取哪个模
• 该先分奇偶，还是先分质因子
• 该不该引入 v_p
• 该不该设 d=gcd(a,b)
• 该不该把整除转成同余
• 该不该先因式分解
• 该不该用 LTE
• 该不该引入阶
• 该不该考虑欧拉定理
• 该不该考虑 CRT
• 该不该走无限递降
• 该不该往 Vieta jumping 的方向试

这些动作，本质上都不是“证明已经完成”，而只是“这条路也许值得试一试”。

这也是我为什么一直强调，要把“启发”和“验证”分开。

因为很多数论题真正难的地方，不是某条规则本身不会，而是：

你到底什么时候该想到用它。

比如同样是一个整除题，有的题适合：

• 先拆成若干个小模
• 先看奇偶性
• 先看质因子
• 先看表达式是否能拆成 a^n-b^n
• 先试一个小模把它直接打死

而有的题，一上来去试模，可能就会越试越乱；这时也许更应该先设 gcd，或者先引入某个素数的赋值。

所以搜索 / 启发层要做的，不是代替证明，而是帮系统决定：

下一步更值得试什么。

这一层在第一期里，我并不准备一开始就做得特别花哨。

更现实的路线，还是先从人工设计的启发开始。

比如：

• 如果目标是 d | expr，优先尝试把目标拆成若干互素因子的整除目标
• 如果目标看起来适合转同余，就先转成 expr ≡ 0 (mod d)
• 如果目标是否定命题，优先试模 2、3、4、8、9 这些常见小模
• 如果式子里有高次幂，优先检查是否存在小模循环、费马/欧拉、阶
• 如果式子长得像 a^n-b^n 或 a^n+b^n，优先看因式分解、LTE 或 valuation
• 如果两边反复出现公共结构，优先考虑引入 gcd

等到底层表达和规则系统打稳了，再考虑是不是要让更强的模型来给这些动作排序。

所以在我的设想里，搜索 / 启发层并不是“会说一篇证明”的层，而更像一个：

动作提议器、方向筛选器、候选生成器。

它可以不那么死，可以带一点经验感；但它提出来的每一步，最后都还是得回到推理层，接受严格检查。

4. 状态层

系统每得到一个新结论，都要记下来：

• 它是什么
• 它从哪几步来的
• 用了哪条规则

这样最后才能往回追，输出证明，而不是只告诉你“我知道这题对”。

5. 启发层

这部分才是“像人”的地方。

比如面对一道题，系统可能会尝试：

• 先把整除转同余
• 先把目标拆成若干个小目标
• 先试几个常见模数
• 先看能不能因式分解
• 先引入一个 gcd

这一层一开始甚至不一定需要大模型。

我觉得第一版，完全可以先用人工设计的启发策略。先把系统做起来，先让它能在一个小范围内稳定工作。

等到底层表达、规则系统、证明追踪这些东西都成熟了，再考虑是否引入更强的模型来做动作排序或候选建议。

这也是我现在比较认同的一点：

先把“可验证”做好，再去追求“更聪明”。

五、第一期我准备怎么走：先做一个小而硬的版本

我现在对“第一期做什么”其实想得比较清楚。

我不会一上来就做一个号称“通用数论自动证明”的大系统。

这种说法听起来很厉害，实际上大概率是在给自己挖坑。

我更愿意先做一个小而硬的版本：

先只处理一部分很明确的题型，先把底层框架做对。

第一期我准备优先碰的，是下面这几类：

• 整除题
• 同余题
• 用奇偶性、模若干小数做反证的题

为什么先选这些？

因为这几类题有两个特点。

第一，它们本身就很适合形式化。

比如“a|b”、“a ≡ b (mod m)”这种东西，本来就比很多别的数学对象更容易用统一语言表示。

第二，它们虽然不算整个数论里最华丽的部分，但非常基础，也非常常见。很多后面的东西，最后还是要落回整除、同余、奇偶性、gcd 这些地方。

所以先把这一层做稳，后面才有可能往上长。

第一期大致会分成几层：

1. 先统一表达

先把题目里的基本对象，翻译成机器能稳定处理的形式。

比如：

• 整除
• 同余
• 相等
• 奇偶
• gcd
• 互素

这些都要先有统一表示。

这件事看起来不显眼，但其实是最基础的。因为如果底层表示都不统一，后面规则、搜索、证明追踪都会很乱。

2. 先做基础规则库

第一期不求大而全，只先放那些最常用、最扎实、最容易反复调用的规则。

比如：

• 同余和整除之间如何互相转化
• 整除在加减乘中的传播
• 奇偶性的基本规则
• gcd 和互素的一部分基础关系
• 一些常见的小模讨论

这一步相当于给系统打地基。

3. 先做“证明链可追溯”

这一点我非常在意。

系统每得到一个新结论，都不能只是说“我知道了”。它要记住：

• 这个结论是什么
• 它是从哪几步来的
• 用了哪条规则

这样最后才不是只给一个结果，而是能把整条推理链回放出来。

这也是我为什么一直强调“严谨”的原因。不是嘴上说严谨，而是系统结构上就要逼自己严谨。

4. 启发先不用太花哨

第一期我甚至不准备一开始就把大模型强行塞进来。

因为我越来越觉得，第一阶段最重要的，不是“让它看起来更聪明”，而是“让它真的站得住”。

所以第一期更现实的做法是：

先用人工设计的启发策略。

比如遇到一个整除目标，系统优先尝试：

• 把目标拆成几个更小的整除目标
• 把整除转同余
• 试一些常见模数
• 看能不能因式分解
• 看是否有明显的奇偶性结构

这些东西，先手工设计，并不丢人。

很多系统一开始最大的问题，不是“模型不够强”，而是底层根本还没打稳。这个时候太早把复杂模型堆进去，很容易把问题遮住，而不是解决。

所以第一期的技术路线，我现在的想法是很明确的：

先做“规则系统 + 证明追踪 + 人工启发”的版本。

先把“能严格推出”这件事做好。之后再考虑是不是要引入更强的候选生成或搜索排序。

六、很实际的起步方案：先从几个小题打通整条链

我现在并不打算一上来就拿很难的题去测系统。

更实际的办法，是先拿几道非常典型、非常小、但足够能检验系统结构的题，去把“输入—推理—输出证明”这条链打通。

比如我很可能会从这一类题开始：

1. 三个连续整数的乘积被 6 整除

像这种题，看起来很基础，但其实特别适合当第一个 demo。

因为它会逼着系统处理：

• 连续整数
• 奇偶性
• 模 3 或“每三个连续整数必有一个被 3 整除”
• 把一个整除目标拆成两个子目标
• 最后再合并

如果这道题能完整地被系统吃进去，并且输出一条像样的证明链，那说明框架至少开始有点形状了。

2. n^3-n 被 6 整除

这道题也很合适。

因为它会逼着系统处理：

• 代数表达式
• 因式分解
• 连续整数结构
• 整除拆分

它比上一题稍微再抽象一点，但仍然处于第一期很适合碰的范围。

3. 平方数不可能模 4 余 2

这种题适合测“反证”和“小模分类”。

因为系统需要学会：

• 一个命题如果要证明不可能，可以转成模若干小数去排除
• 某类数在某个模下的剩余类是有限的
• 一旦所有可能剩余类都不符合，就可以形成矛盾

4. n^5-n 被 30 整除

如果前面的链路通了，这类题就很适合作为一个稍微进阶一点的目标。

因为它会逼着系统同时处理：

• 2、3、5 的拆分
• 同余和整除的来回切换
• 幂的模性质
• 因式分解或分类讨论

我现在更倾向于这样做：

先不用追求做出很多题。

先把两三道、三五道小题，真正从头到尾打通。让系统不只是“能得到答案”，而是真的能把一条推理链稳定地走下来。

这是非常实际的起步方式。

因为很多事情，纸上规划的时候都很顺；但一旦你真的让系统开始处理第一道具体题，问题马上就会暴露出来：

• 表达是不是不统一
• 某些规则是不是太弱
• 某些规则是不是太容易爆炸
• 启发是不是太散
• 证明输出是不是很难看

这些问题，只有真正拿题去跑，才会看清。

所以我对“起步方案”的想法很简单：

不要先做大，先把整条链跑通。

从少数典型题出发，把底层对象、规则、状态、追踪、输出全都过一遍。只要这条链真的通了，后面每往前走一步，都是有积累的。

七、我不怕公开，是因为这件事本来就不该靠“藏”来推进

有些事情，适合保密。

但我觉得这件事情，不太一样。

因为它本质上不是某个短线技巧，不是某个搞流量的小招，不是某个我今天藏着你明天就不知道的东西。

它更像一个方向。

方向这种东西，公开了，不是坏事。

别人知道了，别人做了，甚至别人做得更快、更好，我也不觉得这是什么损失。

因为如果最后真的有人把它做出来了，不管那个人是不是我，受益的都不只是一个人。

可能会受益的是：

• 数学教育
• 竞赛训练
• 数学知识整理
• 自动化推理工具
• 对“AI 做数学”这件事的整体理解

这类东西，本来就更接近公共进步，而不是某个小圈子的独占玩具。

当然，公开不代表空谈。

我也不想只停留在“我有一个很厉害的想法”。

所以我更愿意把它当成一个长期项目，慢慢记录，慢慢做。

做出来一点，就说一点。

规则整理到哪一步了，题型覆盖到哪一步了，哪些路走通了，哪些地方卡住了，哪些想法后来发现不对，都可以慢慢讲。

我觉得这样反而更真，也更有意思。

现在这个年代，大家很容易习惯一种节奏：

• 一周出成果
• 一个月闭环
• 三个月上线
• 半年就要讲商业故事

但我并不想用这种节奏来要求这件事。

因为我很清楚，这不是一个“拼手快就行”的项目。

它牵涉到很多非常基础、非常细的东西：

• 表达方式是否统一
• 规则是否严谨
• 状态是否会爆炸
• 哪些启发是有效的
• 哪些题型值得先做
• 证明输出能不能做到既正确又可读

很多地方可能都要推翻重来。

所以我对这件事的预期，不是“很快就震撼所有人”。

我更现实的想法是：

慢慢做，做出一个真正往前走的东西。

可能一年，两年，谁知道呢。

也许最后先做成的是一个很窄但很稳的小系统；也许后来逐渐扩到更复杂的题型；也许中途会发现某些原来以为可行的路其实很难；也许还会长出一些我现在还没想到的方向。

这些都正常。

我不怕慢。

我更怕的是，一开始就把话说得特别满，最后什么都没有。

所以我宁愿从小处开始，从硬处开始，从真正能积累的部分开始。

八、这件事如果做好了，我觉得价值不只是“会做题”

很多人一听这种方向，第一反应就是：

“那不就是做一个自动解题器吗？”

我觉得不止。

如果真的能把这个方向往前推，它的价值至少有几层。

1. 它能帮助我们重新理解“数学解题到底依赖什么”

很多时候，人的直觉很强，但不容易拆开说清楚。

一旦你试图让机器也能走这条路，你就不得不认真面对：

• 哪些是基础规则
• 哪些是题型套路
• 哪些是中间构造
• 哪些是启发式选择
• 哪些是不可少的真正洞察

这对数学本身的整理是有帮助的。

2. 它可能成为一种新的教学工具

不是只给答案，而是把推理路径保留下来。

如果有一天它真的能在某一类题上稳定工作，那它就不仅是“会不会”这个问题，而是能不能展示：

• 为什么先这样想
• 为什么接下来那样拆
• 哪一步是关键
• 哪一步只是机械整理

这对教学其实很有价值。

3. 它可能逼着我们把很多“模糊会用”的东西真正形式化

很多数论工具，平时我们会用，但不一定真的整理到了机器能接受的程度。

一旦真做这个系统，很多东西会被逼着变清楚。

这本身也是一种推进。

这篇文章发出来，不是为了证明我已经做成了什么。

恰恰相反，是因为我现在还在起步阶段，所以我更想先把方向说明白。

我准备公开做这件事。

不躲，不装神秘，也不搞那种“我这里有个大计划但不能说”的姿态。

就是公开地、老老实实地做。

做一点，记一点。

想法变了，就承认变了。

路线错了，就改。

进展慢了，也没关系。

谁做出来了，都是推进了数学的一点进步。谁在这个方向上往前拱了一下，都是好事。

我当然希望自己能做出一点真正有价值的东西。

但即使最后不是我最先做成、不是我做得最好，我也不觉得这件事白做。

因为有些事，本来就不是靠“捂住”来赢的，而是靠不断把路走出来。

我一直觉得，数学这件事，最动人的地方之一，就是它不太吃话术。

你会就是会，不会就是不会；能推出就是能推出，推不出就是推不出。

所以如果 AI 要真正进入数学，不应该只是学会把话说得更像，而应该学会接受数学本身的规矩。

这也是我想做这件事的一个很根本的原因。

不是为了让机器更像人表演会做题。

而是想看看，能不能把人的启发、机器的搜索、数学的严谨，慢慢拼成一个真正有用的东西。

这条路我会慢慢走。

一年，两年，谁知道呢。

反正先开始。

如果以后这个方向有了一点像样的进展，我也会继续写。

---

免责声明：

本文所载程序、技术方法仅面向合法合规的安全研究与教学场景，旨在提升网络安全防护能力，具有明确的技术研究属性。

任何单位或个人未经授权，将本文内容用于攻击、破坏等非法用途的，由此引发的全部法律责任、民事赔偿及连带责任，均由行为人独立承担，本站不承担任何连带责任。

本站内容均为技术交流与知识分享目的发布，若存在版权侵权或其他异议，请通过邮件联系处理，具体联系方式可点击页面上方的联系我。

本文转载自：简单读写 Uysieot Uysieot《我准备公开做一件事：做一个面向数论题的“严谨推理”程序》