Sebastian Ullrich

Snow makes me just so happy

Leave it to DB to figure a 60min delay into the 80min train ride though

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

Screenshot of slide code block showing a RISC V assembler program embedded into the statement of a Lean theorem followed by a Hoare-style specification

Sweet embedding of RISC V asm at Lean Together

https://researchseminars.org/talk/LT2026/37/

Tantris Restaurant dragon statues lightly covered in snow and lit by the morning sun from behind

Good morning. Very good.

River stone slowly accumulating fractalized ice around it

Goose sleeping with head tucked in while standing on an ice sheet with one leg

it cold

Clear sky showing criss-crossing airplane contrails

Safe travels, everyone

Photo of whiskey glass with "A WEE DRAM" printed on it

Like, 4GB?

@JacquesC2 I believe you mentioned to me back in Bonn that you have/know a paper about comparing benchmark results against historic data for significance detection, could you remind me which one it was?

I'm at Frankfurt Airport and the two things I spotted on the airport TV before I thought of better things to do again were

* a big football stadium banner "DIE FANS"
* a supercut of the 7:1 GER:BRA game

Someone is *not* optimizing this stream for international audiences!

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.

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]

Picture of sunset painting red wavy lines on the clouds

wavy

Photo Bahnhof Mengen, nix los

Mengen, Leere

@fmontesi will be the first director of the new Centre for Formal Methods and Future Computing (FORM)!

Among other things, the Centre will work on the development of Lean's CS Library, where Fabrizio already serves as a member of the steering committee.

Interested in research in formal […]

"Whoa he even defined a class... oh, it has instance methods but no fields"

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

Going to the museum to critique the artist's code

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

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

Steps to Reproduce 1. Cause a global AWS outage 2. Run `lake init pkg math`

Easy reproducer

Ist Ladesäule eigentlich der schwäbische Diminutiv von Ladesau

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

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

With a Settlers cameo even

Another new Map Men already? We are truly blessed

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

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

Wispy

For my new job, I am looking for a flat in Munich from January or February, 2026.
Please let me know if you or someone you know is looking for a new tenant. Retoot much appreciated!

Here are the rough parameters I am looking for in a flat:
Rent (warm) […]

[Original post on social.tr0llhoehle.de]

ein goldgelbes Lindenblatt, und drumherum auf den Dielen drei Fabeltiere aus Eicheln, Bucheckern, Lindensamen und Blättern.

#silentsunday

@andrejbauer I didn't think an actual nightmare-inducing toot could exist

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

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]

Wait why does one out of four British Airways flights have classical music during boarding? What are they plotting?