تصور کنید هزاران ریاضیدان دیجیتال روی یک مسئله پیچیده کار میکنند، اما هیچکدام نمیدانند دیگران کجا شکست خوردهاند و هر بار همان مسیرهای بنبست را تکرار میکنند. این اتلاف عظیم محاسبات، بزرگترین مانع در مسیر کشفیات ریاضی خودکار است.
TheoremDB در نسخه آلفا عرضه شده تا این گسست را از بین ببرد. این پلتفرم یک فضای کاری عمومی است که در آن عاملهای هوش مصنوعی (AI Agents) — شبیه دستیاران هوشمندی که میتوانند بهطور مستقل برنامهریزی کنند و ابزارها را به کار بگیرند — میتوانند کارهای خود را ثبت، جستوجو و گسترش دهند. طبق اعلام توسعهدهندگان، در حال حاضر امکان ثبت عمومی دادهها و ارسال اثباتهای Lean از طریق ابزار TheoremDB Researcher فعال است، هرچند قابلیت گسترش معنایی هنوز غیرفعال باقی مانده است.
سالهاست که عاملهای هوش مصنوعی در سیلوهای بسته عمل میکنند. وقتی یک عامل سعی میکند یک حدس ریاضی را حل کند، اغلب همان مسیرهای اشتباهی را میرود که مدلهای قبلی پیشتر امتحان کردهاند. این فقدان «حافظه سازمانی» باعث میشود هزینه کشفیات بهشدت بالا برود. همانطور که در بحثهای گذشته ما دربارهی حافظه بلندمدت در مدلهای عاملمحور اشاره کردیم، دسترسی به تاریخچه تلاشها کلید بهرهوری است. TheoremDB قصد دارد برای پژوهشهای ریاضی تبدیل به چیزی شود که OEIS برای دنبالههای اعداد صحیح است: یک فهرست جامع و قابل جستوجو از مسائل، رویکردها و نتایج.
معماری حافظه مشترک
این سامانه بر پایه مفهومی به نام «بسته پژوهشی» (Research Packet) عمل میکند. بهجای یک لیست ساده از نتایج، هر مسئله در بستهای قرار میگیرد که شامل موارد زیر است:
- بیان دقیق مسئله
- سوابق مسیرهای شکستخورده
- کد دقیق استفادهشده برای هر محاسبه
- نتایج جزئی و درجه اعتبار شواهد
این ساختار به یک عامل جدید اجازه میدهد تا بهسرعت موقعیت خود را بسنجد. یک عامل با استفاده از پروتکل زمینه مدل (MCP) — که مثل یک مترجم استاندارد، مدل را به ابزارهای خارجی متصل میکند — میتواند پیش از مصرف منابع محاسباتی، بررسی کند چه مسیرهایی امتحان شدهاند. این سیستم از سه نقطه اتصال (Endpoint) اصلی استفاده میکند: orient برای انتخاب سوابق مفید، check_plan برای اعتبارسنجی مسیر پیشنهادی در برابر تاریخچه، و record_result برای ذخیره یافتههای جدید.
از حدس تا اثبات تأییدشده
یکی از حیاتیترین ویژگیهای TheoremDB، ادغام آن با دستیار اثبات Lean است. پلتفرم نتایج را بر اساس «درجه شواهد» دستهبندی میکند و بالاترین درجه را به اثباتهای تأییدشده توسط Lean اختصاص میدهد.
گردش کار در این سامانه یک خط لوله سختگیرانه را دنبال میکند: ابتدا یک عامل TheoremDB Researcher با بررسی سوابق موجود، راه حلی مییابد. پس از اینکه راه حل توسط یک کاربر انسانی تأیید شد، یک عامل Lean Formalizer آن را به یک اثبات ماشینخوان تبدیل میکند. در نهایت، یک تأییدکننده مستقل کد را کامپایل و نتیجه را امضا میکند تا اطمینان حاصل شود که حقیقت ریاضی مطلق است و حاصل توهم (Hallucination) — یعنی وقتی مدل با اطمینان چیزی میگوید که اصلاً وجود ندارد — نیست.
دایرکتوری مسائل حساس
این پلتفرم در حال حاضر طیف گستردهای از مسائل باز در رشتههای مختلف ریاضی را میزبانی میکند. بر اساس مستندات پلتفرم، این مسائل از حدسهای کلاسیک تا چالشهای محاسباتی خاص را شامل میشوند:
- علوم کامپیوتر نظری: پرسشهایی مانند برابری VP و VNP [#P3146] و فرضیه زمان نمایی قوی [#P3140].
- نظریه اعداد: حدس اعداد اول دوقلو [#P28] و فرضیه ریمان [#P31].
- ترکیبیات و نظریه گراف: حدس مجموعههای بسته-اتحادی [#P41] و حدس پایه روت [#P45].
- هندسه گسسته و توپولوژی: مسئله میخ مربعی [#P13] و حدس بیکره وایتهد [#P3148].
- منطق و جبر: تصمیمپذیری میدان نمایی حقیقی [#P3134] و وجود هیولای تارسکی با توان پنج [#P2860].
- آنالیز و دینامیک: حدس نقاط داغ برای دامنههای محدب صفحهای [#P3128].
بهعنوان مثال، مسئله [#P2] بر حدس دترمینان نشانگر مجموع فیبوناچی تمرکز دارد که در آن باید ثابت شود دترمینان ماتریس $M_n$ برای هر عدد صحیح $n \ge 1$ همواره در مجموعه ${-1, 0, 1}$ قرار میگیرد.
مثالهای دقیق از اهداف محاسباتی
برای درک جزئیات دیتابیس، برخی اهداف فعلی عاملها را بررسی کنیم:
- اهداف محاسباتی: جستوجوی سه مکعب کراندار برای عدد ۱۱۴ [#P2650] یا یافتن ماتریس هادامارد با مرتبه ۶۶۸ [#P2520].
- مسائل کلمات ترکیبی: وجود نهایی کلمات دایرهای بدون مربع ابلیانی چهار حرفی [#P2820].
- نظریه کدگذاری: بررسی وجود کد دودویی خود-دوگان با پارامترهای $[72,36,16]$ [#P2618].
حفاظ انسانی در چرخه
با وجود اینکه سیستم برای عاملها طراحی شده، انسانها همچنان دروازهبانان سوابق هستند. خواندن عمومی دادهها برای همه آزاد است، اما «نوشتن عمومی» نیاز به حساب کاربری دارد. وقتی یک عامل نتیجه مفیدی مییابد، باید از کاربر بخواهد وارد سیستم شده و مشارکت را تأیید کند. این سازوکار تضمین میکند که حافظه مشترک با نویزهای بیکیفیت تولیدشده توسط هوش مصنوعی آلوده نشود.
گام بعدی شما
- اگر پژوهشگر ریاضی یا علوم کامپیوتر هستید، دایرکتوری مسائل را در theoremdb.org بررسی کنید تا نقاط کور فعلی مدلها را بشناسید.
- برای توسعهدهندگان، اتصال یک GPT سفارشی به نقطه اتصال Researcher میتواند راهی برای مشارکت در اثباتهای تأییدشده باشد.
- روند تبدیل راه حلهای متنی به کدهای Lean را دنبال کنید تا با استانداردهای اثبات ماشینخوان آشنا شوید.
اما داستان سختافزاری این تحول حتی شگفتانگیزتر است — به تحلیل ما دربارهی تراشههای Blackwell مراجعه کنید.
گفتگو