Interested in geometry, topology & formalization.
Open to opportunities in ML research, theorem proving, and symbolic AI. Let's chat →
I'm a an aspiring researcher interested to work at intersection of mathematics and formalization. Currently at Internet Brands, I build systems that make sense of complex data, analytics and automations and half of me is focused on developing, reading about formal techniques for theorem proving and mathematical reasoning with primary interests around general topology & geometry.
My background is in pure mathematics (M.Sc. from University of Mumbai), and I'm particularly interested in automated theorem-proving systems based on type theory like Lean4. These days, I spend my time tinkering with Lean4 etc. about how to make reasoning more reliable through mathematical rigor. And develop systems that combine neural and symbolic approaches.
Present
Working on lean formalization with an expository ladder from entry level to expert level assimilation of topic. There is no Mathieu group in mathlib this also attempts to add it to Mathlib library. A card game which explains symmetries and groups.
A mini-verfier which calculates the required answer using SymPy and matches with LLM answer to give 100% confidence.
A contextual chatbot using Langchain, Pinecone Vector Database, and GPT-3.5. Implemented multi-lingual embeddings for semantic search across languages. Built to explore how vector databases handle cross-lingual retrieval.
Category Theory by Tom Leinster
Exploring the abstract structures that connect different areas of mathematics—relevant for understanding compositional approaches in AI systems.
Formal Methods for theorem proving
Trying to understand how DPLL/CDCL works and how these are implemented in Lean4. Inspiration behind this Ilya Sergeys work with Velvet.
General Topolgy/Geometry Multiple Refs
σ-locally compact space, σ-compact spaces, Compactly generated hausdorff spaces retraction functor and other topics.
I studied mathematics at University of Mumbai, focusing on functional analysis, topology, algebra, and some optimization. During my master's, I was a summer research fellow at IISER Thiruvananthapuram working on metric spaces and their completion theory.
After graduating, I taught graduate-level mathematics before transitioning into these intersectional domains. The mathematical training has been invaluable—particularly when working on symbolic reasoning systems or optimizing large-scale pipelines.
Certifications: Machine Learning (Stanford/Coursera - Andrew Ng), Advanced SQL & EDA with Python (DataCamp)
Languages: Python, SQL, PyTorch, PySpark, Octave, LaTeX, C
ML/AI: PyTorch, scikit-learn, Langchain, HuggingFace, Vector DBs (Pinecone), Streamlit
Engineering: Git, GCP, Postman, Selenium, PostgreSQL, Tableau
I'm always interested in conversations about mathematical reasoning, symbolic AI, or theorem proving. Feel free to reach out via email or check out my blog where I write about math and ML.
Available for full-time positions and research collaborations