Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub: A Formal Disproof of Hirsch Conjecture. CPP 2023: 17-29