Knuth la ut en artikkel som fremhever en veldig kul AI-bruk som middelmådige, dessverre, kaller vibemathing. Det er det motsatte av «vibe-» noe som helst: Det som skjedde var at Filip Stappers ga problemet til Claude med en veldig stram selvreflekterende løkke, ordrett: ** Etter HVER exploreXX py-gjennomspilling, oppdater denne filen UMIDDELBART [plan md] før han gjorde noe annet. ** Ingen unntak. Ikke start neste utforskning inntil den forrige er dokumentert her. Og så verifiserte de nøye hver av 31 løkker. Og etter den siste løkken, som så ut til å være vellykket, skrev Knuth et faktisk formelt bevisteorem for å fullstendig verifisere resultatene. Dette er ekte matematikk med bruk av elektriske verktøy, det er superkult! Jeg tror det er ganske trygt å si at formell bevisforskning vil vise seg (haha, skjønner) å være veldig viktig i en tid med hallusinerende maskiner.