Formal Verification of Gauss-Jordan Elimination

Stream: mathlib4

[crazerist]

I found the Gaussian elimination method in Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean. I'd like to know if there's a proof to verify the correctness of the algorithm? Specifically, there's a predicate that describes the row echelon form or row simplest form of a matrix, and the coefficient matrix obtained by the algorithm satisfies the definition of the predicate.If so, please let me know the location, thank you very much :)

[Vasilii Nesterov]

I don't think it was verified, because it's monadic code which is (was?) hard to verify. There is a
#general > new monadic program verification framework, but I'm not sure it's ready for such a verification.

[Yves Jäckle]

I remember coming across this repository, but it's in Lean 3.

[Martin Dvořák]

We formalized a part of the theory as a key step in the Seymour project:
https://github.com/Ivan-Sergeyev/seymour/blob/main/Seymour/Matrix/Pivoting.lean

Note that only the pivoting steps have a definition and API; Guassian elimination itself was used implicitly in some inductive proofs and isn't defined as such.