A Formal Disproof of Hirsch Conjecture

on YouTube ↗

" summary

Claims a machine-checked counterexample to the Hirsch Conjecture: an explicit polytope whose graph diameter violates the Hirsch bound. Uses a formal proof assistant with low-level translations to extracted native code and a plugin running on Linux to compute graph distances, so the diameter check is executable and verified. Encodes vertices as bases where vertex-adjacency = basis swap by one element, replaces apex planes by parallel hyperplanes in the construction, and automates search and verification with a verified extractor/verifier.

AI-written summary · about

" related talks

• 55mSiegel's Theorem, Edge Coloring, and a Holant DichotomyJin-Yi Cai · Tensors in Computer Science and Geometry 2014
• 01h 02mFine-Grained Counting Complexity IHolger Dell · Satisfiability Lower Bounds and Tight Results for Parameterized and Exponential-Time Algorithms
• 33mLower Bounds for Subexponential Parameterized Complexity of Minimum Fill-in and Related ProblemsMichał Pilipczuk · Satisfiability Lower Bounds and Tight Results for Parameterized and Exponential-Time Algorithms
• 01h 02mFine-Grained Counting Complexity IIRadu-Cristian Curticapean · Satisfiability Lower Bounds and Tight Results for Parameterized and Exponential-Time Algorithms
• 25mOn computing homological hitting setsUlrich Bauer, Abhishek Rathod, Meirav Zehavi · ITCS 2023
• 23mWorst-Case to Expander-Case Reductionsamir Abboud, Nathan Wallheimer · ITCS 2023
• 25mExponential separations using guarded extension variablesEmre Yolcu, Marijn Heule · ITCS 2023
• 30mParameterized Inapproximability of Max k-Subset Intersection under ETHBingkai Lin · Satisfiability Lower Bounds and Tight Results for Parameterized and Exponential-Time Algorithms