Anima 团队发布 Lean 验证浮点运算库 FloatLib

Caltech 教授 Anima Anandkumar 团队历时数月发布 FloatLib，一个在 Lean 中经过形式化验证的任意精度浮点运算库，目标是让可证明正确性与高效执行兼得。该库支持 IEEE 二进制与十进制、任意宽度等多种数值格式，也覆盖机器学习常用的小精度运算，服务对数值计算可靠性要求高的场景。

2026-09-21 ~ 2026-09-22 · 2 条相关

• Anima 发布 FloatLib:Lean 验证的高精度浮点运算库 — AnimaAnandkumar · 2026-09-21
• Lean 形式化验证库 FloatLib 发布,支持多种数值格式与 ML 小精度 — sytelus · 2026-09-22