为什么值得关注

展示了复杂物理模拟的端到端形式化验证能力，在约 340 秒内自动生成了 24,614 行 Lean 4 代码和 11,730 行经过验证的 C 代码。

适合谁使用

数值相对论和计算天体物理领域的研究人员
形式化验证工程师和定理证明爱好者
研究弯曲时空电动力学的物理学家
自动代码生成与验证工具的开发者

典型使用场景

模拟黑洞等致密天体周围的电磁场
验证广义相对论中麦克斯韦方程组数值方法的正确性
将形式化验证应用于科学计算的课堂教学
评估自动定理证明系统处理真实物理方程的能力

项目优势

涵盖 1D、2D、3D 方程，包括标准版本和带有散度修正的完美双曲版本
明确给出了代码行数和生成时间（如 3D 完美双曲 GRM 方程耗时 86 秒）
从数学方程到可执行 C 代码的端到端验证流程
生成的代码包含 156 个定理和 270 个定义

使用前须知

生成的代码依赖 Lanyon 系统，该系统可能未被公开或难以复现
未讨论与手工优化求解器相比的性能表现
仅限 ADM 分解形式，不涵盖其他 GRMHD 公式

README 快速开始

General Relativistic Maxwell Equations for Curved Spacetime Electrodynamics with Lanyon

Highlights

End-to-end formally verified solvers for the general relativistic Maxwell equations and perfectly hyperbolic general relativistic Maxwell equations (with electric and magnetic divergence error correction), for electrodynamics in curved spacetime, in 1D, 2D, and 3D.
Took ~340 seconds for Lanyon to generate everything.
- ~31 seconds for the general relativistic Maxwell equations in 1D, ~54 seconds for the general relativistic Maxwell equations in 2D, ~71 seconds for the general relativistic Maxwell equations in 3D, ~37 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 1D, ~61 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 2D, ~86 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 3D.
- Real-time screen captures are shown in /screencaps.
24,614 lines of Lean 4 code to prove end-to-end correctness properties.
- 1,966 for the general relativistc Maxwell equations in 1D, 3,710 for the general relativistic Maxwell equations in 2D, 5,532 for the general relativistic Maxwell equations in 3D, 2,342 for the perfectly hyperbolic general relativistic Maxwell equations in 1D, 4,440 for the perfectly hyperbolic general relativistic Maxwell equations in 2D, 6,624 for the perfectly hyperbolic general relativistic Maxwell equations in 3D.
270 total definitions and 156 total theorems.
11,730 lines of formally verified C code.
- 1,001 for the general relativistic Maxwell equations in 1D, 1,798 for the general relativistic Maxwell equations in 2D, 2,641 for the general relativistic Maxwell equations in 3D, 1,150 for the perfectly hyperbolic general relativistic Maxwell equations in 1D, 2,080 for the perfectly hyperbolic general relativistic Maxwell equations in 2D, 3,060 for the perfectly hyperbolic general relativistic Maxwell equations in 3D.

Further Details

In a generic curved spacetime (decomposed into spacelike hypersurfaces via the ADM decomposition), the general relativistic Maxwell equations of covariant electromagnetism combine a pair of hyperbolic evolution equations:

$$ \frac{\partial \mathbf{B}}{\partial t} + \nabla \times \left( \alpha \mathbf{D} + \boldsymbol\beta \times \mathbf{B} \right) = 0 $$

$$ \frac{\partial \mathbf{D}}{\

项目描述

End-to-end formally verified solvers for the general relativistic Maxwell and perfectly hyperbolic general relativistic Maxwell equations in curved spacetime, in 1D, 2D, and 3D.

GeneralRelativisticMaxwell