‏سقوط «اقتصاد قضیه»؛ چطور AI ریاضی رو نابود می‌کنه و بهش دست نمی‌زنه

این مطلب یه جستار بلند از دیوید بسیسه؛ ریاضیدانی که آکادمی رو ول کرده و یه استارتاپ یادگیری ماشین زده. اون با چند خاطره از کار خودش شروع می‌کنه تا یه نکته رو جا بندازه: سخت‌ترین بخشِ کارِ ریاضیدان، اثباتِ قضیه نیست. به گفتهٔ اون، بارها می‌دونسته یه قضیه درسته و اثباتش هم سرراست بوده؛ کار سخت این بوده که شهود بزنه «یه چیزی این‌جا هست» و بعد چارچوب مفهومی و تعریف‌هایی بسازه که اون ایده توش راحت بیان شه.

بسیس این تمایز رو با دو مفهوم توضیح می‌ده: ریاضیِ رسمی و ریاضیِ پنهان. رسمی همون سیستم استنتاجیه که از اصول موضوع شروع می‌کنی و مکانیکی قضیه درمیاری؛ سرد، منطقی و عینی. پنهان بخش انسانیِ ماجراست: چرا این سیستم اختراع شده، چطور باهاش کار می‌کنیم و با چه ترفندهای ذهنیِ عجیبی مرزهاش رو جلو می‌بریم. مشکل اینه که ریاضیِ پنهان هیچ‌وقت وارد برنامهٔ درسی نشده و کم‌ارزش شمرده می‌شه.

نویسنده اسم این وضعیت رو «نفرینِ هاردی» می‌ذاره؛ به این اشاره که سیستم به‌طور بیمارگونه فقط به تقدمِ اثباتِ قضیه بها می‌ده و کار مفهوم‌سازی و تفسیر رو دست‌کم می‌گیره. اون از بیل ترستون، برندهٔ مدال فیلدز، نقل می‌کنه که «محصول ریاضی، وضوح و فهمه، نه صرفِ قضیه‌ها». به گفتهٔ بسیس، این «کد افتخار» فقط برای این دوام آورده که به سلامت و شایسته‌سالاریِ رشته کمک می‌کرده، اون‌هم چون تا حالا مفهوم‌سازی و حلِ مسئله تقریباً همیشه دست‌به‌دستِ هم می‌رفتن.

نقطهٔ عطف جستار، سخنرانیِ جفری هینتونه که ریاضی رو یه «سیستم بسته» مثل شطرنج و Go توصیف کرده و گفته AI ظرف ده سال ازش جلو می‌زنه. بسیس می‌گه همین دیدگاه توضیح می‌ده چرا استارتاپ‌های «AI برای ریاضیِ محض» با این‌که بازارشون کوچیکه، پول‌های نجومی جذب می‌کنن: اگه همه باور کنن ریاضی یه سیستم بسته‌ست، پیچِ سرمایه‌گذاری می‌شه «ما Go و شطرنج رو حل کردیم، حالا ریاضی رو حل می‌کنیم».

بعد سراغ پروژهٔ First Proof می‌ره؛ یه تیم از ریاضیدان‌های سطح‌بالا که ده «سؤال پژوهشی» منتشر کردن تا ببینن AI مستقل (بدون متخصص در حلقه) کجا وایساده. بسیس چند هشدار مهم می‌ده: اول این‌که اون سؤال‌ها در واقع لم‌های فنی بودن نه مسائل عمیق، و بینِ یه لم تا یه مقالهٔ جدی تا یه دستاورد بزرگ «اقیانوس» فاصله‌ست. دوم و مهم‌تر، مسئلهٔ افزایندگی (accretiveness) هست.

این‌جا هستهٔ استدلالشه: مشکلِ اثبات‌های نامفهوم فقط درستیِ اون‌ها نیست. حتی اگه یه اثباتِ AI درست باشه، وقتی نامفهوم و بی‌ایده‌ی روشن باشه، به بدنهٔ دانش ریاضی «افزوده» نمی‌شه؛ چون اثبات‌های انسانی معنادار و جهت‌دار‌ درستن و باگ‌هاشون قابل‌مهار و رفع‌شدنیه. حتی خودکارسازیِ صوری‌سازی (autoformalization) با ابزارهایی مثل Lean هم به گفتهٔ اون این خلأ رو پر نمی‌کنه. نتیجه‌گیریِ بسیس اینه که AI ممکنه به‌زودی قضیه‌ها رو تولید کنه و اقتصادی که فقط قضیه رو می‌خرید فرو بریزه، ولی کار واقعیِ ریاضی، یعنی ساختن فهم و مفهوم، دست‌نخورده بمونه.

نکات کلیدی:

• به گفتهٔ نویسنده، بخش سختِ ریاضی مفهوم‌سازی و شهوده، نه اثباتِ قضیه
• تمایز میان «ریاضیِ رسمی» (استخراج مکانیکی) و «ریاضیِ پنهانِ» انسانی و مفهومی
• سیستم پاداشِ رشته فقط به قضیه ارزش می‌ده و همین آسیب‌پذیری رو AI نشونه گرفته
• اثبات‌های نامفهومِ AI حتی اگه درست باشن، به بدنهٔ دانش «افزوده» نمی‌شن
• نویسنده می‌گه AI «اقتصاد قضیه» رو فرو می‌ریزه ولی به قلب واقعیِ ریاضی دست نمی‌زنه