NavierStokesAndEuler

该项目是OpenAI发布的Navier-Stokes方程与Euler方程有限时间奇点（blowup）结果的Lean 4形式化验证库。核心功能是使用Lean定理证明器对两篇关键论文中关于不可压流体方程解破裂的严格数学证明进行机器可验证的形式化编码，覆盖全空间与环面两类Navier-Stokes设定，以及三维Euler方程的奇点构造。技术特点包括基于Mathlib的高阶数学库支持、端到端可独立验证的证明结构，以及与Comparator工具链兼容的验证流程。适用于数学基础、偏微分方程理论验证、形式化方法在分析学中的应用等研究场景。