60 Jahre 1968 minus 2: Antikriegsprotest beim Amerikahaus West-Berlin

/ Kommentieren

1968 begann heute vor 60 Jahren im Kiez der Technischen Universität Berlin. (2 Jahre zu früh also.)

Bei der ersten großen Demo gegen den Vietnamkrieg in West-Berlin am 5. Februar 1966 warfen Studierende Eier auf das Amerikahaus am Bahnhof Zoo. Die Folgen: Botschafter, die Urlaube abbrachen; Unipräsidenten und Bürgermeister, die sich in Entschuldigungen überschlugen; Springer-Kampagnen, die zur Jagd auf Studierende anstachelten.

So viel Wind um eine Packung Eier! (Angeblich von einem Schaubühnen-Mitgründer für 1,99 D-Mark erstanden.) Was sind ein paar Eier gegen einen Krieg, der drei Millionen Leben fordern wird?

Aber die Aufladung hatte natürlich Hintergründe: Die existentielle Abhängigkeit West-Berlins von den USA kollidierte mit der moralischen Verfehltheit des amerikanischen Kriegs in Vietnam. Das akademische Weltverbesserertum einerseits tanzte mit den Ressentiments rechter Milieus gegen Studierende und Unis andererseits.

Gerade die letzten Jahre in Berlin haben uns gezeigt, dass diese Abgründe noch lange nicht überwunden sind. 1968 begann in West-Berlin also zwei Jahre zu früh – und offenbar ist es immer noch nicht ganz vorbei.

Mysterium Rita Süssmuth (1937–2026)

/ Kommentieren

Ich habe Rita Süssmuth († 2026-02-01) nie ganz verstanden.

Eigentlich scheint es doch ein Naturgesetz: Genug Zeit in der Politik macht Menschen zu Arschlöchern oder zynisch oder resigniert. Mindestens ein Bisschen. Nicht so bei Rita Süssmuth – nach all ihren Jahren in höchsten Rollen bis hin zur Bundestagspräsidentin! Sie war aus einem anderen Material.

Wann immer ich sie im Kuratorium der TU Berlin aus der Nähe erlebte, und auch bei ihren öffentlichen Auftritten: Nie fehlte es ihr an Herz, Mut und Zuversicht. Umso mehr wird sie fehlen.🕯️

Rita Süssmuth bei der Leitung der TU-Kuratoriumssitzung vom 2017-06-13. Sie ließ sich von unserem kleinen Besuch (angesichts TVStud-Tarifverhandlungen) nicht aus dem Konzept bringen und machte sich beim Präsidenten (links) und anderen Kurator:innen stark dafür, auf „die jungen Leute“ zu hören.

Der Politikstil, der Rita Süssmuth gelang, ist nicht leicht nachzumachen. Ich hoffe, viele versuchen es dennoch!

Feel the magic of logic!

/ Kommentieren

Today is World Logic Day. So, I want to give some attention to one of the coolest games on temporal logics that students have developed in my TU Berlin courses.

In Tempus Fugit, you play a mage fighting monsters. 🧙‍♂️🧟 Which spells you can cast (and their strength) depends on past and future events and is expressed in a variant of linear temporal logic (LTL). LTL is one of the most important temporal logics in computer science, where it is used, for example, to describe the behavior of programs.

Play it on: https://games.equiv.io/2019wise-tempus-fugit

Should I switch from Isabelle/HOL to Lean?

/ Kommentieren

“Oh dear, better use Lean then.” — was the first response by an Isabelle core maintainer when I asked how to use Isabelle/HOL with VS Code / GitHub Copilot. … So, should one?

I’ve been an Isabelle/HOL user for 15 years, finished several projects in it, and taught it to many students and colleagues. But maybe it’s time to jump on the Lean train?

In 2021, I was at a similar crossroads. Should I formalize my PhD research in Lean or Isabelle? Lean was just upgrading from 3 to 4, disregarding structured proofs. While I like functional programming and the Curry–Howard correspondence, I don’t think the way Lean (and Rocq) double down on it helps readability. Finally, I opted for Isabelle because of its maintainable proof syntax and clarity.

Since then, Lean has continued to take off. That’s annoying for experts, as the booming community means that people keep reinventing the wheel and producing a lot of not-so-elegant stuff. Isabelle on the other hand is as walled a garden as an open source project can be. (No GitHub repo, special versioning system and tech stack. Giant barriers against drive-by pull requests and issue reports!)

The cited core maintainer is known for his particular style of communication on the mailing list—so, one should not take the offensiveness of the quoted sentence too seriously. But there’s something else about the attitude it reveals:

It seems that a maintainer writing a sentence like “Better use [our competition] then!” has already given up the fight for his system to be the one that people will use in the next decade. It tastes of seeing the writing on the wall and actively refusing to adapt to new trends, in order to not feel passive about it.

I might be totally wrong about all this. Maybe, it’s the right strategy to keep Isabelle on an island. But still, I can’t unsee the dynamic I think to see. And for me, the possibility to use a system in VS Code as well as maintainer attitude contribute to turning the scale on which system to use for my next 10000 lines of formalized math.

So, what do you think? Should one “better use Lean“? (Or Rocq? ;) Or re-learn pen-and-paper math? ;P )

Präsidentschaftswahlen an der TU Berlin und wie man aus Fehlern lernt oder nicht

/ Kommentieren

Diesen Herbst wählen die Gremien der TU Berlin ein neues Präsidium. Amtsinhaberin Geraldine Rauch kandidiert erneut. Aber drei vier weitere Bewerber:innen fordern sie öffentlich heraus.* Das ist eine bei Uniwahlen eher ungewöhnliche Situation, die ich hier fair würdigen möchte. Ich habe 15 Jahre Präsidentschaftswahlen an der Technischen Universität Berlin mitbekommen und jetzt den Luxus, von außen offener darüber nachzudenken. (Update mit neuer Bewerbung am Ende.)

weiterlesen

All the things LLMs can’t do

/ Kommentieren

“Could an LLM write your diary for you?”—That’s the question I want to ask to all those AI evangelists out there.

Whenever I check LinkedIn since opening my account three months ago, I’m bombarded with posts on AI eating everything. It’s annoying to the point that I’m now writing a post myself.

The key issue: Meaningful texts are artifacts that document human experience. They are part of our social world.

There is no point in an AI generating diary entries for you—because the purpose of such an entry is *your* thought process around it. You materialize your experiences and document them for future-you. You might also share the text on some social media site or blog. There, the audience cares about it because they care about you. The human can’t be taken out of the mix.

What is true for diary entries also applies to most genres of meaningful writing. A text that is generated without human experience is just bullshit. An LLM can’t think or experience in your place.

LLMs are great at speeding up many good things like search-heavy workflows, copy editing, translations and the like. And they are even better at plagiarism and at creating bullshit texts.

At the moment, this leads to more bullshit texts out there, and the AI grifters seem to aim for this to become the new standard of text production. But my faint hope is that now that it’s become trivial to draft bullshit texts, humanity might move beyond this genre of text altogether. 🤞

Perspektive als Wissenschaftlicher Mitarbeiter bei „Berlin ist unkürzbar“: Was ist noch garantiert?

/ Kommentieren

Mein Redebeitrag von der „Berlin ist unkürzbar“-Demo gegen die Haushaltskürzungen des Berliner Senats, 2025-02-22:

Tach allerseits, ich arbeite als wissenschaftlicher Mitarbeiter in der Informatik der TU Berlin. Dort bin ich in Mittelbauini und Kuratorium. Das Kuratorium hatte kürzlich die große Ehre, einen Haushalt zu beschließen, den der Senat postwendend rasierte.

Letzte Woche meinte Wissenschaftssenatorin Czyborra zum Tagesspiegel:

In diesen Zeiten ist es generell ziemlich schwierig, als Politikerin Garantien zu geben.

Dasselbe müssen wohl bald auch die Hochschulen sagen: Wie sollen wir Lehre und Forschung garantieren?

Wegen der Einschnitte zehrt die TU Berlin dieses Jahr ihre beweglichen Rücklagen auf. Danach ist das realistische Szenario für kurzfristiges Sparen, dass man Stellen von wissenschaftlichen Mitarbeiter:innen nicht mehr neu besetzt. Denn unsere Beschäftigtengruppe arbeitet größtenteils kettenbefristet.

weiterlesen

Yeti Tournament: Snowy team battles!

/ Kommentieren

Yeti Tournament is a small team-battle game with Yetis engaging in a snow fight. To mix things up, the Yetis have UFOs and rocket launchers at their disposal. You should definitely try it! The game is cute and arcady and features basic tactical elements.

View from above on map with snow cones for yetis to spawn at
Yeti watching others defend a giant candy cane with rocket launchers

This game has been lying around for a decade! It’s been my only Unity project, originally using Unity 3.0. While it’s kinda fun to have so much taken care of by a powerful game engine. On the other hand, the code is frozen in Unity 2017 as it’s using the discontinued UnityScript and the peer-to-peer networking system from 2012. You can read more about it’s past in the itch.io devlog.

weiterlesen

Ein Jahrzehnt Viertelparität an der TU Berlin

/ 1 Kommentar

Am Mittwoch, dem 15. Mai 2013, geschah etwas Historisches an der Technischen Universität Berlin: Der Erweiterte Akademische Senat beschloss eine neue Grundordnung, nach der dieses Gremium zukünftig viertelparitätisch besetzt würde: mit je 15 Professor:innen, 15 akademischen Mitarbeiter:innen, 15 Studierenden sowie 15 Technik- und Verwaltungsmitarbeiter:innen. Die vorherige Zusammensetzung, die vor allem bei Präsidiumswahlen ausschlaggebend ist, sieht eine Mehrheit von 31 Profs zu je 10 der anderen Gruppen vor. Verrückterweise gilt die „vorherige“ Zusammensetzung noch heute – zehn Jahre später, als wäre nichts beschlossen worden! Dabei wurde die Viertelparität gleich fünf Mal beschlossen… Wie kann das so lange dauern?!

weiterlesen

Use the boxes, trap the monsters! – Clave 0.1.0

/ Kommentieren

This is the first actual (pre-alpha) release of Clave. Finally! \o/

I originally developed this game over-night on 12/13 April 2012 in the context of a university course. The task back then was to build a minimal C#/XNA game only using circles and squares for graphics.

The game idea derives heavily from the box/circle requirement: My thinking was that the circles likely should be something that moves and that the squares would represent things blocking the movement. This lead to the idea of one circle being that tries to create an area on the map with boxes that is separated from the other circle beings.

The result actually made a lot of fun for an overnight project and also impressed the other course participants and instructors. Obviously, the code was geared towards throwaway-prototyping. But I always wanted to redo a “clean” implementation of Clave.

Thus, in 2016, I recoded the original game using Scala.js (and with browser 3d graphics using Three.js). The levels and mechanics are mostly identical with the original overnight prototype. Today’s release is mostly this version with some bug fixes and extended by support for touch devices since 2016.

I’m still hoping to extend on the mechanics one day. But for now, this pre-alpha release is just a more shiny version of the proof-of-concept game from 2012. I hope, you enjoy it anyways. It can be played directly on https://benkeks.itch.io/clave. The source is on https://github.com/benkeks/clave. Don’t let the monsters get you! :)