Professor, @plfmse, @IllinoisCS! Proof Automation. @SigplanM & CCF Founder. Israeli-American for peace, equality, justice. Mom. They/ืืื, ND, bi
Joined March 2016
- Tweets 113,556
- Following 6,645
- Followers 32,575
- Likes 100,900
6,506 Photos and videos
Pinned Tweet
Miscellaneous excerpts from a fellowship application I put together this morning. Starting to put some of my thoughts about recent AI shenanigans into words
2
6
47
4,817
Talia Ringer ๐๐ชฌ retweeted
as an AC: LLM assisted reviews are terrible. LLM assisted author responses are terrible. Even if the authors and reviewers do take the effort to carefully guide the LLMs so they reflect their points precisely (and not all do) the result is a wall of text that is just painful.
6
5
74
7,528
Wish this had made it into the book, but glad to have it written here too. An email to Terry turned into an informal coffee chat in July 2023, which in turn changed how both Terry and I viewed the role of proof assistants and AI in the future of mathematics. (Also became friends)
One of the most interesting aspects of @leanprover's rise, as I came to understand it writing The Proof in the Code, is the degree to which chance events and small encounters changed its course:
*Johan Commelin walking along the side of the road in Princeton
*Kevin Buzzard tuning into Tom Hales's lecture from his backyard shed
*Patrick Massot needing to check a student's calculation.
Another story which I didn't get to include in the book is @TaliaRinger emailing Terry Tao, which turned into meeting for coffee in the summer of 2023, which turned into a multi-hour chat about the potential for Lean and other systems to facilitate large-scale collaborationsโthe kind that are common in other fields but rare in math (and would later be realized with the equational theories project).
As Talia wrote later in the Notices of the @amermathsoc, "In the futuristic world we live in, when you submit a pull request to Terry Taoโs GitHub repository, you do not need to worry much about accidentally breaking his proofsโno matter who you are."
2
2
31
3,983
Sometimes those informal coffee chats are more impactful than any publication you could write, any theorem you could prove, any tool you could build. But the informal moments get lost in history while the rest are preserved. They're cool and worth remembering
9
452
Talia Ringer ๐๐ชฌ retweeted
@TaliaRinger's article: ams.org/journals/notices/202โฆ
1
2
16
1,103
Talia Ringer ๐๐ชฌ retweeted
One of the most interesting aspects of @leanprover's rise, as I came to understand it writing The Proof in the Code, is the degree to which chance events and small encounters changed its course:
*Johan Commelin walking along the side of the road in Princeton
*Kevin Buzzard tuning into Tom Hales's lecture from his backyard shed
*Patrick Massot needing to check a student's calculation.
Another story which I didn't get to include in the book is @TaliaRinger emailing Terry Tao, which turned into meeting for coffee in the summer of 2023, which turned into a multi-hour chat about the potential for Lean and other systems to facilitate large-scale collaborationsโthe kind that are common in other fields but rare in math (and would later be realized with the equational theories project).
As Talia wrote later in the Notices of the @amermathsoc, "In the futuristic world we live in, when you submit a pull request to Terry Taoโs GitHub repository, you do not need to worry much about accidentally breaking his proofsโno matter who you are."
1
8
71
9,264
Talia Ringer ๐๐ชฌ retweeted
Jun 13
I canโt believe Anthropic comparing their product to nuclear weapons 800 times backfired on them. I am shocked
128
696
17,061
441,269
Talia Ringer ๐๐ชฌ retweeted
Jun 13
Wait - so Amazon, one of Anthropicโs biggest investors, allegedly jailbroke Claude and then snitched to the U.S. government?
This cant be real. What.
Jun 13
Wall Street Journal is reporting that Amazon reported the jailbreaks to the Department of Commerce, who instituted the ban
155
385
5,579
839,845
Talia Ringer ๐๐ชฌ retweeted
Jun 13
You have to be humble even when pursuing excellence.
I think the arrogance with which Anthropic has pursued the latest release has universally landed poorly.
30
61
892
58,981
I guess we are entering the era of omnipresent security exploits before the era of widespread formally verified software systems becomes a thing. Formal proof summer and hacker summer are one and the same, should have seen that one coming.
8
11
105
4,799
I mean, all software was terrible for so long before this, this has been a disaster waiting to happen for decades now.
1
23
1,052
And the software got even worse in the days of vibe coding before vibe proving. It will get better but only after everyone learns the hard way just how bad things can get.
28
681
What a series of events
Jun 13
The US government, citing national security authorities, has issued an export control directive to suspend all access to Fable 5 and Mythos 5 by any foreign national, whether inside or outside the United States, including foreign national Anthropic employees.
The net effect of this order is that we must abruptly disable Fable 5 and Mythos 5 for all our customers to ensure compliance.
Access to all other Claude models is not affected.
We apologize for this disruption to our customers. We believe this is a misunderstanding and are working to restore access as soon as possible.
Read our full statement: anthropic.com/news/fable-mytโฆ
1
13
1,191
Talia Ringer ๐๐ชฌ retweeted
Jun 12
Tapping the hoarding wealth sign again ๐๐ผ
Jun 12
BREAKING: Elon Musk has become the first trillionaire in history.
48
1,185
7,895
118,554
Talia Ringer ๐๐ชฌ retweeted
Jun 12
Elon Musk held up a chainsaw, fed USAID into the wood chipper, and at least 600,00 people have already died as a result - two-thirds of them children.
History's first trillionaire.
6,313
10,576
35,828
1,545,998
Talia Ringer ๐๐ชฌ retweeted
Jun 12
i donโt know how anyone can read that thereโs now someone with a verified net worth of a million million dollars and not conclude there is something deeply wrong with our current system
51
85
1,517
25,226
Talia Ringer ๐๐ชฌ retweeted
Instead of discussing how Elon Musk is now the world's first trillionaire, we should talk about how he killed hundreds of thousands of people through his dismantling of food and medical aid to poor countries
currentaffairs.org/news/how-โฆ
4,625
17,955
43,776
1,524,872
Talia Ringer ๐๐ชฌ retweeted
Jun 12
This proof is so funny. Computable functions on the unit interval have a computable fixed point but the proof has the nonconstructive step โcheck if there is a rational fixed point.โ Indeed, 1D Brouwer fails in certain sheaf topoi, and 2D computable-Brouwer outright fails in ZFC.
4
7
135
11,659
Soon AI will be so good at predicting the World Cup winner that none of the humans will have to play. We will be obsolete
1
1
10
811
Took the afternoon off and went on a date with my husband. Got Ethiopian food at Blue Ethiopian, then wandered to the small batch roastery from which they buy their coffee (Columbia Street)
1
21
1,059
I roast at home, so I asked if they ever let people see how the roasting goes there, and they said informally they do, and that I could just go back and look
1
5
635
Went back and spoke to the roaster, Grant, who was working. Learned a bit more about coffee and about drum roasting. Saw some custom roasting software for the drum roaster. Feel good
6
457