Formal in Silico

领域 · mini-MD v0 · 现状快照 2026-10-01

mini-MD

一维 Lennard-Jones 原子链，Velocity Verlet 积分。Lean 检查器给出计算轨道与 Newton 方程真解之间距离的严格界：每一步都有，从初值出发的整体界覆盖约一个振动周期；守恒量则精确计算。2026-10-01 作为纲领阶段 2 的 MD 基础版本完成，与 ASE 3.29 交叉校验。

14条命题登记在可信账本中：T4 4 条，T3 9 条，1 条未完成
0.99真实局部误差 ÷ 证书的局部界：界几乎是精确的
≤ 5×10⁻¹⁴与 ASE 在位置、动量、能量上的差
约 1 个周期由从初值出发的整体界覆盖（8 个原子时 t = 0.5）

01

问题

体系直线上按次序排列的 N ≥ 2 个原子，质量 mi > 0。自由边界，全部原子对都相互作用，Lennard-Jones 势 φ(r) = 4ε((σ/r)¹² − (σ/r)⁶) 不截断。
方程q′ = p/m，p′ = F(q)。“真解”指这组方程的任意解，经典解都包括在内。
积分步长为 h 的 Velocity Verlet：半步踢、漂移、半步踢。驱动用双精度计算，不允许乘加融合。
输入参数与初值取证书中的精确有理数，即驱动实际使用的 double。它们与命令行十进制数的差别不在证书范围内（假设 A-MD-01）。

02

一次有证书的运行给出什么

8 个原子，步长 h = 0.001，600 步，初始温度 0.01。驱动把轨道写成证书，Lean 检查器 certify-md 用精确有理数重新检查；下面是报告的末尾。

build/mini-md --N 8 --steps 600 --dt 0.001 --T0 0.01 --certify run.cert --verify
…
Lean  MD_OK 8 600
Lean  E0 -7.186568898605097 -7.186568898605096
Lean  ENERGY_DRIFT 0.00000046826354893195
Lean  MOMENTUM_DRIFT 0.00000000000000029057
Lean  VERLET_RES 0.00000000000000044369
Lean  LOCAL_OK 0.00000000279045942382 0.00000004228626446212
Lean  TRUE_OK 500 0.500000000000 0.00099933951185418332 0.01514386287974667751
Lean  TRUE_HORIZON 500 0.500000000000
Lean  KMAX 19.447984
Lean  EPSMAX 0.00000004460799189706
行Lean 定理保证的内容命题
LOCAL_OK dq dp对每一步 k：从计算状态 (Qk, Pk) 出发的任意真解，一步之后与 (Qk+1, Pk+1) 的位置误差 ≤ dq、动量误差 ≤ dp。计算轨道是真实流的 dq 伪轨道。MD-B01
TRUE_OK j t dq dp从初值出发的任意真解，在 tj 时刻与计算状态的误差 ≤ dq / dp。MD-B02
TRUE_HORIZON H t整体界覆盖 [0, t]；其间原子保持次序，真解的能量恒等于 E₀。MD-B02、C01
E0 lo hi初始能量 H(Q₀, P₀)，精确计算后向外取整。MD-B03
ENERGY_DRIFT、MOMENTUM_DRIFT计算轨道上能量与总动量的最大变化，精确计算。MD-B03
VERLET_RES d数据满足 Verlet 的两个方程，残差 ≤ d：除了舍入，这条轨道确实是 Verlet 算出的。MD-B04
KMAX、EPSMAX诊断量（最大的 Lipschitz 常数与缺陷），不是结论。—

这次运行中，计算轨道的能量漂移了 4.7×10⁻⁷，而真解的能量在 t = 0.5 之前恒等于 E₀。这个漂移就是 Verlet 自身 O(h²) 的能量误差，现在它是有证书的数，而不是估计。

03

证书如何工作

对每一步，检查器构造一条可证明接近 Newton 方程某个解的曲线，再用管道定理推出任意解都留在它附近。全程用精确有理数；驱动的浮点数只是数据。

  1. 1

    真实流的 Taylor 多项式

    在每个数据点，检查器精确算出真解对时间的前四阶导数，为每个原子得到一个四次多项式。改用 Verlet 数据点做插值会留下 O(h) 的缺陷，因为 Verlet 的局部误差是 O(h³)。

  2. 2

    原子互不重叠

    由多项式的区间界，每对原子在这一步内距离为正；否则检查器报告 MD_FAIL。

  3. 3

    缺陷

    四次多项式离 Newton 方程有多远：D = m z″ − F(z)，力的三阶导数用区间包住（MD-A03）。

  4. 4

    盒子上的 Lipschitz 常数

    向量场在曲线的 ρ 邻域上 Lipschitz，常数由 φ″ 的区间界给出（MD-A02）。

  5. 5

    管道定理

    Grönwall 界 δeKt + (ε/K)(eKt − 1) 小于 ρ 时，任意解都留在盒子内并满足这个界。证明用首次离开时刻的反证，不需要事先知道解走到哪里（MD-A01、A04）。

局部界为什么几乎是精确的：它的主项是多项式与下一个数据点之差，也就是 Verlet 自己的局部误差 O(h³)；缺陷项是 O(h⁴)。三个体系中真实局部误差都是界的 0.99。

04

整体界与它的覆盖范围

多体 Lennard-Jones 轨道的逐点误差界必然指数增长：动力学是混沌的，相邻轨道按 eKt 分开。证书的界一开始就贴着真实误差（10 步后比值 0.91），然后以 K ≈ 19 的速率增长，到 t = 0.5（约一个振动周期）时达到管道半径。此后检查器仍然对每一步给出局部证书，但不再给出与初值真轨道的距离。

与真轨道的距离 · 8 个原子，h = 0.001

各原子位置误差的最大值，对数坐标。证书的界是 Lean 的 TRUE_OK；真实误差相对高精度参考解（scipy DOP853，rtol 10⁻¹³）测得，只作比较，本身不严格。

查看数据

这是问题本身的性质，不是证明技术的局限：混沌动力学不存在长时间的逐点误差界。长时间的结论要换一种形式——伪轨道的 shadowing、Verlet 修正 Hamiltonian 的向后误差分析、或轨道的统计量——都列在缺口里。

05

可信账本中的命题

T4 端到端 · 4 T3 机器证明 · 9 尚未达到目标 · 1
编号命题等级
MD-C01能量守恒：原子保持次序时，真解的能量不变T3
MD-C02动量守恒：力之和为零，总动量不变T3
MD-C03解的存在：Newton 方程在 [0, T] 上有解未达到
MD-D01Velocity Verlet 时间可逆T3
MD-D02Velocity Verlet 保持总动量T3
MD-D03Velocity Verlet 是辛映射，对 Lennard-Jones 原子链成立T3
MD-A01管道定理：Grönwall 界小于管道半径时，任意解都被限制在管道内T3
MD-A02缩放向量场在盒子上的 Lipschitz 常数T3
MD-A03四次多项式近似轨道的缺陷界T3
MD-A04一步的误差界T3
MD-B01检查器可靠：每一步的局部误差T4
MD-B02检查器可靠：从初值出发的整体误差；覆盖范围内原子保持次序、能量精确不变T4
MD-B03检查器可靠：初始能量、能量漂移与动量漂移的精确值T4
MD-B04检查器可靠：数据满足 Verlet 方程，残差不超过报告值T4

Verlet 辛性达到 T3（MD-D03）是纲领阶段 2 退出标准的一半；另一半 Céa 引理见 FEM 页。

06

交叉校验与辅助证据

  • ASE 3.29（LennardJones + VelocityVerlet），5、8、12 个原子的三条链，最多 2000 步：位置 / 动量 / 能量≤ 3.6×10⁻¹⁵ / 5.0×10⁻¹⁴ / 3.2×10⁻¹⁴
  • 整体误差与能量漂移的阶，相对 DOP853 参考解2.00
  • 计算轨道上的总动量守恒到 3×10⁻¹⁶
  • 真实误差 ÷ Lean 的界，局部与整体，三个体系≤ 0.99
  • 8 个原子的整体覆盖范围：T₀ = 0.01、h = 0.001 / T₀ = 0.1、h = 0.002 / T₀ = 0.001、ρ = 10⁻⁴500 / 122 / 全部 800 步
  • 篡改证书中的一个位置只让残差与局部界变大
  • 负质量、原子重叠、管道半径小于一步的缺陷MD_FAIL
  • 检查时间，8 个原子 1000 步（随 N² 增长）约 50 秒
  • AddressSanitizer 与 UBSan 下的驱动无报错
  • 报告校验：报告中每一行 Lean 都是检查器自己的输出；检查器拒绝、崩溃或不存在时驱动以错误退出通过
  • 收紧输入解析后，在 AddressSanitizer 与 UBSan 下对驱动做模糊测试（约 10 000 个变异输入）无内存错误、未定义行为与崩溃

07

缺口

  • 真解的存在证书对任意解成立，管道内解唯一，但解的存在性还没有机器证明（MD-C03）。可以用截断向量场加 Picard–Lindelöf，或用能量守恒做延拓。
  • 长时间的逐点误差如上所述，由混沌决定。能量范数下的对数范数、Lohner 型线性化传播可以延长覆盖范围；真正的长时间结论需要 shadowing、修正 Hamiltonian 或统计量。
  • 统计量温度、径向分布函数、自相关都和能量一样是计算状态的精确函数，尚未实现。
  • 周期盒子、截断、恒温器、约束、二维与三维、并行未开始。截断使力不连续，管道定理需要分段光滑的推广；并行协议（原子迁移、halo 交换）按计划用 TLA+ 描述。
  • 检查时间8 个原子每步约 50 毫秒，主要花在 φ 及其导数的精确有理数计算上；改用区间运算会快得多。
  • C 驱动本身不受信任（T0），所有结果都经过检查器。10 月 1 日起拒绝非有限或格式错误的参数，积分出现非有限状态时停止；证书中的初值与 Lennard-Jones 参数除 E0 外仍不由检查器回显。阶段 3 计划让 Verlet 单步达到 T4。