FloatLib — First release

After several months of work, we’re releasing FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean. We built it with both speed and flexibility in mind, especially for verified machine learning and numerical software.

FloatLib supports IEEE binary and decimal, arbitrary-width posits, P3109, and user-defined formats and rounding rules. Its certified software backends carry Lean proofs that they return the same results as their reference specifications. The library also provides rounding, error-bound, and exactness theorems, including exact posit quire accumulation within capacity! More updates on the interval soon:)!