Talia Ringer

Stream: new members

[Talia Ringer]

Hi all, I'm Talia, and I'm finally joining this Zulip. I'm primarily from the Coq community, but recently I have gotten looped into some cool discussions about AI for math with proof assistants in the loop, and correspondingly I want to stay in touch with this community and understand what is going on here.

I'm a professor at UIUC and my work is on proof automation. These days I do everything from dependent type theory research to machine learning research in service of making formal proof more accessible. I also do a ton of community stuff, and I talk a lot on social media. Website is here: https://dependenttyp.es/

I am also really interested in potential collaborations with mathematicians, eventually. Most of my work has been for program verification, but I have strong views that if I'm building automation a community might use, I should know what it's like to do the work that community does. So I'd really enjoy doing some formal math at some point (I've done a small amount of math research before, before I ever got into computer science, but nothing with proof assistants), even before building automation targeting mathematicians specifically.

Anyways, hello :wave:

[Talia Ringer]

Thanks @Heather Macbeth for reminding me this place exists lol

[Johan Commelin]

Welcome Talia! Great to see you here!

[Jireh Loreaux]

Hi Talia, we're relatively close geographically; I'm at SIUE. We should chat a bit and find a time to get together.

[Talia Ringer]

Sure, you can use my Calendly for that: https://calendly.com/taliaringer/1-on-1-with-talia?back=1&month=2023-08 (for an initial chat, then we can plan from there)

[Jason Rute]

I definitely want to plug the #Machine Learning for Theorem Proving steam to you. Feel free to mention your papers and projects there when they come out.

[Talia Ringer]

See @Kevin Buzzard I joined after all :D