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

Sunday updates: * extending the approach to 1000 modules worked well/even better; see screenshot 1 * Fable is now struggling through extending it to 10k modules (1/6th of the entire project), not unexpectedly both build times and edge cases are blowing […] [Original post on functional.cafe]

https://leanprover.zulipchat.com/#narrow/channel/416277-FLT/topic/Anthropic.20formalization.3A.20code.20analyses/near/621955721

modules 59,300
CPU time 788,017 s (218.9 CPU-hours)
instructions 3.14 x 101
wall, main run 10,463 s (2 h 54 min)
peak memory 451 GiB, largest single process 39.3 GB

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 · 06/09/2026

@soaproot Thanks, that definitely works better on other platforms...

000

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

I'm going to pause here for now because thinking about 60k modules apparently gave me quite a headache. Meanwhile Fable decided to take a peek at the slowest file in the cone and figured out a two-line shortcut instance that saves about as much in relative terms as everything above.

Screenshot of https://leanprover.zulipchat.com/#narrow/channel/416277-FLT/topic/Anthropic.20formalization.3A.20code.20analyses/near/621906329 showing new last row "shortcut Algebra [...]"

100

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

`import Mathlib` is a great way to start development on a module because it gives you everything, including invisible parts like registered simp theorems, out of the box without having to hunt for specific imports. But once development has become more stable, it only makes sense to minimize […]

functional.cafe

Original post on functional.cafe

100

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

I don't have a clear answer to the sys time collapse specifically, so Fable's guess is as good as mine: "the wrapper modules formed wide waves of short-lived processes all faulting in the same Mathlib mappings at once, and that contention, not the wrappers' own work, was most of the sys time". I […]

functional.cafe

Original post on functional.cafe

100

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

So far we have still kept the file splits as is; but when the proof file is imported only privately into only one other module, there really is not much need to keep it around as a separate file. So let's merge them (github.com/Kha/fermats-last-theorem…)! Again a few […]

functional.cafe

Original post on functional.cafe

100

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

The Modulize.lean port so far really is naive: it keeps all existing `import` directives at `public` i.e. transitively available in all downstream modules, matching non-module system semantics. But building on it, we can quite easily express something the Prove2Me paper alluded to but could not […]

functional.cafe

Original post on functional.cafe

100

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

I should highlight that one limitation of our 100-modules cone is that Mathlib size dominates it by almost two orders of magnitude while the full build is one OOM larger than Mathlib. So any effects on Mathlib importing will have outsized impact compared to importing between local modules in […]

functional.cafe

Original post on functional.cafe

100

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

Ok, let's talk about those statement/proof splits: as the paper describes, this is because "Lean recompiles the entire downstream cone whenever a module changes, even for a proof-only edit". Now, if you are following recent Lean, you might know this is no longer actually true: the module system […]

functional.cafe

Original post on functional.cafe

100

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

The low degree of parallelism is perhaps not too surprising for this small cone of the project when looking at the concrete `lake build` output: `Def_ModularCurve_CharLFrobeniusGeomLevel` alone takes about 55s, half as long as the entire build. Haven't looked at what intra-file parallelism looks […]

functional.cafe

Original post on functional.cafe

100

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

Now I haven't tried to build the entire repo yet. The readme says it took them 5hrs+ and 153GB RAM using 96 jobs, so let's maybe start with something smaller. Assuming Mathlib is already built, the following will build exactly 100 FLT modules: lake build P2M.Sol […]

functional.cafe

Original post on functional.cafe

100

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

(continent in question) (second picture for disambiguation)

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

121024273

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

This happened _twice_ in Lisbon and I wish I had had an answer that much to the point

000

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!

81102237

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

(If you are not familiar with the feature: the gray parts are server annotations of the free variables of the following term, which you can click on to convert them into actual binder syntax)

000

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

Impromptu q&a continuation by way of the following speaker not showing up, oops

000

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

Or, to give the slightly more readable version, jj rebase --source wstt --onto 'parents(wstt) ~ xklum'

000

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' ```

100

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 · 14/06/2026

@lars The queue wasn't even that long, at least compared to the Staatskanzlei. But that was already enough queuing for one day. The DDR machine of the Health Ministry OTOH had no queue...

100

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