Ik kan niet geloven dat mensen handmatig Lean-code schrijven, man. En dat dingen daarin werden geformaliseerd voordat LLM's bestonden. Iets in Lean formaliseren voelt net zo plezierig als je huid eraf schrapen met een aardappelschiller en net zo interessant als het drogen van verf.

Vertel me niet over de "vreugde van het spel" / "het is zo interactief" of wat dan ook. Er zijn spellen met overal wat te zien, net zoals er overal ra*e is, en ik weet het verschil.

@notmoeezm "Het kan me niet eens schelen of machines zelfs bewijzen verifiëren" bron: gast die zoekalgoritmes afstemt op bewijsruimte voor de lol, met Lean😞