New blog post about the logical model for floating-point numbers that will be part of Lean 4.33: https://juliahimmel.de/blog/float-qanda/