Sebastian Ullrich
LightNews LightNews
banner
kha.functional.cafe.ap.brid.gy
Sebastian Ullrich
@kha.functional.cafe.ap.brid.gy
35 followers 0 following 120 posts
makes Lean at Lean FRO

Munich, Germany

[bridged from https://functional.cafe/@kha on the fediverse by https://fed.brid.gy/ ]
Posts Replies Media Videos
kha.functional.cafe.ap.brid.gy
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.
November 19, 2025 at 1:39 PM
kha.functional.cafe.ap.brid.gy
wavy
Picture of sunset painting red wavy lines on the clouds
November 11, 2025 at 4:00 PM
kha.functional.cafe.ap.brid.gy
Mengen, Leere
Photo Bahnhof Mengen, nix los
November 9, 2025 at 11:46 AM
kha.functional.cafe.ap.brid.gy
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
November 2, 2025 at 3:48 PM
kha.functional.cafe.ap.brid.gy
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?
October 31, 2025 at 10:28 AM
kha.functional.cafe.ap.brid.gy
Easy reproducer
Steps to Reproduce 1. Cause a global AWS outage 2. Run `lake init pkg math`
October 21, 2025 at 11:36 AM
kha.functional.cafe.ap.brid.gy
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
October 19, 2025 at 4:09 PM
kha.functional.cafe.ap.brid.gy
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)
October 9, 2025 at 12:24 PM
kha.functional.cafe.ap.brid.gy
Wispy
October 8, 2025 at 4:35 PM
kha.functional.cafe.ap.brid.gy
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]
A jj history of 5 linear changes The 5 changes now on separate paths, merging back together in the end The changes with PRs attached
September 5, 2025 at 1:51 PM
kha.functional.cafe.ap.brid.gy
"You don't need a .pkpass, just use our app!"

The app:
British Airways, 1.2 stars
August 11, 2025 at 6:41 AM
kha.functional.cafe.ap.brid.gy
Nice

https://tenpages.github.io/us-level/eu.html
"Europe Level 69" according to countries visited
August 10, 2025 at 3:24 PM
kha.functional.cafe.ap.brid.gy
What building current Mathlib from scratch on a 32-hardware threads machine looks like
Perfetto UI showing thousands of Mathlib modules closely packed together being built across 32+ threads. After 15 minutes, the degree of parallelism drops to ~10 threads on average when only the "critical path" and some related modules remain, finishing after 6 more minutes.
August 3, 2025 at 3:19 PM
kha.functional.cafe.ap.brid.gy
Brief respite from the rain. What a summer!
A small slice of sun peaks out from below dark clouds and alights a wet street and surrounding buildings in Maxvorstadt, Munich
August 2, 2025 at 11:33 AM
kha.functional.cafe.ap.brid.gy
Me, sophisticated: "Parmesan demon core"
Stock photo of pasta alla ruota made in hollowed-out cheese wheel
July 29, 2025 at 5:58 PM
kha.functional.cafe.ap.brid.gy
My friends were kind enough to leave my body with the capybaras
Screenshot of Peak showing a player character leaving behind another character swimming upside down in a hot spring with three capybaras
July 22, 2025 at 8:54 PM
kha.functional.cafe.ap.brid.gy
We were in a wildlife park on Friday and the responsibility fell to me to explain the concept of Flat Fuck Friday
Picture of a very flat raccoon
July 20, 2025 at 12:02 PM
kha.functional.cafe.ap.brid.gy
We are well-equipped at the office. We have booths for both large land mammals as well as French people.
A photo of two booths saying "ELEPHONE" and "LEPHONE"
July 16, 2025 at 7:35 AM
kha.functional.cafe.ap.brid.gy
And finally a minimum viable demo, fast-forwarding through rebuilding some 1030 files on trivial changes to the `Init.Prelude` root file
Screen recording on VS Code. In the top half, I do simple changes to a Lean file: adding whitespace, comments, changing proofs. In the bottom file, the library is automatically rebuilt on each file save, always skipping immediately to the end after the touched file has been rebuilt.
July 5, 2025 at 3:07 PM
kha.functional.cafe.ap.brid.gy
Took me a while to notice what it reminded me of...
Image from Neon Genesis Evangelion: the Magi computers are being taken over by a virus
July 4, 2025 at 5:52 PM
kha.functional.cafe.ap.brid.gy
I made a lil visualization of how far I've already spread the module system through the Lean std libs
A directory tree map showing ported files in orange, with `Init` fully ported, `Std` mostly, and `Lean` starting to
July 4, 2025 at 5:49 PM
kha.functional.cafe.ap.brid.gy
Unhappy little bike
June 27, 2025 at 7:04 AM
kha.functional.cafe.ap.brid.gy
Happy big train
ICE train with rainbow strip
June 27, 2025 at 7:03 AM
kha.functional.cafe.ap.brid.gy
who is little friend under table
June 17, 2025 at 7:50 AM
kha.functional.cafe.ap.brid.gy
"It's good enough" - Buger Buger
June 17, 2025 at 7:47 AM