iiinova — where your digital self keeps evolving

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

My mind cannot conceive of a better break. Please tell me about yours!

Pastel de nata and Matcha Flat White (less milk, more matcha) at Matcha Lab, Munich

200

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 · 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 · 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 · 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 · 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

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

When the inevitable delay does hit, there's worse places to be than Cologne Station

100

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

Eindhoven University sure has some things going on

Full organ above a Subway in the university Auditorium

100

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

First time I had train water as well, I didn't know that was a thing! It tasted better than that description may have made it sound like

000

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

Chestnut season surely is the most beautiful, after snow season

Red-blooming chestnuts opposite Munich Residence

000

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

asan looking at my runtime code and intervening

000

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

Me when I implement an optimization and it actually goes faster

112

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

Me when there's vacation wonders to marvel at but my brain is still asleep

Sleepy cat in front of misty mountains in Alishan National Park, Taiwan

010

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

Munich 🚞 Garmisch-Classic, direct train from main station to ski lift

100

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

it cold

$River stone slowly accumulating fractalized ice around it$ Goose sleeping with head tucked in while standing on an ice sheet with one leg

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 19/11/2025

After nine months of design, implementation, and orchestration, Lean's new module system I have been working on is now live in 4.26.0-rc1 and adopted throughout Mathlib. By introducing a system for checked and enforced API boundaries between files, it allows […] [Original post on functional.cafe]

Demo of adjusting a proof somewhere deep in Mathlib followed by a rebuild that succeeds immediately after building the touched file.

Graph of Mathlib build memory usage showing continuous growth to 5.8GB over the last two years followed by a fall to 3.2GB from switching to the module system.

000

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 02/11/2025

Going to the museum to critique the artist's code

Roboter arm drawing a neon-colored picture in front of a depiction of its code printed on the wall

100

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 31/10/2025

Gonna store all my jewelry in Hilbert's Hotel going forward

BBC: Louvre robbery: Could a 50-year-old maths problem have kept the museum safe?

010

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 19/10/2025

Anything can look serene if you crop out all the people around it

Picture of a house across a lake, framed by autumn-colored trees

010

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

For a second I was convinced Mathlib had a file named VerySmallDog.lean

feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem
(mathlib4#26660)

000

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

Okay this is just too fun using `jj`: over the week I've accumulated a good amount of random fixes and improvements on a prototyping branch (pic 1). Using `jj parallelize 'ancestors(@, 5)'`, I can make them independent while keeping the ultimate contents of […] [Original post on functional.cafe]