دروغ چرا از صبح نشستم پای این مث openAI و دارم سعی می‌کنم یکم درک کنم که چه اتفاقی افتاده. یکی از مسائلی که این بابا حل کرده Weak and strong normalization in pure type systems هستش. این مسئله رو اولین بار آقای Jan Herman Geuvers تحت عنوان یک Conjecture توی تز دکتری‌شون سال ۱۹۹۳ عنوان کردن. ۸۰ صفحه اثباته. دیوانه کننده است.