julesh

Applied Compositional Thinking

Public Key

npub162av2ljs9sm0x3t0ryrz0ucrj6a70her80m7m0lrtxg086zu73rstvlr5t

NIP-05 Address

julesh@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqsd9wk90egzcdhng4h3jp387vpedwl8mu3nhaldhl34ny8napw0g3cpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qa0tfsz

Publishing to

relay.ditto.pub

Author Public Key

npub162av2ljs9sm0x3t0ryrz0ucrj6a70her80m7m0lrtxg086zu73rstvlr5t

Show more details

Last Notes

2026-08-03 13:15:30 UTC

Alright nerds I need linux advice, I think I have probably come to the right place
This laptop ships with a fairly heavily modified fork of Ubuntu that removes a lot of the Canonical stuff and replaces Unity with KDE
Last time I used linux was about 15 years ago. Back then I used Ubuntu with Gnome, and I personally disliked the feel of KDE a lot. How have things changed since then, and in particular in the shitshow that has been the last 6 months? If the first thing I do to this machine is replace KDE with Gnome, am I going to have regrets?

2026-02-19 14:00:36 UTC

- reply

@nprofile…97ud There is a better resolution using type-in-type: an omnipotent God can create a stone so heavy that they can't lift it, and then they can lift it

2026-02-19 12:33:17 UTC

- reply

@nprofile…sqfw What is this heresy? Category theory is not superior to the Son or the Holy Ghost, but equal to them

2026-01-27 14:37:43 UTC

- reply

@nprofile…tfwq I'm preparing to move my stuff off Godaddy and OVH are my leading contender, do you still recommend them?

2026-01-14 14:30:50 UTC

The hardest problem in computer science is naming things, therefore Nicolaas de Bruijn solved the hardest problem in computer science

2026-01-14 12:26:21 UTC

- reply

@nprofile…amew Well yes but everything is that, that doesn't distinguish what is special about transformers

2026-01-14 11:15:46 UTC

It's weirdly difficult to find good sources that explain how transformers and attention actually work, considering how important they are. Everybody just seems to repeat a variant of this diagram from the original paper, as though it actually explains anything
https://media.mathstodon.xyz/media_attachments/files/115/893/159/408/201/698/original/cdb664f51e5d8838.png

2026-01-06 20:23:55 UTC

Assembling furniture without instructions feels like solving a well designed puzzle, right down to that moment when you have finally understood the puzzle deeply enough to figure out what the real puzzle is

2025-12-31 13:16:05 UTC

- reply

@nprofile…4x5t I've still got a good 30 years to go until retirement and I have enough funding runway right now to spend time reskilling as a lumberjack or a circus juggler or a vtuber or whatever, so.... bet you my career that it doesn't?

2025-12-31 11:01:57 UTC

- reply

@nprofile…4x5t I don't doubt that, but it doesn't change what I said

2025-12-30 19:23:04 UTC

- reply

@nprofile…4x5t There was me thinking that (human) chess was currently going through its greatest golden age since the cold war

2025-12-26 11:06:23 UTC

- reply

@nprofile…8eua A discrete manifold equipped with an approximate scalar field? That sounds like it could be useful for some other stuff too

2025-12-25 13:32:19 UTC

- reply

@nprofile…8eua Today is the first day of Christmas so you should only expect a(1) = 1 gifts

2025-12-25 10:39:36 UTC

The number of gifts sent to you by your true love up to and including the 𝑛th day of Christmas is
𝑛(𝑛+1)(𝑛+2)/6
https://oeis.org/A000292

2025-12-21 21:01:43 UTC

- reply

@nprofile…8eua I'm not sure I have that much to say, especially not that you haven't already said. To be honest, I feel like doing interdisciplinary research is so difficult that if you're in a position where advice from a blog would help you, you've probably already failed

2025-12-21 14:53:35 UTC

- reply

@nprofile…8eua I had to scan back through my blog to see if I'd forgotten anything, but no, I never wrote about it. Well, pretty sure I wrote a few twitter threads about it, but it would be easier to write it again than to track those down

2025-12-21 14:07:34 UTC

There is no AI bubble. There is an LLMs bubble, and among all the other problems it causes it's also blocking progress in AI far more effectively than all the AGI doomer bros could ever hope to achieve

2025-12-21 13:58:21 UTC

- reply

@nprofile…8eua I submit {me, Philipp Zahn} (with several other people joining at various points) as a successful ACT collaboration. My experience broadly matches yours, this collaboration is more than a decade long and required very much meeting each other half way

2025-12-20 17:32:37 UTC

- reply

@nprofile…4x5t I'm not the right person to answer that (I happen to be an Idris programmer); my vague feeling is that Agda is the main language used as a testbed for new ideas (ie. the same role that Haskell used to have for polymorphic type theory), so it will probably continue to evolve, provided they have the courage to periodically break everybody's stuff like ghc always has. Perhaps Lean will do that too, but I would guess they probably face more social pressure to not break the big libraries

2025-12-20 16:47:31 UTC

- reply

Science advances one funeral at a time, and a bunch of mathematicians who are currently young and betting their career on Lean are eventually going to be dinosaurs sitting on hiring committees and insisting to their grave that it is good actually that their favourite proof assistant falls over if you hit it with a corner case of dependent pattern matching on something defined with coinduction-corecursion or whatever

2025-12-20 16:44:23 UTC

While it's cool and good that a bunch of mathematicians are experimenting with proof assistants, I'm very confident that one of the biggest consequences is that 20 years in the future, it will finally be sufficiently understood how to write a dependent typechecker, and a bunch of mathematicians are going to learn the hard way the meaning of the term "technical debt"

2025-12-15 12:24:00 UTC

What the LaTeX feature of Mathstodon is supposed to be used for: Writing formulas that appear beautifully typeset (except to people on any other server and anyone using any client except the web client)
What I actually use it for: quick access to the → unicode symbol for talking about my train journeys

2025-12-15 12:17:56 UTC

- reply

@nprofile…u6hy I was wondering which cities I've been to between 5 and 10 times. My first thought was Amsterdam

2025-12-09 13:28:37 UTC

- reply

@nprofile…ztfm uBlock Origin has no problem at all with native adverts on other sites, so I guess it's a non issue

2025-12-07 15:48:11 UTC

- reply

@nprofile…ral2 I find theorem proving (even for non open problems) impressive for the same reason that AlphaGo still blows my mind: algorithmic search for such high dimensional problems with no known metric seems to be obviously impossible

2025-12-03 23:15:50 UTC

Catching the subway home at 11.15 and I haven't missed the last one, finally I'm in a real city

2025-12-02 16:18:10 UTC

First I lived in Oxford when Lewis was still be regularly filmed, and later a chunk of a Transformers film was also filmed there. Then I moved to Leipzig where a police procedural for local tv was filmed in the same building I worked in. Then I moved to Glasgow where many Hollywood films are filmed (in the 5 years I was there there was a bunch of Batman, a bunch of the Catwoman that was infamously deleted for tax reasons, and a scene of Indiana Jones). Now I live in London and *something* is being filmed outside our window, although I haven't figured out what yet.

2025-12-01 10:29:28 UTC

- reply

@nprofile…ral2 They made up a number and got mad at it

2025-11-28 22:15:58 UTC

This idiot left their laptop in a cafe so I'm forced to (gasp) read books
Just did the first half of Logicomix and now making a start on Piketty's Capital

2025-11-24 12:05:03 UTC

- reply

@nprofile…ztfm i saw Helfgott give a talk about this proof once. I understood basically none of the details (starting from the explanation of the classical Hardy-Littlewood proof that it starts from), but it was still one of the coolest talks I ever saw

2025-11-18 11:13:07 UTC

A genre of twoot I just don't understand is screenshots of google dot com showing a hilariously and/or dangerously wrong answer. Like, you're using an LLM and trying to treat it like it's a search engine, literally what did you expect?

2025-11-10 14:13:59 UTC

- reply

@nprofile…4x5t @nprofile…0775 For me the interesting question is why every actegory gives you both, while general enrichments only give Para and only tensored ones give you Copara. Feels like a broken symmetry

2025-11-10 11:04:24 UTC

- reply

@nprofile…4x5t Inside our group that was Dylan. I don't remember if it ever got written down anywhere though

2025-11-05 17:21:37 UTC

- reply

@nprofile…ral2 Fun fact, since negation is strictly involutive (p and not-not-p are different names for the same proposition), proof of negation and proof by contradiction are actually different names for the same logical rule, they only differ by a relabelling

2025-11-02 13:03:20 UTC

- reply

@nprofile…mk8f No, 100% organic artisan CSS

2025-11-02 12:28:12 UTC

https://julesh.com/ is finally starting to look close to how I would like, after changing the font to Open Sans 3
https://media.mathstodon.xyz/media_attachments/files/115/480/092/771/387/183/original/b698cecc81ada5ba.png

2025-10-29 12:44:08 UTC

- reply

@nprofile…ral2 When ported all my blog posts recently I checked all the links, and noticed that a few that claimed to be to my twitter threads were dead

2025-10-26 11:12:58 UTC

- reply

@nprofile…jahe I might do that if I get stuck, but I only ever use an llm if I want to do something without learning how to do it, and I do in fact want to learn css

2025-10-25 11:35:36 UTC

I really want to improve the visual style of https://julesh.com. Unfortunately this requires learning something about CSS. This is quite a dilemma.

2025-10-25 10:15:25 UTC

- reply

@nprofile…ral2 I think the hype bubble was so ridiculous that nobody can be taken seriously for working on it even like 3 decades after it burst

2025-10-23 21:51:20 UTC

- reply

@nprofile…ztfm @nprofile…8eua
This is the orange site, if you don't expect the worst from it then you haven't been around it long enough

2025-10-23 20:33:53 UTC

- reply

@nprofile…ztfm @nprofile…8eua
https://news.ycombinator.com/item?id=45677397
(but nothing especially worth seeing there)

2025-10-22 16:58:36 UTC

- reply

@nprofile…ztfm She does have a daemon, you just can't see or interact with it

2025-10-20 23:12:24 UTC

The proof is left as an exorcism for the reader

2025-10-18 10:36:51 UTC

- reply

@nprofile…ral2 My pet theory is that the main purpose of sleep is to copy memories from the cortex to somewhere more stable, but that requires suspending normal operation of the cortex. Meanwhile anything running on digital hardware you can generally copy anything freely without disrupting anything

2025-10-17 11:13:19 UTC

- reply

@nprofile…ral2 My gut feeling is some version of the first thing will actually be necessary, but not the second thing (whatever is the function of sleep, my gut feeling is that it is probably a quirk of the weird hardware the mind runs on)

2025-10-16 20:58:10 UTC

- reply

@nprofile…w8t5 Academics gonna academic

2025-10-16 11:08:23 UTC

- reply

@nprofile…w8t5 Hm, I find this a pretty interesting question, at first I strongly disagreed but I'm sort of coming round to your point of view. If the rules of form are only being checked externally, either by a machine or by other humans, are you working formally or informally? If you submit classical paintings over and over until the curator accepts you got the form right, were you following the laws of form? Is it possible that Bach intuited the formal rules of fugue so deeply that he was actually writing informally?

2025-10-14 18:29:30 UTC

Migrating https://julesh.com off https://wordpress.com has been something I've wanted to do since at least 2019. I'm so so happy to have finally done it.

2025-09-29 22:20:31 UTC

For some reason I was 100% convinced Wikipedia was based in Sweden, I'm actually horrified to learn that it's entirely American
So...... rest-of-world alternatives to Wikipedia?

2025-08-18 10:58:57 UTC

- reply

@nprofile…pmdx It's one of the papers that made me first notice how irrelevant the idea of publication is

2025-08-06 09:50:10 UTC

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.

2025-07-26 12:28:22 UTC

If I was planning a city from scratch I would simply grade the surface 1 floor higher than the natural ground. You have the additional cost that every street needs a covered roof strong enough to bear the weight of pedestrian traffic, but in return for that you solve a whole bunch of problems. The streets of the entire city are exclusively for pedestrians and cyclists - you don't even have the option to backtrack on that because they can't bear the weight of road traffic. Most buildings have a basement level, and below every street you have a combination of mass rail transit, roads for cars (with exhaust fumes extracted and vented far away from the pedestrians), loading bays and car parks, utility tunnels, floor reservoirs, and commercial buildings that don't need daylight access like supermarkets and distribution warehouses. You avoid ever having to dig any tunnels, and never having to see or breathe a car is a massive quality of life boost for everyone.

2025-07-20 15:00:44 UTC

ibuprofunctor

2025-07-19 16:27:40 UTC

- reply

@nprofile…hszg How short is short? If I remembered correctly that's the topic of the first half of Lambek & Scott Introduction to higher order categorical logic

2025-06-26 18:55:12 UTC

As far as I can tell, HoTT is about making types into (∞,0)-categories (aka ∞-groupoids), and the directed HoTT folks want to make types into (∞,∞)-categories (aka ∞-categories), but I reckon you could already get a lot of mileage if you could make types into (∞,1)-categories (aka categories, up to the amount of weakness I expect to be necessary in type theory). And that sounds probably a bit easier.

2025-06-11 10:11:00 UTC

- reply

@nprofile…e5g0 Unable to tell if sarcastic or not, but I suspect yes

2025-06-05 10:43:13 UTC

- reply

@nprofile…fa4k Here's the standard answer: the von Neuman-Morgenstern expected utility axioms are equivalent having real-valued utility, and *you* try doing any nontrivial modelling without using any calculus

2025-05-26 07:28:37 UTC

The intuitive reason that the internal logic of lenses is linear is that if you could copy data then you could have update conflicts. You can only copy the things for which you have a strategy to resolve conflicts.

2025-05-23 18:51:51 UTC

So apparently Scotland now has a tropical monsoon climate and everyone is excited that the rains have come

2025-05-14 12:46:30 UTC

- reply

@nprofile…hszg !!!!!
I worked a lot of this problem back in the day, which led to this unpublished paper
https://arxiv.org/abs/1811.06810
where we concluded that this is impossible - but the argument was very technical and I don't remember how it worked
Since it's been a long time since I worked on this stuff, remind me, is your definition of "optimal play" equivalent to "strategic play of a subgame perfect equilibrium"? The goal for me was always to characterise the set of those.

2025-04-23 17:29:11 UTC

- reply

@nprofile…fa4k Nice! Unlike last year I'm going to make an effort to hang around for this, if I'm allowed to. Naturally I'm very interested in the economic part

2025-04-01 19:37:14 UTC

- reply

@nprofile…fa4k For those who don't know, PhD positions in the UK that are not just open to UK citizens (or those with existing residence permits) are rare as hens teeth

2025-03-16 17:52:05 UTC

- reply

@nprofile…fa4k The article I linked has a lot to say about that. One of the main underlying causes is that the Scottish government pays for Scottish students to study in Scotland, but they amount they pay hasn't been adjusted for inflation in a very very long time, so universities now make quite a big loss on every single Scottish student

2025-03-16 17:32:14 UTC

https://www.bbc.co.uk/news/articles/cddynyz9q6po
https://media.mathstodon.xyz/media_attachments/files/114/173/301/214/753/739/original/7b8dea33deb86b6f.png

2025-03-14 15:21:32 UTC

Recreational mathematics puzzle: is there an interesting number that is approximated by today's date, 14.3?

2025-03-01 13:39:53 UTC

Einstein notation works for the frobenius/hypergraph structure of tensors, right? As in, instead of an index appearing exactly twice it can appear any number ≥ 1 times and you just sum over all of them? Do physicists actually use that?

2025-02-24 11:22:53 UTC

- reply

@nprofile…e5g0 Same (although I have long assumed that the CDU is not more right wing than British Labour, who allegedly pass for left wing in England)

2025-02-24 10:21:28 UTC

A lot of politics is threatening to occur
https://media.mathstodon.xyz/media_attachments/files/114/058/357/580/848/534/original/b6b9ac97e2c9a507.png
https://media.mathstodon.xyz/media_attachments/files/114/058/358/081/869/379/original/856f2819c1812cc6.png

2025-02-21 20:31:31 UTC

Ah yes, a letter of support for the NIH, that'll learn the bastards for sure

2025-02-17 13:07:14 UTC

It's a day to keep a close eye on the news. Counting so far: Germany, Sweden and the UK have said they are willing to put soldiers on the ground in Ukraine

2025-02-16 15:07:49 UTC

- reply

@nprofile…e5g0 Ok I last thought about how Enigma works when I was a teenager and don't remember much about it, now I am wondering whether it's yet another thing that's secretly lenses

2025-02-16 12:36:54 UTC

- reply

@nprofile…e5g0 Is it just that they are both instances of iterating a fairly simple function a few times creates complicated behaviour?

2025-01-15 13:14:25 UTC

It's only a banana if you have 2 of them. If you only have 1 it's a unanana, and if you have a bunch of 𝑛 of them it's an 𝑛-anana

2024-09-02 09:50:38 UTC

Current affiliations:
90% Institute for Categorical Cybernetics
10% University of Strathclyde

2023-12-31 14:43:27 UTC

Knives are cutlery, forks are stabblery, spoons are scooplery

2023-12-12 13:42:30 UTC

New blog post: AI safety meets value chain integrity
tl;dr - Advanced AI making economic decisions in supply chains and markets creates poorly-understood risks, especially by undermining the fundamental concept of individuality of agents.
https://cybercat-institute.github.io/2023/12/11/ai-safety-meets-value-chain-integrity/

2023-08-08 13:12:17 UTC

There seems to be a decentralisation-usability tradeoff, very similar to the security-usability tradeoff

2023-07-16 16:34:49 UTC

How in the world did people do international travel before the internet?
Like... you can't even look up hotels in the phone book, unless you happen to have a phone book for the country you're going to...