Formal in Silico

领域 · 目标 G1 · 现状快照 2026-10-01

mini-DFT

一维周期约化 Hartree–Fock 模型，平面波离散。这是项目的第一个领域，可信账本、证书检查器与 trace validation 都在这里建立。目标 G1：在同一离散问题上与 DFTK.jl 0.8.0 功能对齐，每个输出都有 Lean 定理保证。

102条命题登记在可信账本中
92%已有机器证明：T3 74 条，T4 20 条
6 / 46项 DFTK 对齐功能完成；另有 4 项已一致、证书不全，其中包括 LDA
≤ 5×10⁻¹⁵与 DFTK 在同一离散问题上的能量差

01

可信账本中的命题

账本的 132 条命题中有 102 条属于 mini-DFT，下面按主题分组。等级的定义见纲领页。

T4 端到端 · 20 T3 机器证明 · 74 T2 模型检验 · 2 T0 测试 · 1 尚未达到目标 · 5
DFT 基础命题
离散模型 · 算法 · 并行 · 浮点
19
基态能量证书
8
有限温度自由能证书
14
Gaussian 展宽与冷展宽
5
SCF 解证书
Methfessel–Paxton · Marzari–Vanderbilt
10
k 点采样与超胞等价
7
离散误差
截断 K → ∞ · 真实高斯外势
13
基态密度与本征值证书
10
能带结构与态密度证书
3
LDA 交换（Slater）
实空间网格上的交换项 · 非线性 SCF 解证书 · 能量
13

T4 命题是各个证书检查器的可靠性定理（检查器全程用精确有理数，不涉及浮点）与 C 可信内核无运行时错误的证明。尚未达到目标的 5 条：一维 rHF 的连续适定性、平面波先验误差估计、线性混合的收敛（三者都在等待文献核对，目标 T1），截断极限等于连续模型的能量，以及 Lean 与 Rocq 的接口命题。

02

目标 G1：mini-DFT 与 DFTK 功能对齐

参照 DFTK.jl 0.8.0，在同一离散问题上比较。顺序：先在一维做全（M0–M3），再把 Lean 模型推广到 d 维做 2D/3D（M4–M5），最后是基础设施（M6）。

完成：实现、一致、有证书 对齐：一致，证书不全 实现：尚未对照 未开始
M0
已有功能
5 / 9
M1
一维求解器、占据与 k 点
1 / 7
M2
一维物理项
0 / 7
M3
一维后处理与响应
0 / 9
M4
d 维
0 / 7
M5
完整三维
0 / 4
M6
基础设施与接口
0 / 3

M0 · 已有功能

功能状态证书覆盖
动能、外势（Fourier 系数）、Hartree 项完成基态能量、密度、本征值与各能量分项
Fermi–Dirac 展宽与熵完成自由能、熵与能量；有限温度基态的存在性与密度唯一性已证明
Γ 中心、奇数个 k 点完成经等价超胞给出每个原胞的能量及其截断极限
偶数个 k 点、Monkhorst–Pack 网格完成半整数频率的等价超胞；含区界的网格除外
稠密对角化完成残差界给出每个本征对的包含区间，Sylvester 惯性确认它们是最低的几个
线性、Kerker、Anderson 混合实现不影响结果，结果由证书检查
非自洽能带、高斯展宽态密度对齐零温 Γ 点运行有证书；有限温度与 k 点运行尚无
超胞实现超胞等价已证明
k 点并行实现线程而非 MPI；并行协议经模型检验（T2），不同线程数结果逐位一致

M1 · 一维求解器、占据与 k 点

功能状态证书覆盖
Gaussian、Methfessel–Paxton、Marzari–Vanderbilt 展宽对齐
Gaussian 完成		Gaussian：自由能、熵与能量。MP、MV 的占据会超过 1，没有变分原理；检查器改为证明离散 SCF 方程在计算解附近恰有一个解，给出其化学势的界及其能量、自由能的严格区间（自由能区间宽约 5×10−14）。DFTK 的费米能级、能量与自由能都落在 Lean 区间内。缺：高阶 MP。
Monkhorst–Pack 网格、平移、时间反演约化完成不含区界的网格都有证书；DFTK 的能量落在 Lean 区间内
能带与态密度与 DFTK 对齐对齐同 M0
基于网格的 Hψ、LOBPCG、预条件未开始网格上的作用无混叠已证明
自适应能带数与对角化容差未开始
LDOS、介电、χ0 混合，势混合未开始
Newton 法、直接极小化未开始

M2 · 一维物理项

功能状态认证的内容
LDA 交换关联（Slater 交换、PW92 关联）对齐在与 DFTK 相同的实空间网格（M = 4K + 1 点）上求值；零温、Fermi–Dirac、Marzari–Vanderbilt、Gaussian 加 Monkhorst–Pack k 点、能带与态密度等六个体系的能量、各分项与全部本征值都与 DFTK 一致。能量不再凸，没有变分证书；对 Γ 点的 Slater 交换加 MV 或 1 阶 MP 展宽，检查器证明非线性 SCF 方程在计算解约 10⁻¹² 的邻域内恰有一个解，并给出它的化学势、能量（含交换能）与自由能的区间（DFT-X01–X13）。DFTK 的费米能级、能量与自由能都落在 Lean 区间内。缺：PW92 关联、零温、Fermi–Dirac 与 Gaussian 展宽、k 点。
计划中：M2–M6（29 项未开始）

M2 · 一维物理项

  • 共线自旋（LSDA）、磁场项
  • 局部非线性（Gross–Pitaevskii）
  • 精确交换（Hartree–Fock、杂化泛函）
  • 原子与赝势：局域与非局域部分、Ewald、修正项
  • 原子间两体势
  • DFT+U

M3 · 一维后处理与响应

  • 受力
  • 结构优化
  • 应力
  • 响应：χ0、Hessian、DFPT
  • 极化率
  • 声子
  • 弹性常数
  • 后验误差估计与细化
  • 电流

M4 · d 维

  • Lean 模型推广到 d 维晶格
  • 2D/3D 平面波与 FFTW
  • 任意晶格、原子结构、对称性
  • HGH 与 UPF 赝势
  • 三维 Ewald 与赝势修正
  • anyon（2D）
  • 与 DFTK 示例对标：硅、石墨烯、GaAs 表面、Cohen–Bergstresser

M5 · 完整三维

  • GGA、meta-GGA
  • 三维受力、应力、声子、弹性常数
  • 精确交换（ACE）
  • MPI k 点并行，1 到 64 个进程逐位一致

M6 · 基础设施（最后做，可删减）

  • GPU
  • 任意浮点类型、自动微分
  • Wannier90、VTK、JSON 与绘图接口

03

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

以下各量的严格区间

  • 离散基态能量；截断极限，以及离散误差的上界
  • 真实高斯外势（含 Fourier 尾部）下的能量
  • 基态密度（Coulomb 范数与逐点）与 Hartree 势的误差
  • 基态 Hamiltonian 的全部本征值与能隙
  • 动能、外势能、Hartree 能三个分项
  • 沿路径的能带与态密度的取值
  • 有限温度下的自由能、熵与能量
  • MP、MV 展宽：局部唯一的 SCF 解、其化学势、能量与自由能
  • LDA（Slater 交换）加 MP、MV 展宽：非线性 SCF 方程局部唯一的解、其化学势、含交换能的能量与自由能
  • k 点运行：经等价超胞给出每个原胞的值

04

交叉校验与辅助证据

基准不提升可信等级，但能发现理解上的错误：如果 Lean 区间排除了一个独立的参考值，就说明模型写错了。

  • DFT 基准，含与 DFTK.jl 的交叉校验（10 月 1 日的运行）143 / 143 通过
  • 同一离散问题上与 DFTK.jl 的能量（自由能）差≤ 5×10⁻¹⁵
  • 与 DFTK.jl 的全部本征值与能量分项差≤ 10⁻¹²
  • DFTK 的 Gaussian 自由能，以及 MP/MV 的费米能级、能量、自由能落在 Lean 区间内
  • LDA 在相同网格上对照 DFTK.jl：能量、含交换关联的各分项、本征值（六个体系）；有证书的 LDA 运行中 DFTK 的费米能级、能量、自由能一致；落在 Lean 区间内
  • LDA 的 SCF 解证书，K = 8（Marzari–Vanderbilt）：唯一性半径 / 能量区间 / 自由能区间 / 检查时间4×10⁻¹² / 1×10⁻⁸ / 2×10⁻¹⁵ / 6 秒
  • 1、2、4、7 个线程的运行报告逐位一致
  • Trace validation：收敛、能隙闭合、达到迭代上限、证书未通过四种结局全部接受
  • Trace validation：篡改的轨迹（证书未通过却报告收敛、丢失记录、上限不符）全部拒绝
  • SCF 控制器规范的变异测试（去掉证书检查或迭代上限）TLC 均能发现
  • k 点线程的 trace validation：每次领取、汇合与累加都按协议规范重放，1、4、7 个线程全部接受
  • 篡改的线程日志（重复领取、领取顺序与计数器不符、累加顺序错误、退出前汇合、缺少求化学势的步骤）全部拒绝
  • 报告校验：报告中每一行 Lean 都是检查器自己的输出；检查器拒绝、崩溃或不存在时驱动以错误退出通过
  • 收紧输入解析后，在 AddressSanitizer 与 UBSan 下对驱动做模糊测试（约 4 000 个变异输入）无内存错误、未定义行为与崩溃

05

缺口

没有 Lean 定理的输出算未完成。下面是已知的缺口，如实列出。

  • k 点求和相对无限晶体的误差每次 k 点运行对它自己的离散问题有证书，但 k 点求和相对无限晶体的误差还没有界；k 点能量不是变分的。
  • 含布里渊区边界的 k 网格没有证书；DFTK 在区界上的处理也不是同一个离散问题，两边都不比较。
  • 高阶 Methfessel–Paxton，以及 SCF 解证书的规模检查时间约按超胞阶数的四次方增长；有能隙体系在化学势取能隙中间时 SCF 方程病态，证书如实不通过；唯一性只是局部的。
  • Γ 点 Slater 交换加 MP/MV 以外的 LDAPW92 关联、零温、Fermi–Dirac 与 Gaussian 展宽、k 点与 DFTK 一致，但还没有证书；LDA 的能量区间是一阶估计，只覆盖 M = 4K + 1 点的网格。
  • 有限温度的离散误差目前只有零温的证书。
  • 截断极限等于连续模型的能量尚未证明。
  • 有限温度与 k 点运行的密度、本征值、能带与态密度目前只有零温 Γ 点的证书。
  • 证书中写的问题外势系数、周期长度、截断、电子数、温度与展宽函数由不受信任的驱动写出；检查器认证的正是这个问题，但既不重算也不回显它（A-DFT-05）。只有高斯外势的几行把系数与真实势对照。
  • 区间算术的代码层证明Lean 模型与 C 代码的一致性只有逐行对照与差分测试，没有证明。