Lean, NSF, and REU

Stream: general

[Jeremy Avigad]

Good news: the National Science Foundation in the US is now looking for REUs (Research Experiences for Undergraduates) involving formal methods and mathematics. It explicitly mentions Lean and formal libraries for mathematics.
https://www.nsf.gov/pubs/2023/nsf23082/nsf23082.pdf?WT.mc_ev=click&WT.mc_id=&utm_medium=email&utm_source=govdelivery

[Adalynn]

OF COURSE ITS AFTER IM DONE WITH UNDERGRAD

[Adalynn]

The literal end of my UG, too!

[Alena Gusakov]

Wonder if it would be worth it for me to try to apply for an NSF fellowship again, I got rejected the first time (I applied with a graph theory formalization research proposal) but that was a few years ago at this point

[Newell Jensen]

If there is anything that I have learned from mathematics it is try and try again.

[Newell Jensen]

But only if your heart is in it of course ;)

[Kevin Buzzard]

I apply for more grants than I get, I'm just sufficiently autistic that it doesn't bother me if I don't get one. There have been times where I've applied for something, not got it, understood from the referees reports what the problems were, fixed them, applied again and got it. But yhere have also been times when I've applied for something, not got it, tweaked it minimally, applied again and got it. Yhe reason I persevere is that I've seen how the system works from the other side (having been on committees) and am absolutely convinced that randomness plays a nontrivial role in the decision making process when giving out grants to mathematicians (at least in the UK). The bottom line is that if you don't apply, you definitely won't get anything!

[Alena Gusakov]

I guess the issue with NSF GRFP specifically is you can only apply to it twice in total

[Alena Gusakov]

Ahh actually I'm not even going to be eligible, you can't apply if you already have a masters degree/are more than a year into grad school and I am in my second year

[Jeremy Avigad]

Ah, that's too bad. There were three NSF representatives at ICERM last summer (one mathematics, two CS) and four at IPAM (all mathematics). They seemed to be enthusiastic about Lean and formal technology, so there's reason to be hopeful. Kevin is right that it's really a numbers game, and the only way to win is to keep playing.