Literally the first line of the link:

“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“

My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.