Post by Thomas Kahle

Hmm. https://github.com/openai/math hat trotz Inklusion von kompilierten PDF files mehr als 3 mal so viele Sterne wie https://github.com/leanprover-community/mathlib4/

Das kann doch so nicht bleiben Leute. Stern bedeutet “Fav” auch auf GitHub !!!

Jetzt wollte ich das all modern infrastructure xkcd einbauen hier mit alle AI Resultate basieren auf lean. Aber das habe ich dann nicht gemacht, weil lean ja kein wackeliger kleiner Balken ist sondern super-solide Foundation ohne die die ganzen KI-Firmen nicht wären wo sie sind.

@tomkalei

Dann schreibe doch 'lean' an die starke Seite des XKCD-Comics und 'Running out of tokens' an die schwache, wackelige Seite. 😉