Brutkey

julesh
@julesh@mathstodon.xyz

My new job:

https://www.renaissancephilanthropy.org/a-structured-representation-of-tactics-for-machine-assisted-theorem-proving

julesh
@julesh@mathstodon.xyz

My new job:

https://www.renaissancephilanthropy.org/a-structured-representation-of-tactics-for-machine-assisted-theorem-proving

julesh
@julesh@mathstodon.xyz

Holy shit I think the category of dependent lenses aka the category of containers aka the category of polynomial functors is cartesian closed and I completely missed it

To be fair the construction is gnarly as fuck (I can't figure out how to implement it in idris)

julesh
@julesh@mathstodon.xyz

My thoughts about this just clicked. I have seen a bunch of cases of professed non-programmers building pretty big things entirely by vibe-coding, and they work fine. This allows people to participate in creation without years of training, and in the end that is not a bad thing

There are a bunch of other systems like this, that allow non-experts to simulate being able to do the real thing. Playing a shooter with aimbot. Playing guitar with 3 chords. Driving automatic.

These are all perfectly good things that allow amateurs to match the performance of experts, and none of them are bad things. But if you don't take the hit and switch over to the real thing sooner or later, you'll be a novice forever.

julesh
@julesh@mathstodon.xyz

Today is the 5th anniversary of my start date at Strathclyde, so today I will announce that I'm leaving academia

I am not leaving research - in fact the opposite, my research time is going to increase. For now I am essentially going back to being a postdoc, giving up my permanent position in return for a whole lot of upsides.

I will be retaining an official but unpaid position at Strathclyde for continuity of PhD supervision. I requested to stay on 10% FTE, in order to get at least a small fraction of the funding I've brought in, but my boss' boss rejected my request.

I have a lot of thoughts about the state of academia, possibly enough for a blog post, or at least a tweetstorm at some future date

I conspicuously haven't said where I'm going or what I'll be doing; this is under embargo but will follow at some point soon.