这是关于作者基于 Z3 开发的半自动化 Python 证明辅助工具 Knuckledragger 的介绍，包含基本设计、理论探索、应用领域等方面：

• 基本设计与内核：基于 Z3 的 AST 数据类型构建定理数据类型，以尽可能薄的框架原则性地链接到自动定理证明器，限制逻辑接近求解器已提供的内容以获得更多距离和可用性。核心是Proof数据类型，通过axiom和lemma函数构建，还可定义新函数和递归定义等。全局的lemma/define函数和defns字典稍显古怪，或许可分离到不同上下文。

• 理论探索：

  • Nats：自然数是定理证明器的基本数据类型，smtlib 未提供内置自然数类型，可从整数中切出或使用 Peano 代数数据类型，也可将自然数视为整数的子集，有多种双向归纳等原则。
  • Lists：列表是有用的类型，类似可定义其归纳原则，序列是内置类型，可基于其定义列表类型。
  • Reals：考虑了多种实数相关的内容，如避免 epsilon-delta 演算痛苦，考虑形式幂级数、实归纳、序列、收敛、中间值定理、扩展实数、Eudoxus 实数等。
  • Complex：将复数定义为实部和虚部的记录很自然，可定义复数的加、乘、共轭等运算及相关性质。
  • Powers：Z3 对抽象幂的推理原则不佳，可能需 axiomatize 幂运算，因为幂是加法和乘法群之间的同态。
  • Exp, Sine, Cosine：它们较难定义，可能需要通过复数或引入外部库如 flint 的界限来定义，如通过flint_schema定义正弦和余弦的界限。
  • Sets：尝试构建 ZF 风格的集合论，定义了Set等相关类型和函数，还探讨了替代集合论。
  • Linear Algebra：关注低维和有限维向量空间，定义了相关数据类型和运算，还探索了几何方面的内容。
  • Group Theory：群论很代数，可直接 axiomatize 单个有限可表示群，也可考虑以整数上的置换作为“宇宙”数据类型。
  • Category Theory：在项目中有一定基础，尝试将广义代数理论嵌入 Z3 ，并解决相关 typing 义务。

• 应用与便利系统：

  • 软件方面：包括建模 CPUs（如 Nand2Tetris 和 RiscV CPU）、Hoare 和 WP 逻辑、进行编程语言的元理论证明等，还在数值计算（如区间算术、固定点算术、浮点数等）和特征（如重载、datatype 字段、notation、tactics 等）方面有研究。
  • 替代求解器：lemma函数可接受额外的solver参数，默认使用 Z3，目前正在将 cvc5、vampire 等其他求解器适配到 Z3 接口，还提供了打印 tptp 和 smtlib 的实用函数。
  • 引理数据库：可扫描系统中的Proof对象构建引理数据库，用于机器学习训练集和提取定理证明竞赛基准等。
  • 其他：如 refinement 和 partiality、existentials、lambdas、induction（包括归纳关系）、generics、context、algebraic hierarchy、quotients、ite chains 等方面的研究和实现。
• 总结：Knuckledragger 在多个数学和软件相关领域进行了探索和实践，虽存在一些设计选择和挑战，但为自动定理证明提供了多种工具和思路。