RecodeX 重构消息，NEAR Protocol宣布其NEAR AI系统在Lean FRO的Lean Eval v1基准测试中排名第一，该基准用于评测极高难度的形式化数学问题。该系统几乎完全运行在开源权重模型DeepSeek V4.1 Flash上，成本较低且不依赖第三方模型。NEAR表示，这项工作为形式化验证NEAR Protocol及其核心合约奠定基础，也可作为工具供其他团队验证自身代码。