iiinova — where your digital self keeps evolving

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 11/09/2026

Some 6 months after I adopted Mathlib to the module system, Mathlib will soon start warning any dependent libraries that have not yet adopted it. This will allow them to make more ambitious refactorings (e.g. github.com/leanprover-community/mat…) enabled by the module […]

functional.cafe

Original post on functional.cafe

001

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 10/09/2026

Summer is over, time for even more tea

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 06/09/2026

Today I learned that you can just rent AMD EPYC Genoa 9554P with 64 cores and 768GB RAM at $1.78/hr. That's crazy. ...well, you no longer can, at this particular provider, because I took the last one

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 05/09/2026

Let's do some performance exploration of the Anthropic FLT proof (github.com/anthropics/fermats-last-…) To set the scene, we are talking about 60,475 Lean modules in FLT on top of 8,312 already part of Mathlib. However, these two file sets are not of quite the same shape: the […]

functional.cafe

Original post on functional.cafe

102

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 02/09/2026

> A rat king lived in the tower walls, but it knew better than to send its rat knights against a Craftswoman. They knelt as she passed. I'm back to the Craft series after one more Wandering Inn book and the small-scale world building mentioned in passing (heh) is once more on point.

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 02/09/2026

The real numbers are the friends we made along the way

012

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 30/08/2026

Unethical pro-tip: use Windows paths in your commit message to make your commit go faster

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 17/08/2026

After who-knows-how-long, I have completed all top 100 25x25 puzzles in Nonograms Katana What... what do I do now

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 12/08/2026

Seems like you only need to switch continents to get asked again if you're a student

100

Reposted by Sebastian Ullrich

Tom Gauld @tomgauld.bsky.social · 01/08/2026

My latest cartoon for @newscientist.com

Panel one: a climber reaches the top of a towering cliff. There, among the clouds, a serene figure with a long beard, wearing a robe, sits crosslegged on the bare rock. He is "The Great Wise One of the Mountain"

Panels two, three and four: sitting serenely crosslegged on successively lower clifftops we see the Assistant Wise One of the Mountain, The Post-Doc Research Fellow of the Mountain and a group of PhD Students of the Mountain

121023273

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 01/08/2026

"I see you're wearing Scarpas, are you a climber?" - "No, I'm German."

100

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 31/07/2026

What, how does this Portuguese hotel have loose-leaf pu-erh. This is amazing.

000

Reposted by Sebastian Ullrich

Tom Gauld @tomgauld.bsky.social · 29/07/2026

My latest cartoon for @newscientist.com. Inspired by recent news about the SpudCell. NS subscribers can read about it here: www.newscientist.com/article/2532...

Title: The artificial cell's diary

Panel 1: An oval green cell with a face opens its eyes.
Caption: Woke up to the scientists discussing whether I was alive or just exhibiting some of the symptoms.

Panel 2: The cell looks thoughtful
Caption: A bit heavy for first thing in the morning.

Panel 3: The cell eats some little dots in the liquid around it.
Caption: Had a swim, then ate some of the molecule soup that I live in. My day is pretty much all soup-based.

Panels 4: The cell looks uncomfortable
Caption: Then I began to feel rather odd.

Panel 5 and 6: the cell hseems to be splitting in two
Caption: But, I saved the big news for last:

Panel 7: The cell smiles. A new, smaller cell smiles back.
Caption: I made a new friend!

81101237

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 25/07/2026

At the Lean workshop, Ningning Xie presented Lott, a WIP Ott-like embedded into Lean. Formal typing rules were one inspiration for the implicit quantification feature of Lean 4 so it's beautiful to see this coming full circle, properly annotated by the Lean language server.

100

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 25/07/2026

Lean workshop keynote accomplished, find me there/at ITP to ask me lots more questions!

100

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 22/07/2026

Just realized I can use jj's expressive revset language to eject a parent from a merge commit without having to look up the names of all the other parents ``` jj rebase -s wstt -d 'wstt- & ~xklum' ```

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 12/07/2026

It happens. God I love Rhythm Heaven Groove

Rhythm Heaven Groove screenshot

"some of your friends will turn into soap bubbles. It happens. But it will change the rhythm!"

000

Reposted by Sebastian Ullrich

Tom Gauld @tomgauld.bsky.social · 26/06/2026

All my New Yorker covers (2/3) They are all available on the Condé Nast Store where you can buy prints, cards, and other merch. I get a royalty from this. www.condenaststore.com/art/tom+gauld

The New Yorker
‘On the beach’
cover by Tom Gauld
Description 'Panels of people arriving, sunbathing, swimming and finally leaving the beach'

The New Yorker
‘Winter Garden’
cover by Tom Gauld
Description 'Woman watering plants in an indoor garden on a rainy winter day'

The New Yorker
‘Dog walking 2.0’
cover by Tom Gauld
Description 'Robot walking a dog in the park comes upon a woman walking a robot dog'

The New Yorker
‘Rooftop Astronomy’
cover by Tom Gauld
Description 'Panels depicting an adult and a child looking at the stars from a rooftop telescope'

433147

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 18/06/2026

I did *not* know that ctest records test timings and uses them to optimize future test run scheduling. Extremely pleasing to see how it manages to make all cores finish at almost the same time, except for those running the most expensive tests

Perfetto rendering of a Lean test suite run showing expensive tests being scheduled first

001

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 13/06/2026

I just don't know about this mode of swordfighting

100

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 12/06/2026

Pretty sure I just encountered a liminal space: both subway tracks were blocked by trains (the ancient edition, just to drive the point home), neither of which could be boarded. Bonus points for mirror on top.

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 10/06/2026

Had a great time listening to Tom Gauld @tomgauld.bsky.social talk about his work and workflow at today's reading in Munich "I basically drink coffee until I have an idea or I get sick" fed.brid.gy/r/https://bsky.app/prof…

Tom Gauld in front of a projection of his sketchbook

120

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 03/06/2026

Munich🚄Eindhoven for the Dutch Formal Methods Day! I made sure to have at least one reference to the Netherlands in my talk just to be on the safe side...

200

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 30/05/2026

For your consideration: not one but TWO cute & delightful puzzle games store.steampowered.com/bundle/58864…

CATÖoo bundle (CATO + Öoo) on Steam, 28% off

110

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 28/05/2026

Sometimes you still find surprisingly low-hanging perf fruits in unexpected places. There is a linter in Mathlib that did something not unreasonable before I implemented parallel elaboration in Lean. When I did so, some amount of task-clock increase was of course expected and so a single linter […]

functional.cafe

Original post on functional.cafe

000

Reposted by Sebastian Ullrich

nosfe @nosfe.kamu.social.ap.brid.gy · 18/05/2026

so, umm, this is a 16 bytes intro 16 bytes !!!!!!!!!!!!!!!! www.youtube.com/watch?v=MvycyU-kLjg #demoscene #intro

2127

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 17/05/2026

When the recipe is missing a crucial measurement and you just go by intuition

A Bördy water drip styled as a bird neatly nestled among basil plants

A Bördy XL completely dominating a small pot hosting a few meek basil sprouts

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 14/05/2026

TIL that "mesmerize" comes from the name of Franz Mesmer, 18th-century physician ...who believed in an all-permeating force field that he could manipulate www.bbc.co.uk/programmes/m002cqq3