OSI 黑客松作品 SciLib：用 Lean 对科学理论做机器可检验的形式验证

CatAstro_Piyush · x · 2026-10-23

团队在 OSI 黑客松提交了 SciLib——一个基于 Lean 的框架，为科学理论与实验带来机器可检验的形式化验证。其架构分层为 Lean → Mathlib → Physlib → SciLib，将理论（命题）与实验（原始记录）建模为图结构：节点是理论与实验，边表示推导、矛盾与实验解释关系，支持传感器/执行器的实验室仿真接口，可自动判断某推导出的主张是被实验支持还是与其矛盾。配图展示了用该框架形式化物理学史经典案例（Balmer 公式、Thomson 阴极射线、Rutherford 散射、Bohr 原子模型等）的示意。