Sebastian is the Head of Engineering at the Lean FRO, which he co-founded together with Leonardo de Moura, creator of Lean, in 2023. A Lean contributor since 2015, Sebastian was drawn to the project by its focus on general language design as well as user interaction. He wrote his PhD thesis on the design and extensibility of the user-facing “frontend” of Lean 4, the current version of Lean. He is the main author of Lean 4’s macro system Lean’s notational flexibility is based on.