Self-introduction: Jeremy Kahn

Stream: new members

[Jeremy Kahn]

Hi there! I'm a professor of mathematics at Brown University, working in complex analysis and dynamics, Lie groups, and hyperbolic geometry. Aside from finding Lean to be a highly addictive (and frequently sleep-destroying) video game for mathematicians, I'm hoping to contribute to the development of Lean as a tool for verifying research mathematics (including my own).

In particular I'm interested in automating formalization, and even more specifically, in the automated completion of subgoals.

[Alex Kontorovich]

Making it official, eh?! :) Woohoo!

[Kevin Buzzard]

@Jeremy Kahn I guess @Rob Lewis is also at Brown, in CS. He was one of the people behind the 2019 formalisation of Ellenberg-Gijswijt, a 2017 Annals paper.

[Jeremy Kahn]

@Kevin Buzzard Yes, I've met with @Rob Lewis a couple of times, and he recently gave a colloquium on Lean at the math department. We're lucky to have him!