See: https://www.nature.com/articles/s41586-022-05172-4 https://www.nature.com/articles/s41586-022-05172-4 IIRC there was another paper recently, with similar

See: https://www.nature.com/articles/s41586-022-05172-4 https://www.nature.com/articles/s41586-022-05172-4 IIRC there was another paper recently, with similar methodology about computing xAx. These papers produce algorithms which aren't empirically correct, but provably correct. They do this by operating on a graph data structure, which describes the algorithm and then verifying the algebraic equality to the correct result. There is a substantial difference here. And I think utilizing algorithms which only are empirically correct can be dangerous.