لا أصدق أن البشر يكتبون شيفرة Lean يدويا يا رجل. وأن الأمور كانت تتشكل فيها قبل نماذج اللغة الكبيرة. إضفاء أي شيء في Lean كان ممتعا مثل تقشير الجلد بمقشرة البطاطس، ومثيرا للاهتمام مثل مشاهدة الطلاء يجف.

لا تخبرني عن "متعة اللعبة" أو "إنها تفاعلية جدا" أو أي شيء من هذا القبيل. هناك ألعاب لها كل مكان لتراه، تماما كما يوجد الغضب في كل مكان، وأنا أعرف الفرق

@notmoeezm "لا يهمني حتى إذا كانت الأجهزة تتحقق من البراهين" المصدر: الشخص الذي يضبط خوارزميات البحث على مساحة الإثبات للمتعة، باستخدام Lean😞