Reingold (STOC '05) proved in his breakthrough result that the problem of Undirected Connectivity, i.e. deciding whether nodes s and t are connected in a given undirected graph G, is in Logspace, culminating incremental improvements over a long series of works. In this talk, we will discuss whether Logspace can define and prove all the concepts involved in this result. Namely, is there a proof of "Undirected Connectivity in Logspace" in a system of Bounded Arithmetic that can only reason with concepts definable in Logspace? We answer this question in the affirmative. To establish this result, we use an alternative and arguably simpler proof of this result, by Rozenman and Vadhan (APPROX-RANDOM '05). Additionally, both proofs use eigenvalues and eigenvectors which are not known to be definable in Logspace, so we use the alternate and essentially equivalent concept of mixing ratios to formalize Rozenman and Vadhan's proof, using results from Buss, Kabanets, Kolokolova, Koucky (Ann. Pure and Applied Logic, 2020) and Mihail (FOCS '89) to bridge the gap. The proof is then completed by applying fixes to other concepts outside of Logspace used in the proof such as square roots and iterated matrix multiplication. Based on joint work with Sam Buss, Anant Dhayal, Valentine Kabanets and Antonina Kolokolova.
Short Bio: Sasank Mouli is an Assistant Professor at the Indian Institute of Technology, Indore. He received his PhD from the University of California, San Diego and his Bachelors degree from the Indian Institute of Technology, Kanpur. His area of research is Proof Complexity.
