01
问题
| Poisson | (0, L) 上 −u″ = f，两端各取 Dirichlet、Neumann 或 Robin 条件（两端都是 Neumann 除外）；任意有理节点网格上的 P1 线性元。 |
| 梁 | (0, L) 上 u⁗ = f，两端为固支、简支、自由、滑动的任意组合；三次 Hermite 元，未知量是节点值与节点斜率。 |
| 右端项 | 多项式、eλx、sin、cos（包括 qπx 的）的和与积；检查器用 Taylor 模型重新包住它们，不信任求解器的数值积分。 |
| 为什么先做一维 | Green 函数与经典解可以绕开 Sobolev 空间，所以每个结论都能针对真解；二维需要 Lean 中的 H¹ 模型。 |
02
可信账本中的命题
T4 端到端 · 3
T3 机器证明 · 8
| 编号 | 命题 | 等级 |
|---|---|---|
| FEM-C01 | Poisson：Green 表示是经典解，并且是唯一的经典解 | T3 |
| FEM-D01 | P1 的节点精确性与离散 Green 表示 | T3 |
| FEM-D02 | 单元内的逐点误差：Mh²/8 加节点误差 | T3 |
| FEM-D03 | Céa 引理（抽象形式，为二维做准备） | T3 |
| FEM-D04 | 离散最大值原理 | T3 |
| FEM-C02 | 梁：经典解存在且唯一 | T3 |
| FEM-D05 | Hermite 元的离散稳定性（不需要最大值原理） | T3 |
| FEM-D06 | Hermite 元的节点精确性与 h⁴/384 插值误差界 | T3 |
| FEM-B02 | 右端项的 Taylor 模型可靠 | T4 |
| FEM-B01 | P1 检查器可靠：u(xi) 的区间与 max |u − uh| 的上界 | T4 |
| FEM-B03 | 梁检查器可靠：节点值与斜率的区间，以及最大误差界 | T4 |
03
目标 G2：带形式化证明的有限元，对照 scikit-fem
参照 scikit-fem 12.0.2，在同一离散问题上比较。完成标准与 G1 相同，另加一条：能做到的地方，证书的结论针对连续问题的真解，而不只是离散解。一维时可以绕开 Sobolev 空间，用 Green 函数与经典解；二维需要 Lean 中的 H¹ 模型。
F0
一维 Poisson，P1 元
7 / 7F1
一维扩展
4 / 9F2
二维三角形网格
0 / 5F3
更多物理与三维
0 / 5F0 · 一维 Poisson，P1 元：已全部完成
| 功能 | 状态 | 证书覆盖 |
|---|---|---|
| 一维网格：均匀、加密、任意有理节点 | 完成 | 检查器验证节点有序 |
| P1 线性元、刚度与载荷组装 | 完成 | 检查器用 Taylor 模型重新包住载荷，不信任求解器的数值积分 |
| 非齐次 Dirichlet 边界 | 完成 | 由检查器的可靠性定理覆盖 |
| 多项式右端 | 完成 | 精确积分 |
| 线性方程组求解 | 完成 | 求解器不受信任，它的节点误差有精确的界 |
| 真解的节点值与逐点误差界 | 完成 | 经典解存在唯一、节点精确性、h²/8 插值误差、离散最大值原理均已证明 |
| Céa 引理（抽象空间） | 完成 | 已证明，为二维做准备 |
F1 · 一维扩展
| 功能 | 状态 | 证书覆盖 |
|---|---|---|
| Neumann、Robin 边界 | 完成 | 全部理论按一般边界条件证明；两端 Neumann 除外 |
| 非多项式右端 | 完成 | 多项式、指数、正弦、余弦的和与积，用余项经过证明的 Taylor 模型；节点区间宽约 10−15 |
| Hermite 梁元（四阶问题） | 完成 | 固支、简支、自由、滑动的任意组合；节点值与斜率都有严格区间；h⁴/384 插值误差已证明 |
| 自适应加密（一维） | 完成 | 按经过证明的单元误差界标记，而不是估计量；最终网格有证书 |
| 变系数方程 | 未开始 | |
| P2 及高阶 Lagrange 元 | 未开始 | |
| 特征值问题 | 未开始 | 可复用 DFT 的惯性论证 |
| 能量范数误差 | 未开始 | |
| 与 scikit-fem 的一维示例逐一对照 | 未开始 |
计划中：F2–F3（10 项，均未开始）
F2 · 二维三角形网格
- 三角形网格，形状正则性由检查器验证（Sleipner 的教训）
- P1、P2 三角形元
- H¹0 的 Lean 模型
- 保证上界的后验估计（平衡通量）
- 四边形元
F3 · 更多物理与三维
- 线弹性（Korn 不等式）
- Stokes 与混合元（inf-sup 条件）
- 二维自适应加密
- 四面体、六面体网格
- 并行组装，用 TLA+ 规范
04
一次有证书的运行现在能给出什么
关于真解的严格结论
- 每个节点上 u(xi) 的区间
- 梁问题另有斜率 u′(xi) 的区间
- 求解器自己算出的节点值的精确误差
- 整个区间上 max |u − uh| 的上界，以及逐单元的上界
- 自适应加密到指定容差的网格，容差在最终网格上有证书
05
交叉校验与辅助证据
- 11 个 Poisson、6 个梁用例，Lean 节点区间都包含参考解宽度 ≤ 3×10⁻¹⁵
- scikit-fem 与 mini-FEM 的节点值差（Poisson / 梁）≤ 3×10⁻¹³ / 4×10⁻¹²
- 证明的最大误差界与采样到的实际误差之比0.85 – 1.00
- 篡改节点值只让误差界变大
- 报告校验：报告中每一行
Lean都是检查器自己的输出；检查器拒绝、崩溃或不存在时驱动以错误退出通过 - 收紧输入解析后，在 AddressSanitizer 与 UBSan 下对驱动做模糊测试（约 14 000 个变异输入）无内存错误、未定义行为与崩溃
06
缺口
- 其他右端函数对数、分式、分段函数需要各自的 Taylor 模型；现在只有多项式、指数、正弦、余弦。
- 两端 Neumann 条件解只确定到一个常数，需要相容性条件与规范化；驱动与检查器现在都拒绝。
- 超越函数右端的检查时间每个单元约 13 毫秒，主要花在中点处的精确有理级数；改为逐项舍入的区间级数会更快。
- 梁的变刚度与弹性支承只有 EI = 1；检查器接受任意 4×4 边界矩阵，驱动只写出四种标准端部条件。
- C 驱动本身不受信任（T0），没有 Frama-C 证明；所有结果都经过检查器。10 月 1 日起严格解析数值，无法精确写出的输入一律拒绝（模糊测试曾发现右端项在 4 KB 处被截断、NaN 参数被写成 0）；证书中的边界数据与载荷仍不由检查器回显。阶段 3 计划让单元刚度组装达到 T4。