区间算术
一种以区间代替单一数值进行运算的数值方法，通过将每个数表示为保证包含真实值的闭区间来避免浮点舍入误差积累，常用于计算机辅助数学证明中以保证计算结果的严格可靠性
时间轴 (近 90 天)
区间算术是一种用下界与上界构成的区间替代单个浮点数进行运算的方法，每一步运算都保证真实结果落在计算出的区间内，从而把浮点舍入、截断等误差累积为严格的整体界。
该研究提出了一套计算框架，将机器学习发现与计算机辅助数值认证、形式化验证相结合，针对周期重力-毛细波实现了接近机器精度的残差。
作者冻结神经网络给出的一个候选解，将其转化为显式的有限表示，然后使用区间算术对其方程残差给出严格的一致界，考虑了浮点舍入、傅里叶截断、混叠以及网格到连续统的误差。
区间认证和形式化工作均在大语言模型的辅助下完成，但结果的有效性独立于语言模型：数值界由区间算术严格包围，后续数学推导由Lean内核检查。
证明的核心是将几何体所有可能朝向切分成约1230万个盒子，对每个盒子用区间算术进行验证
整个验证过程消耗了约38个CPU小时
区间算术将每个数表示为保证包含真实值的闭区间，使数值计算达到接近严格数学证明的可靠性
计算机辅助证明先用高精度数值模拟定位可能的奇点结构，再用区间算术对计算误差进行严格界定，将数值观测转化为数学定理
全部知识事实 (8)
区间算术是一种用下界与上界构成的区间替代单个浮点数进行运算的方法，每一步运算都保证真实结果落在计算出的区间内，从而把浮点舍入、截断等误差累积为严格的整体界。
50%待验证该研究提出了一套计算框架，将机器学习发现与计算机辅助数值认证、形式化验证相结合，针对周期重力-毛细波实现了接近机器精度的残差。
50%待验证作者冻结神经网络给出的一个候选解，将其转化为显式的有限表示，然后使用区间算术对其方程残差给出严格的一致界，考虑了浮点舍入、傅里叶截断、混叠以及网格到连续统的误差。
50%待验证区间认证和形式化工作均在大语言模型的辅助下完成，但结果的有效性独立于语言模型：数值界由区间算术严格包围，后续数学推导由Lean内核检查。
50%待验证证明的核心是将几何体所有可能朝向切分成约1230万个盒子，对每个盒子用区间算术进行验证
50%待验证整个验证过程消耗了约38个CPU小时
50%待验证区间算术将每个数表示为保证包含真实值的闭区间，使数值计算达到接近严格数学证明的可靠性
50%待验证计算机辅助证明先用高精度数值模拟定位可能的奇点结构，再用区间算术对计算误差进行严格界定，将数值观测转化为数学定理
50%