Talia Ringer

Professor, PL/FM/SE at UIUC. Proof automation. SIGPLAN-M Founder, CCF President. They/them, ND, bi.

Public Key

npub1vku3fe6ehffwyphmz04977g4h9v73ppgkzem3tnanp6pp4fkennqyvace4

NIP-05 Address

TaliaRinger@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqsxtwg5uavm55hzqma386jl0y2mjk0gss5tpvac4e7esaqs65mveesprpmhxue69uhhyetvv9ujuumwdae8gtnnda3kjctvqy28wumn8ghj7un9d3shjtnyv9kh2uewd9hstuv3yz

Publishing to

relay.snort.social

relay.damus.io

nos.lol

Author Public Key

npub1vku3fe6ehffwyphmz04977g4h9v73ppgkzem3tnanp6pp4fkennqyvace4

Show more details

Last Notes

2026-10-06 15:07:05 UTC

I want to frame this review summary. It reads like poetry and it really gets what our paper is going for. So happy today ☺️ will publish an updated pre-print once our camera-ready is ready. Very happy for my Ph.D. students Trey Plante, Eric Paul, and Cosmo Viola, and for my awesome collaborator Alex Kavvos. Such a fun collaboration with such a good team, and such a good outcome from it all.
https://media.mathstodon.xyz/media_attachments/files/117/394/569/546/769/297/original/67db054b8760c995.jpg

2026-06-10 20:07:39 UTC

Recently I had a chance to be publicly credited in a book for influence that I had informally and in private, but that had a downstream effect I consider positive and strongly in line with my career goals. Being credited also would have made it clear that certain parts of my vision for the future are not just things I ripped off of more famous researchers who, by default, get attributed for parts of the vision we share, even when the influence is mutual. This involved a popular science publisher that, in the past, had ignored me when writing about my field of expertise many times, even when others had sent them my name. Even getting interviewed was a first for me for this publisher!
That chance was quashed when the relevant influence was cut from the book. Now there is just a hole there. I have been replaced in the book by the muse of a famous researcher, nameless and never explicitly mentioned. I am a hole.
I am actually very depressed about this, even though it feels irrational to have ever expected this to work out. I know these informal sources of influence are usually left to recommendation letters. I know in this case that I have access to such a letter and that it can make my tenure case. I know that the researcher tried his best and this is more about the author and publisher of the book. And the author has even apologized to me.
But the chance of having this published in a book, as something I could cite and even show my parents, got my hopes up so high. Now the book is sitting on the floor of the entrance to my house, right where I dropped it when I first picked it up and had those hopes quashed. I'm left wondering why, time and time again, I play the role of the nameless muse.

2026-05-08 16:00:25 UTC

Our synthetic Euclidean Geometry proof assistant is now open for public contributions! We created this together as a class in my Build Your Own Proof Assistant course this semester. Please give it a spin and consider contributing! https://github.com/nicegeo/nicegeo
Some features:
- Dependent-type-theory-based proof kernel
- Synthetic Euclidean geometry layer (axiomatization of System E) with elaboration exhaustively tested
- Tactic-based interactive proofs
- Holes, bidirectional type checking, and unification
- Proof state management
- Custom tactic framework in OCaml
- Pretty-printing and error reporting
- Kind error messages
- Standard library (Euclib) for Euclidean geometry
- VSCode IDE plugin with many novel usability features
- Some geometry-specific proof automation
What's next:
- Interactive visual proofs
- Tabular proofs
- More geometry-specific & advanced automation
- Better support for user-written automation (e.g., a tactic language)
- Stronger IDE integration
- Expansions to Euclib
Please see our GitHub issues for more!
Our proof assistant is MIT licensed. Please see our contributor's guide if you would like to contribute. We especially welcome contributions addressing any of our open GitHub issues! https://github.com/nicegeo/nicegeo?tab=contributing-ov-file
This was a very impressive collaboration of about 20 students from many different backgrounds, who all came together for a semester to build something real. Everything from the domain to the design philosophy to the kernel to the automation was built from scratch collaboratively!

2026-02-04 18:29:49 UTC

- reply

@nprofile…0hgz I don't have anything decoupled from protected student information right now, but at the end of the class I will certainly write something about it in detail. Euclidean geometry as a target domain was something the class collectively decided on last week. I can send an early version of the course doc without identifying information but it also lacks domain specialization and specific ideas since that depends on what the class decides :)

2026-02-04 18:21:37 UTC

Build Your Own Proof Assistant course is going nicely. Still every class I cannot get people to leave once the class ends. They want to stay and keep collaborating.
The three initial teams exploring in parallel the three choices of foundations we are choosing from for our Euclidean geometry proof assistant (E, Hilbert, Tarski) are all making other fundamentally different design decisions (logic vs. type theory, LCF-style vs. classic de Bruijn style) and I'm super psyched for the discussion we have at the end of next week about those decisions and their tradeoffs.
After that we'll converge on one kernel and probably built it next sprint.
I rotate and help teams, but in between when I don't want to stress people out by hovering, I read Euclid’s Elements.
https://media.mathstodon.xyz/media_attachments/files/116/013/752/696/492/299/original/42cf87a0a352209b.jpg
https://media.mathstodon.xyz/media_attachments/files/116/013/753/348/306/320/original/692dda4cece749da.jpg

2026-01-29 17:59:55 UTC

What resources can I send students to help them get ideas for how to build a proof assistant kernel? Both LCF-style and more classic de Bruijn style are welcome. Example kernels, preferably at least some that are simple to understand, are also welcome.

2026-01-27 22:29:05 UTC

Euclid really was like "yo let's do synthetic constructive mathematics where diagrams have semantics" in 300 BCE what a fucking cool dude

2026-01-13 22:04:18 UTC

Guys. I did it. I submitted my third-year review package. Going to reuse most of it to go up for tenure "early" (on time minus the two extensions I took) next year

2025-12-24 12:20:05 UTC

- reply

@nprofile…l4xy my old grad school personal statement lol

2025-12-24 11:46:14 UTC

I think about this a lot tbh
https://media.mathstodon.xyz/media_attachments/files/115/774/374/262/393/514/original/ce4a28affe883850.jpg

2025-12-04 22:12:00 UTC

- reply

@nprofile…f2wy I always have trouble even understanding what constitutes a "cognitive task." In humans, we do not have any separation between cognition and embodiment, so all tasks we perform are in a sense cognitive. Where is the line drawn here? Often arbitrarily, from what I've read on this. Sometimes quite deliberately, in ways that excludes certain tasks in order to fulfill some narrative (typically one of utopia or dystopia).

2025-11-12 16:55:10 UTC

- reply

That link is supposed to be publicly shareable, but here it doesn't seem to load publicly for some reason, can others access it?

2025-11-12 16:49:47 UTC

New from me, in Nature: Mathematicians put AI model AlphaProof to the test. A solicited News & Views article about AlphaProof that was an absolute joy to write!
https://rdcu.be/ePz4Q

2025-11-07 18:44:49 UTC

What are all of the cool things you can do to polynomials, and what are the analogues for polynomial functors?

2025-11-05 21:40:19 UTC

- reply

@nprofile…rrqe yes that, what is the specific meaning? Are there useful examples? Could this give me an interesting class of changes for proof repair?

2025-11-05 21:19:02 UTC

- reply

@nprofile…rrqe er, the polynomial functor in a P-algebra / F-algebra, depending on which one you call it lol

2025-11-05 19:05:09 UTC

From the perspective of categorical semantics of inductive types, what would it mean to factor the polynomial functor in the P/F-algebra corresponding to its W-type encoding? From an automation perspective, what can I do when I can factor P/F?

2025-11-03 20:41:44 UTC

- reply

@nprofile…rrqe do you have any pointers on what problems there are open? I know Carlo mentioned in your controlling unfolding paper (which I will read soon for class) that there are actual soundness issues with forcing certain things to be opaque at certain times

2025-11-03 20:27:57 UTC

All proof assistants that have a notion of definitional equality should also have an option users can toggle to annotate proof terms with propositional equalities corresponding to each definitional reduction rule as it occurs. These propositional equalities would also be definitional by default, and in most cases would be useful for debugging and understanding computation. But one should also be able to force them to be opaque if needed, to pretend they are not definitional.
(I like definitional equality. I don't think we should get rid of it, and I think avoiding it for the most part as in mathlib is a big loss. I do think we should give people a way to make it more explicit, though!)

2025-10-30 20:59:42 UTC

Just had a conversation with someone else's PhD student from Indiana that immediately conjured, via vibes and feelings, a conversation I had back in 2016 and prompted me to tell them about the work discussed in that conversation. It may or may not be useful, but I'm just kind of baffled that my vibe/feeling-indexing of research ideas goes back to conversations I had almost a decade ago.

2025-10-09 20:48:01 UTC

- reply

@nprofile…hszg Formal Mathematics Seminar lol

2025-10-09 16:56:17 UTC

Are there any good, publicly available summaries of why people might prefer to work with synthetic math? Big discussion ongoing in class right now. @nprofile…4508

2023-08-26 20:54:19 UTC

If you're in the US, now is a good time to check that you're registered to vote, before election season kicks off. (My registration was out of date, it turns out)