@TaliaRinger@mathstodon.xyz

Talia Ringer @TaliaRinger@mathstodon.xyz

· 2mo ago

RE: https://lipn.info/@mevenlennonbertrand/116997917683191056 Scary. Also makes a case for funding fundamental type theory research in the age of AI

Quoting

Meven Lennon-Bertrand

@mevenlennonbertrand@lipn.info

This whole Lean kernel bug is almost too on point to be true, it fits perfectly in the discussions we've had here and elsewhere over the last months/years…

To summarize:

an AI agent let loose provides a sorry-free proof of the Collatz conjecture
the proof is detected as actually being a kernel bug
the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel's code is the reference
external checkers (lean4lean and nanoda from a week ago) reproduce the bug, because they essentially copied the reference kernel implementation

And so

AI raises the bar for kernel correctness by a lot
without a clear type-theoretic understanding of what is actually implemented, we're toast
external checkers help to catch implementation bugs, but without a clear specification they can't catch logic bugs

Open quoted post

lipn.info

Meven Lennon-Bertrand: "EDIT: I jumped too fast on the easy story, and o…" - lipn.info

25

2

6

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

We named the standard library for our Euclidean Geometry proof assistant "Euclib" and I'm so proud of this

44

1

4

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 2mo ago

A model that can't find vulnerabilities can't fix them, let alone formally prove their absence (for specific classes of vulnerabilies). When we keep those models out of the hands of the public, the bad actors will still find a way, but the public will be defenseless. Open weight is the future, and the sooner the US government sees that, the sooner they regain this country's once-comfortable lead in the AI race. For now, China will bask in this dual soft-power and hard-power win.

8

0

1

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

A few thoughts from talking to some of my favorite mathematicians (both for their work and, like, as people and friends) at the expMath meeting:

1. There is a big culture clash between math and AI, and it is really urgent that AI folks respect the mathematical culture if they want fruitful collaborations with math folks. (I remember this time in PL very well, in 2021-2022)

2. Never occurred to me that an emerging use case for proof repair is porting definitions, theorems, and proofs between ones mathematicians actually want to use and the ones autoformalization is good at (typically the mathlib ones)

3. What a time to be alive!

4. Lean's hegemony makes sense given community effects and need for a critical mass, but it's also worrying, and has implications for what kinds of math are represented. We need more work for other proof assistants

5. We have FROs, institutes, big commercial labs, startups, government labs, nonprofits, government funders, and academics who all care about this a lot. How can we work smoothly together? This is a hard problem without a single answer

6. Mathematicians want to create benchmarks by and for mathematicians, but they are also learning that doing this is a hard skill that needs to be developed

7. There is widespread agreement that collecting more of the data on thought processes and mistakes along the way to writing a proof is necessary. (This is an interest of mine dating back to the REPLICA paper in 2019)

Probably more can go here but I need to collect more thoughts first

28

0

7

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

Nobody warned me that humans can be this cute

24

0

1

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 8mo ago

We chose a target domain for our Build Your Own Proof Assistant class today. We are going to build a very encouraging and friendly proof assistant for middle/high-school geometry proofs.

Any resources or tips for targeting this domain?

35

10

8

2

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

God, the social questions around AI and math are way harder than the technical questions

19

1

4

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

I am so tired

10

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

Should I feel complimented or annoyed that proof repair (which I introduced in my Ph.D. thesis work) has become so commonplace that people don't even bother citing my work anymore when they do proof repair work?

12

0

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 4mo ago

Replying to

NiceGeo now includes a walkthrough that ships with the VSCode IDE plugin! Thanks to Priyam's hard work :)

6

0

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

If people are wondering what class prep looks like on my end for Build Your Own Proof Assistant, it's mostly organizing GitHub issues based on progress for the last sprint, and then writing specific goals for teams for the upcoming sprint that align with those issues and have concrete outcomes. So, basically, software engineering management.

9

0

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

Found a bug in our synthetic layer of axioms, then asked Gemini 3 Pro to see if it could find any bugs in our axioms just by comparing our `env.txt` file with the source PDF we are formalizing. It did, without being pushed towards the particular axiom, even though there are like 40 axioms in this system. That is promising. (No idea if the rest of what it says is meaningful, will investigate.)

https://github.com/nicegeo/nicegeo/issues/125

github.com

7

0

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

How do people decide whether to submit a formalized mathematics paper to AFM or JAR? I think the emphases of the venues are different, but in this case I think we could write a paper with either emphasis. Right now my algorithm is just "ask my Ph.D. students which kind of paper they would rather write"

6

0

3

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

My niece, who is 10 years old, is two years ahead in math (this does not surprise me, because I watched her put together puzzles stating at 6 months). I'm visiting her now. In their math class, apparently they meet to discuss famous mathematicians once in a while. "That's so cool, I just came from a big meeting with a bunch of mathematicians!"

I asked her if she remembered any they had spoken about and she couldn't remember lol

5

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

In particular, I went into this movie expecting to hate Oppenheimer. I instead found that I related to him a lot. That scared me, and made me think more about what this means for me right now as a researcher. It is something I need to sit with for a while, and I wanted to express that.

98

18

14

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 5mo ago

I'm looking for students interested in a paid summer research position: https://opportunities.cs.illinois.edu/research/paid-summer-research-opportunity-in-ai-for-program

opportunities.cs.illinois.edu

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

I probably could have been more eloquent at expressing this. I was also having a lot of feelings and just wanted to quickly get those feelings into words before going to sleep. I assume for some reason this led to folks digging into my past and finding the post about the NSA interview which mentioned a fun math puzzle. I maintain that this was the coolest interview question I ever had to answer, even though I'm also glad I didn't go work for the NSA. My research in undergraduate was in elliptic curve cryptology, and pretty much everyone around me interviewed with or went to work for the NSA; among math majors at Maryland in the pre-Snowden days, this was considered a prestigious and honorable thing to do. That sounds incredibly weird to me in retrospect, but it's also true.

69

4

9

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

I mentioned in that post that the war in Ukraine had changed my views about my ties with the department of defense in my capacity as faculty. This is true. I used to feel very torn about accepting any money from the department of defense for my verification work, or giving the department of defense advice about anything related to my research area of expertise, but recently I have been a lot less torn because of this war. My point with the previous post was that maybe feeling a lot less torn is shortsighted on my part. Maybe this was obvious to a lot of people, but it wasn't obvious to me.

51

23

3

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

Anyways, if you're going to dig through my past, here's my undergraduate honors thesis (under Larry Washington) if you'd like a bit of entertainment: http://honors.cs.umd.edu/reports/ringer.pdf

honors.cs.umd.edu

27

3

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

How do standard proof assistants handle motive inference for induction and rewriting? Especially interested in those that can actually do some kind of actual unification to tractably solve for all possible motives P, a la this ongoing issue in our geometry proof assistant: https://github.com/nicegeo/nicegeo/issues/182

GitHub

Improve unification algorithm to support motive inference · Issue #182 · nicegeo/nicegeo

Some kind of higher-order unification would help us a lot with improved automation for induction and rewrites. See below (a similar issue applies for all induction though). Fancy version that might...

1

2

1

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

@samth@mastodon.social @clegoues@lebrady.net I just wanted this post up so folks I follow understand the context of why I'm here and my old account disappeared, and so I can find my old followers, and so I can make clear where I stand on all of this. Part of that means please not attacking undergrads running a community space for free that they didn't even intend to become a space for the community that eventually migrated to it

3

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

@TristanNguyen@mathstodon.xyz He really is both an amazing teacher and a wonderful research advisor. I enjoyed working with him so much

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

@samth@mastodon.social @clegoues@lebrady.net I also want people to remember these mods are literally undergrads. I'm not happy with the events and would rather have my original followers and posts and DMs ported over, but also these are undergraduates running a thing for free, the power dynamic here is so obviously flipped. Anyone going after them or saying bad things about them rather than the particular decision is making me more upset than the original decision, honestly

2

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

@rastilin@aus.social Yeah, so one reason it was very easy to relate to Oppenheimer is that I am also a Jew, and my grandparents are Holocaust survivors. My grandfather in particular survived a Nazi death camp, and was orphaned and homeless after the war. I do not think I would be able to even think about tradeoffs when posed with a chance to stop the Nazis. I'd just do it. I feel haunted by that genocide still and I have nightmares about it sometimes. As a kid I was afraid of public showers because I thought I'd get gassed. I am emphatically not a pacifist when genocide is happening, and I believe that the Russian war in Ukraine is an ongoing act of genocide. I strongly support intervention, the same way I would strongly support intervention in China for the Uyghur genocide, or intervention in Myanmar for the Rohingya genocide. The larger picture is that something that starts as an act of intervention in genocide can easily be used as an act of genocide, or something equally horrifying. I don't think pacifism is the answer, but I do think I need to sit with that and understand what it means for the military-academic complex.

1

0

1

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 6mo ago

Whom will I see at the expMath kickoff?

0

Talia Ringer @TaliaRinger@mathstodon.xyz

· 38mo ago

Replying to

@vyodaiken@discuss.systems To be fair they somehow managed to make Teller look like the lead singer of My Chemical Romance which definitely didn't help his case

0

2

0