Joseph Rotella

I am a Research Software Engineer at the Lean FRO, where I help develop the Lean programming language and theorem prover. I received my Sc.B. in Mathematics and Computer Science from Brown University, where I wrote my honors thesis, advised by Robert Y. Lewis, on verified tabular programming in Lean. In the summer of 2024, I worked on the AILean project as an intern at Amazon Web Services. I also spent many semesters as a TA for courses on interactive theorem proving, discrete math, and (at Carnegie Mellon) functional programming.

You can find my professional credentials on LinkedIn and my code on GitHub.