Ich kann nicht glauben, dass Menschen Lean-Code manuell schreiben. Und dass Dinge darin formalisiert wurden, bevor LLMs existierten. Alles in Lean zu formalizieren fühlt sich so angenehm an wie sich die Haut mit einem Kartoffelschäler abzuziehen und so interessant wie das Trocknen von Farbe zuzusehen.

Erzähl mir nicht von "Freude am Spiel" / "es ist so interaktiv" oder was auch immer. Es gibt Spiele, in denen es überall etwas zu sehen gibt, genau wie es überall Ra*e gibt, und ich kenne den Unterschied.

@notmoeezm "Es ist mir scheißegal, ob Maschinen überhaupt Beweise verifizieren" Quelle: Typ, der Suchalgorithmen im Beweisraum zum Spaß anpasst, indem er Lean verwendet😞