> The suggestion engine (korb suggestion threshold) is re-implemented in Lean 4 with five mathematically proven properties: suggestions have positive frequency, are sorted descending, come from ordered and available products, exclude basket items, and respect the count limit.

This is amazing. I mean this literally in that I am amazed, but also figuratively in that I am delighted to watch the type-safe-mad build cool shit.