继2025年9月7日，以徐扬、郭海林、陈树伟（茄子视频
系统可信性自动验证国家地方联合工程实验室）和Jun Liu（英国Ulster大学计算机系）为共同第一作者在Github上发布自动定理生成器Δ1以来，该团队先后在Github上发布了都能自动生成命题逻辑定理、一阶逻辑定理和高阶逻辑定理的系列自动定理生成器Δ1、Δ2、Δ2.5、Δ3和Δ4，在机器自主发现知识领域取得重大进展。
当分别给这些自动定理生成器输入任意多个、任意复杂的逻辑文字或闭公式后，这些自动定理生成器都能自动地直接快速分别生成海量的、逻辑上有意义的、逻辑上互不等价的非平凡命题逻辑定理、一阶逻辑定理、Henkin语义或Kripke语义下的高阶逻辑定理、命题逻辑极小不可满足子句集、一阶逻辑极小不可满足子句集、Henkin语义或Kripke语义下的高阶逻辑极小不可满足子句集、命题逻辑可满足子句集、一阶逻辑可满足子句集和Henkin语义或Kripke语义下的高阶逻辑可满足子句集。其正确性都由自动定理生成器的构建机制自身确保，不需要任何验证系统和人工再做验证，且也没有在这些自动定理生成器中内设任何自动验证系统。这些自动定理生成器在一阶逻辑中：直接成功地避开了（1）一阶逻辑中Turing Machine停机问题；（2）一阶逻辑定理的Church不可判定性；（3）一阶逻辑子句集不可满足性的不可判定性；（4）一阶逻辑不可满足子句集极小性的不可判定性；（5）一阶逻辑子句集可满足性的不可判定性；（6）生成的一阶逻辑定理之间等价性的不可判定性。这些自动定理生成器在高阶逻辑中，在Henkin语义或Kripke语义下：都直接成功地避开了（1）高阶逻辑定理的不可判定性；（2）高阶逻辑中子句集不可满足性的不可判定性；（3）高阶逻辑中子句集极小不可满足性的不可判定；（4）高阶逻辑中子句集可满足性的不可判定性；（5）高阶逻辑定理之间等价性的不可判定性。
这为人类让机器从更深层次、更高水平、更加快速发现新知识提供了一种全新而强大的手段，将对人类的科学研究与探索、工程应用以及生产生活方式等产生重大影响。
这项研究工作一直得到了中国茄子视频
和英国Ulster大学计算机系的大力支持。
有兴趣的人员可从如下网站免费下载和应用这些系统：
//github.com/SWJTU-math/Automated_Theorem_Generator
//github.com/SWJTU-math/Automated-Theorem-Generator-2
//github.com/SWJTU-math/Automated-Theorem-Generator-3
//github.com/SWJTU-math/Automated-Theorem-Generator-4
