使用Lean4进行形式化建模（以Java线程池为例）

2025-11-13 分类：技术专栏 阅读(212) 评论(0)

首先需要搞清楚一个概念，形式化证明，也是通过编程的形式进行的，只不过这段代码使用形式化编程语言进行表达，从数理层面来看更为严谨，常见的形式化语言有：