Ryland Gross

I’m a student at Harvard and currently a course assistant for Math 157 under Nathan Chen. In mathematics, I’m particularly interested in commutative algebra, formalization, and hyperreal analysis. Recently, I've also become interested in economics.

Currently, I'm working on formalizing the Allais Paradox.

LeanTeX

I am also actively working on LeanTeX, a LaTeX package for embedding Lean 4 code directly in LaTeX and rendering Lean's infoview output in the compiled PDF. The source code is here: GitHub.