There's 2 cool things related to floating point error I learned recently. First, `x + x + x + x + x == 5x`. This is true for values up to 5, but is not true fo

There's 2 cool things related to floating point error I learned recently. First, `x + x + x + x + x == 5x`. This is true for values up to 5, but is not true for 6. Proving this is a fun exercise, but is a little bit painful and has a lot of cases. Second, SMT solvers can actually prove stuff like this relatively easy! In Z3py, one can prove this in 4 lines of code. from z3 import x = FP('x', FPSort(8, 24)) set_default_rounding_mode(RNE()) solve(5*x != x + x+ x+ x + x)