Some of the decomposition algorithms of Eigen are described as “proven”. I am someone who sometimes works on machine-checked proofs of code, so I am wondering what “proven” actually means here. I am thinking is most likely means that there is a hand proof (somewhere) of the algorithm but that the code itself has not been subjected to machine-checked proof. In any case, can someone point me to the proofs in question, please?