photo

Shashank Pathak

Hello. I am Shashank. I am a PhD student in the Department of Computer Science at The University of Manchester, working on the natural language of mathematics and its relationship with type theory, with Dr Ian Pratt-Hartmann. Previously, I completed an MS in mathematics from IISER Bhopal. My MS thesis was on the topological semantics of the basic modal language and was supervised by Dr. Sujata Ghosh and Dr. Kashyap Rajeevsarathy. I am interested in automating mathematical reasoning and making proof assistants better.

Peer-reviewed Work

  • Pathak, S. (2026). Extending Flexible Boolean Semantics for the Language of Mathematics. In: de Paiva, V., Koepke, P. (eds) Intelligent Computer Mathematics. CICM 2025. Lecture Notes in Computer Science(), vol 16136. Springer, Cham.
  • Pathak, S., Extending Flexible Boolean Semantics for Plural Definites in Mathematical Language. ESSLLI 2025 Student Session, p.90. Slides.

    • Preprints

  • Pathak, Shashank. "GFLean: An autoformalisation framework for lean via GF." arXiv preprint arXiv:2404.01234 (2024).

    • Slides and Talks

  • Extending Flexible Boolean Semantics for the Language of Mathematics. Presented at the International Conference on Mathematical and Computational Linguistics for Proofs, 15-18 September 2025, Institut Pascal, Orsay.
  • This is another talk about GFLean presented in the Bonn Trimester Program called 'Prospects of Formal Mathematics' at the Hausdorff Institute of Mathematics, University of Bonn. It describes some recent developments in GFLean. Here are the slides and here is the video (22 July, 2024).
  • This is a talk about an earlier version of GFLean. Here is the video of the talk presented in Lean Together 2024 (1 January 2024).
  • On McKinsey-Tarski Theorem. This is the presentation of my MS Thesis Defense. In this, I describe a recent proof of the McKinsey-Tarski Theorem, and also a model-theoretic proof of the completeness of S4 with respect to the class of all topological spaces. The latter builds a topo-model out of the canonical topological space. This is in continuation with the first semester presentation
  • Topological Completeness of S4. This was the presentation that I gave at the end of the first semester of my MS thesis. It deals with axiomatizing modal logics of spaces. Specifically, the topological interpretation (first given by McKinsey and Tarski) of the basic modal laguage is introduced, and the soundness and completeness result of the modal logic S4 with respect to the class of all topological spaces is described (9 December, 2020).
  • This is something we (I and my friend Prasanna) presented in the 8th Indian School on Logic and its Applications (ISLA 2020) on the last day as a part of student's presentations. In this we describe what is automated theorem proving, and describe the Robbins conjecture whose proof was found by an automated theorem prover EQP. Automated Theorem Proving and the Robbins Conjecture (23 December, 2020)

    • MS Thesis

    This is my MS Thesis titled 'Modal Logics of Spaces'.

    Abstract: We describe two soundness and completeness results. The first one is the soundness and completeness of S4 with respect to the class of all topological spaces. The second, a stronger one is the soundness and completeness of S4 with respect to the class of all dense-in-itself separable metric spaces, called the McKinsey-Tarski Theorem. The theorems give a syntactic characterization of the logic of these class of spaces. For soundness and completeness with respect to the class of all spaces, we describe two different proofs. The first one uses the soundness and completeness of S4 with respect to the class of all reflexive transitive frames. The second one is called the canonical topo-model proof, and is constructive. Next, we describe a recent proof of the McKinsey-Tarski theorem which uses the fact that every formula which is not in S4 can be falsified on the space of rational numbers with the usual topology. We conclude with how these two results together point out the limitations of the introduced topological interpretation.

    Here is the abstract but in the “Explain Like I'm 5” format.

    This is an ongoing attempt by me to formalize my MS project in Lean. My first aim is to formalise the canonical topo-model proof of completeness of S4 with respect to the class of all topological spaces.

    Short CV

    Find it here.

    Contact

    Contact me at shashank dot pathak at manchester dot ac dot uk