tbh a lot of bluesky brand feels to me like "we added a hacky thing to solve what felt like a problem at a time and now we can't ever remove it although no other platform does this"
RE:
i worked on this proof for the entire week, and i finally got it working! i feel like i learned a lot about how to work with Lean.
the proof is about showing that it's possible to construct a set of all functions from one set to another as long as you have some way to construct a set of all subsets
[See https://leanprover.zulipch...](https://gist.github.com/gaearon/25a437a7b1773f4af94146af13d4fbd2 )
there's this liminal space of learning ability where you can already fix things with some luck but you don't fully understand why your fixes work. it's a funny feeling, like you have to rely on luck a bit and still can get royally lost but you're also not walking completely randomly. drunkard's fix
one thing that’s comforting about mathematics is that it doesn’t seem likely to fall apart with the passage of time (it did feel close to that a few times, but each time, it only came back richer and more magical — imo)
is there, in any sense, a field of amateur mathematics? i don’t mean in the “it doesn’t actually work” sense, although sometimes it is a consequence of being an amateur, but in a more general “tinkering but not too seriously” sense. in some other fields, amateurs make important contributions
