SciLib 项目用 Lean 形式化百年物理实验与理论体系

CatAstro_Piyush · x · 2026-10-23

博主在连续 hackathon 第 241 天晒出 SciLib 项目的进展图。该项目试图在 Lean(其上依次搭建 Mathlib、Physlib、SciLib)中形式化物理学史：图示涵盖巴耳末公式(1885)、汤姆逊阴极射线测 e/m(1897)、盖革-马斯登 α 粒子散射(1909)、弗兰克-赫兹实验(1914)、长冈半太郎与玻尔的原子模型及卢瑟福散射论文等经典工作。

核心设计是把科学史表示为一个图结构：节点是理论(命题)与实验(原始记录)，边表示「A 蕴含 B / A 与 B 矛盾 / A 解释实验」，支持重复推导、检索全部已知结论、返回解释某实验所需理论的「return」操作，以及 supported/granted/refuted 状态标记。还定义了实验室仿真的传感器(读状态→数值)与执行器(施加命令→新状态或报错)接口。