FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean
arXiv:2602.15965v1 Announce Type: new Abstract: The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike the fixed types of IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats — some with as little as one bit of precision — alongside novel features such as stochastic rounding and saturation arithmetic. These deviations create a unique […]