One of the major projects that's ongoing in the current decade is moving the standard math library functions to fully correctly-rounded, as opposed to the traditional accuracy target of ~1 ULP (the last bit is off).

For single-precision unary functions, it's easy enough to just exhaustively test every single input (there's only 4 billion of them). But double precision has prohibitively many inputs to test, so you have to resort to actual proof techniques to prove correct rounding for double-precision functions.

I don’t think I ever used atanh, but I always love some floating-point nerdery. These other documents by the same team are fantastic resources: https://inria.hal.science/hal-04714173v2/document for complex values and https://members.loria.fr/PZimmermann/papers/accuracy.pdf for real values.

Lots of good stuff here: https://members.loria.fr/PZimmermann/papers/ .

Good to know!