1977年，58岁的吴文俊先生开始研究几何定理的机器证明。在这之前，他已经是学部委员、国家自然科学奖一等奖获得者，在拓扑学上做出过被五位菲尔兹奖得主引用的工作。以他的学术地位，本可以选择更熟悉的研究方向。
他转向一个与此前研究截然不同的方向：把几何定理的证明变成可按固定规则机械执行的计算过程。1978年，他发表关于几何定理机器证明的奠基性论文，提出先把几何问题代数化，再以可机械执行的代数变换把假设方程组化成具有三角结构的特征列，据此逐步判定结论。整个证明过程可由计算机完成。这套方法后来被国际同行称为“吴方法”。
当时的研究条件与今天差距很大。电子计算机在国内远未普及，他最初成功证明的几条定理是手算出来的，证明中涉及的多项式往往有数百项，任何一步出错都会导致后面全部作废。后来有了机器，他从零开始学编程，自己写程序、自己上机，存储介质是穿孔纸带和打了洞的卡片，在相当长一段时间里是整个数学所上机时间最长的人。
到 80 年代，他把几何定理机器证明的方法扩展到更一般的方程机器求解，形成了一个系统的领域，即数学机械化。它的方法后来渗透到力学、天文学、物理学、化学、计算机科学，也被用于机器人、连杆设计、控制技术和计算机辅助设计。1997年，他获得国际自动推理领域的最高奖Herbrand杰出成就奖；2000年，他成为国家最高科学技术奖设立以来的首位获奖人。
吴方法在国际上产生了较快影响。1984 年以后，自动推理与符号计算界的一批知名学者，包括Bledsoe、Wos、Boyer、Moore、Kapur等人，对他的工作给予高度评价；他在国内发表的两篇论文，分别被《自动推理杂志》与美国数学会出版的《当代数学》论文集全文转发（当时国外很难看到国内发表的论文）。他的学生高小山后来回忆，1986 年前后吴先生在欧美各地讲学，意大利学者在二十年后的会议上仍说：“会议的明星是吴文俊教授。”
值得记下的是这个方向与产业的关系。如今，吴方法已被实现于若干主流的符号计算软件中；欧共体在1992—1995年资助的POSSO计划（POlynomial System SOlving）也开发了包含特征列方法的多项式系统求解软件包CARDANO。方法是中国人的，软件实现却率先发生在别人的系统里。这并非个人疏忽，而是从算法到软件产品通常要经历的过程；在中国，这一段路走得比较长。
事实上，这条路的探索在国内一直没有停。1990年，国家科委专门拨款支持数学机械化研究，中国科学院成立数学机械化研究中心，吴文俊先生任主任。1992年，国家攀登项目“机器证明及其应用”立项，他任首席科学家。1997年国家启动973计划，“数学机械化与自动推理平台”在270多个申请项目、三轮答辩后入选首批，1999年正式启动。
这个项目的名称值得注意：平台。从方法到算法，从算法到系统，从系统到平台，路线图是清楚的，方向也一直是往“能用”上走的。
这条路线最终落实为一套软件。在中国科学院数学与系统科学研究院数学机械化研究中心，高小山、王定康等把这条路线做成了一套自主的数学软件：数学机械化平台（Mathematics Mechanization Platform，MMP）。它以吴文俊开创的特征列方法为核心，能做多项式方程系统、代数常微分方程系统与代数偏微分方程系统的求解与投影，能做几何定理的机器证明与自动发现，还带有方程求解、机器证明、几何作图、机器人、机构设计、曲面拼接等成组的应用模块。因为整套软件要建立在自己的方法之上，MMP里包含一套自己的符号计算基本运算系统，由支撑系统、符号计算系统、核心模块与应用模块四个部分组成；它用 C++ 写成，运行在Windows图形界面下，发布过 3.0版本，以及MMP/Geometer、MMP/Robot、MMP/Linkage等应用包。2006 年，高小山、王定康、裘宗燕、杨宏把这套方法连同软件本身写成了《方程求解与机器证明——基于MMP的问题求解》，由科学出版社出版；这本书既是MMP的使用手册，也是了解数学机械化的入门参考。
中国科学院学部在一份战略研究里回顾这段历史时写道：在MMP之前，国内在方程求解、机器证明、几何作图等方向上做过多个成功的软件，但其中大部分是在 Maple 一类国外软件的基础上开发的，始终没有一个基于自己的理论、真正独立的通用软件平台。MMP走的正是另一条路：它用C++写成，自带一个符号计算基本运算系统作为支撑；按这份报告的说法，它不建立在Maple一类国外软件之上，是国内第一个基于自己的理论、真正独立的通用软件平台。这标志着国内符号计算软件的一条自主路线。值得提出的是，MMP与今天的ProdCAS 内核形态不同：MMP是一套自带图形界面与编程环境的完整平台，用户直接在这套软件里做计算；而ProdCAS是嵌在通用科学计算软件里的内核，供平台上的各种计算共同调用。
吴文俊先生本人对国家需求的变化十分敏感。2007年秋天，他在《参考消息》转载的一篇日本媒体文章中看到，中国尚未掌握高端数控的核心技术。在实验室的讨论班上，他从随身带的黑色书包里拿出那份报纸，对学生们说：“数学机械化方法有可能攻克这一关键技术，打破日本封锁。”此后，中国科学院的基础局与高技术局设立联合项目，支持数学机械化重点实验室与中科院沈阳计算所开展交叉研究；这一合作在数控系统最核心的“数控插补”环节提出了国际上性能最好的算法之一，并在商用数控系统中得到实现。
这些工作证明，中国的算法积累足以支撑起可用的软件，只是它们分散在不同的项目与团队里，各自沿着一条具体的路线走。从1977年到2007年，这三十年间，这个方向一直在向实际应用靠近。方法有了，软件也有人做过，但符号计算内核这块最基础的东西，始终没有作为一块通用的内核，装进任何一款国产软件里。
转折出现在2020 年。
那一年，美国MATLAB软件对国内部分高校停止授权。这件事在计算数学界引起的反应，不只是“少了一个工具”，而是一个更根本的问题被摆到桌面上：数学运算是一切工程计算的根干，而这个根干长期长在别人的地基上。在中国计算数学学会的常务理事会上，大家认为需要造出自己的MATLAB。任务落到了北京大学数学科学学院李若教授与卢朓副教授肩上。
起步的难度，团队后来这样形容：好比是对着核潜艇的图造核潜艇。一款通用科学计算软件，要从第四代编程语言写起，要把数值、优化、符号、统计各类算法整合编排成直观易用的功能，还要让人愿意用、能用起来。卢朓后来回忆，那几年他不得不花很多精力做软件推广。
那时候还有一个具体的窟窿：数值计算之外，凡是要拿出精确结果的地方都得靠符号计算内核，而北太天元没有这样一块内核。
最早顶上来的，是上海交通大学应文俊教授编写的原型代码。它解决了一部分问题，但可处理的范围有限。此后，团队转向调用开源符号计算库SymPy的路线，以支撑平台内部的基本需求。这条路走得通，也走得很艰难：性能受制于解释层与数据交换，接口要反复适配，功能边界取决于别人实现到哪里，而且平台的核心能力始终建立在一个外部依赖之上。
那几年，缺少自主符号计算内核是一个明确的事实。
在数学机械化的谱系里，还有另一条线索在延续。
李若教授的硕士导师黄凯教授，是吴文俊院士的博士后。李若在硕士阶段跟随黄凯教授学习计算机代数，博士期间转向偏微分方程的数值解，此后长期在计算数学与科学计算软件上用力。二十多年后他再次回到这个题目上，而这一次要做的不是论文，是一个能装进软件里的内核。而在中国科学院数学与系统科学研究院，数学机械化重点实验室至今延续着吴文俊先生开创的方向。贾晓红研究员长期以来在计算几何和计算机代数结合的方向上开展研究，自2020年起带领团队开发自研的CAD几何内核，而在几何内核的很多关键功能模块里，底层需要大量的符号计算库。“在团队专注开发几何内核的过程中，常常需要额外投入人力开发一部分符号计算库，这是一个不小的困扰。”于是，当李若说起要做符号计算内核这件事时，两个团队很快走到了一起。这项工作是李若与他培养的学生先做起来的；后来，中国科学院数学与系统科学研究院的贾晓红研究员与团队工程师曾铮也加入进来，一同参与开发。贾晓红研究员从计算几何与计算机代数的结合处走来，又带着自研 CAD几何内核的经验回到符号计算，走了一条不算短的路。李若同样离开过又回来。两个人最终走到同一个题目上。
这就是这件事的来路：一个从1977年开始的题目，几代人的算法积累，一个国家项目名单上写着的“平台”，以及两个因为同一个缺口走到一起的团队。
