Nu pot să cred că oamenii scriu cod Lean manual, omule. Și că lucrurile erau formalizate în el înainte de LLM-uri. Formalizarea oricărui lucru în Lean se simte la fel de plăcută ca și cum ți-ai curăța pielea cu un decojător de cartofi și la fel de interesantă ca privirea vopsea uscându-se.

Nu-mi spune că nu există "bucuria jocului" / "e atât de interactiv" sau ceva de genul. Există jocuri cu oriunde de văzut, la fel cum este ra*e peste tot, și știu diferența

@notmoeezm "Nici măcar nu-mi pasă dacă mașinile verifică dovezile" Sursa: Tip care ajustează algoritmii de căutare pe Proof Space de plăcere, folosind Lean😞