in the lean zulip you're encouraged to introduce yourself in a specific channel and I would like to but (as usual) the feeling that it's not a space i belong in, especially after seeing how everyone has their PhDs and is working in cool math stuff

and i'd be like haiiii :neofox: i'm just messing around, have contributed some lemmas to agda's stdlib and that's kinda about it