I am a first year PhD student in Computer Science at UIUC where I am working with Talia Ringer. My research is in making interactive theorem proving a better tool for mathematicians.

Projects

Formalization of Holder’s theorem

Here is the homepage for the project which inludes a complete blueprint. Holder’s theorem classifies the ordered semigroups that are isomorphic to a subsemigroup of the real numbers. My formalization in Lean involves developing the basics of ordered semigroups and groups that are not commutative. This is a key step in the research I have done with Garrett Ervin.