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.
Preprint
GFLean: An Autoformalisation Framework for Lean via GF:
We present an autoformalisation framework for the Lean theorem prover, called GFLean.
GFLean uses a high-level grammar writing tool called Grammatical Framework (GF) for parsing and linearisation.
GFLean is implemented in Haskell.
We explain the functionalities of GFLean, its inner working and discuss its limitations.
We also discuss how we can use neural network based translation programs and rule based translation programs together complimenting each other to build robust autoformalisation frameworks.
Slides and Talks
- This is a talk about GFLean.
GFLean is a Haskell program that uses the grammar writing tool 'Grammatical Framework' to autoformalise natural language text to Lean 4 expressions.
Here are the slides which I presented in the Bonn Trimester Program called 'Prospects of Formal Mathematics' at the Hausdorff Institute of Mathematics, University of Bonn (22 July, 2024).
- 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.
On McKinsey-Tarski Theorem (15 April, 2021)
- 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)
- 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.
Topological Completeness of S4 (9 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