My picture

Hello! I’m Rish, a CS PhD student at the Laboratoire Méthodes Formelles (LMF) in ENS Paris-Saclay, part of the Deducteam research group. I am supervised by Frédéric Blanqui on the design and implementation of a tool for translating between Lean and Dedukti, and I expect to complete my doctoral studies in February 2026.

I’m generally interested in the use of proof assistants for formalizing mathematics and verifying/synthesizing provably correct programs. My doctoral studies relate to the topic of proof translation between proof assistants, for improved interoperability between proof systems with different theoretical foundations.

My post-doctoral research interests are around the areas of program verification and program synthesis, specifically within the context of proof assistants such as Lean. I’m interested in designing search spaces and intelligent agents for program synthesis, program specification synthesis, and subroutine discovery, as well as applications of program synthesis to automated reasoning tasks, in particular those of metaprogram/tactic synthesis, automated theorem proving, and the automated discovery of mathematical theories within proof assistants. I’m actively searching for post-doc positions along these lines!

Publications

Conference papers

(accepted paper preprint) Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation

Rishikesh Vaishnav

22nd International Colloquium on Theoretical Aspects of Computing (ICTAC) (2025)

Workshop papers

A Term-Patching Framework for Eliminating Definitional Equalities in Lean (work-in-progress report)

Rishikesh Vaishnav

LFMTP: Logical Frameworks and Meta Languages: Theory and Practice (2024)

Master’s thesis

Formalizing the Beginnings of Bayesian Probability Theory in the Lean Theorem Prover

Rishikesh Vaishnav

Master's Thesis, UC San Diego (2022)

Education

Community service