تصور کنید پیچیدهترین استدلالهای ریاضی که تا به حال توسط انسانها نوشته شده، حالا توسط یک ماشین خط به خط بررسی و تأیید شوند. این دیگر یک رویای نظری نیست؛ بلکه واقعیتی است که با تأیید رسمی قضیه فاصله اعداد اول ۲۴۶ محقق شده است. در حالی که اثبات اینکه بینهایت جفت از اعداد اول وجود دارند که فاصله آنها از یکدیگر حداکثر ۲۴۶ است، از نظر فنی دشوارترین بخش نظریه اعداد مدرن محسوب میشود، اکنون توسط یک سیستم هوش مصنوعی بهطور رسمی تأیید شده است.
طبق گزارش IEEE Spectrum، شرکت Axiom Math در ۱۷ اوت ۲۰۲۶، اثباتی ماشینخوان در زبان Lean 4 را منتشر کرد که این قضیه را به طور کامل تأیید میکند. این نتیجه، لبهی فعلی دانش بشر در مورد «حدس اعداد اول دوقلو» (Twin Prime Conjecture) است؛ فرضیهای از قرن نوزدهم که پیشنهاد میکند اعداد اولی که فاصله آنها دقیقاً ۲ است، تا ابد تکرار میشوند. اگرچه این حدس هنوز به طور کامل ثابت نشده است، اما کران ۲۴۶ نشاندهنده مرز مطلق دانش فعلی انسان است. کن اونو، ریاضیدان مؤسس Axiom Math، در این باره میگوید: «این قضیه در حال حاضر نشاندهنده آستانه دانش بشر درباره اعداد اول است.»
تأیید رسمی (Formal Verification) با داوری سنتی همکاران متفاوت است. در اینجا، اثبات به زبانی ترجمه میشود که یک «هسته مورد اعتماد» (Trusted Kernel) — برنامهای کوچک و بسیار دقیق — میتواند آن را بدون خطای انسانی خط به خط بررسی کند. به نقل از Axiom Math، این فرآیند احتمال خطای انسانی را از زنجیره تأیید حذف میکند، هرچند صحت نهایی همچنان به ترجمه درست صورتمسأله اصلی و سلامت خودِ برنامه بررسیکننده وابسته است.
شکاف موجود در ریاضیات هوش مصنوعی
تا پیش از این، سامانههای هوش مصنوعی که در بنچمارکهای ریاضی با یکدیگر رقابت میکردند، عمدتاً بر مسائل مسابقاتی تمرکز داشتند. این مسائل معمولاً دارای اثباتهای کوتاه و مجزایی هستند که در یک چارچوب بسته تعریف شدهاند.
همانطور که در تحلیلهای پیشین ما دربارهی مدلهای استدلالی اشاره کردیم، شکاف عمیقی میان نتایج بنچمارکها و رسمیسازی در سطح پژوهشی وجود داشت. این الگو در سیستمهای اولیه مشهود بود که در هندسه المپیاد میدرخشیدند، اما ریاضیات پیچیده پژوهشی را تا حد زیادی دستنخورده باقی گذاشته بودند. این چالشها باعث شد تا نیاز به زیرساختهایی برای مدیریت دانش ریاضی احساس شود، مشابه آنچه در پروژه TheoremDB برای تبدیل تلاشهای شکستخورده به پایگاه دادههای تأییدشده مشاهده میکنیم.
مسیر رسیدن به عدد ۲۴۶
دستیابی به این عدد، حاصل دههها تلاش انسانی بود که اکنون توسط هوش مصنوعی بازسازی شده است. این حدس ابتدا توسط آلفونس دو پولینیاک در قرن نوزدهم بهطور دقیق فرمولبندی شد. مسیر رسیدن به کران فعلی به شرح زیر است:
- ۲۰۱۳: ییتانگ ژانگ نخستین کران متناهی از هر نوع را تعیین کرد و ثابت کرد بینهایت جفت عدد اول وجود دارند که فاصله آنها از یکدیگر حداکثر ۷۰ میلیون است.
- اواخر ۲۰۱۳: جیمز مینارد با معرفی یک روش غربال اصلاحشده، این کران را به ۶۰۰ کاهش داد. این اثر پژوهشی در نهایت به دریافت مدال فیلدز او در سال ۲۰۲۲ کمک کرد.
- پروژه Polymath8b: یک همکاری گسترده شامل مینارد و ترنس تائو که توانست این کران را از ۶۰۰ به ۲۴۶ کاهش دهد و تنگتر کند.
صفحه پروژه Axiom Math این اثر را به عنوان یک رسمیسازی یکپارچه از مقاله سال ۲۰۱۳ مینارد با عنوان «فاصلههای کوچک بین اعداد اول» (Small gaps between primes) و بخشهای مرتبط از پیگیریهای پروژه Polymath8b توصیف میکند.
خط لوله AxiomProver
شرکت Axiom Math برای رسیدن به این رسمیسازی از یک خط لوله سه مرحلهای استفاده کرد:
- مرحله طرح (Blueprint): پژوهشگران ابتدا اثبات را بهصورت یک طرح کلی نوشتند. هر تعریف، لم و قضیه دارای یک برچسب، بیان دقیق و فهرستی از وابستگیها بود. این کار منجر به ایجاد یک گراف وابستگی شد تا ترتیب اجرای مراحل کار مشخص شود.
- مرحله تولید (Generation): سامانه AxiomProver — یک سامانه چندعاملی (Multi-agent System) برای پژوهشهای ریاضی از طریق اثبات رسمی — اثباتهای ماشینخوان Lean 4 را تولید کرد. این فرآیند بر پایه Mathlib (کتابخانه ریاضیات جامعه) و پروژه PrimeNumberTheoremAnd بنا شد که یک پروژه رسمیسازی موجود به رهبری الکس کنتوروویچ و ترنس تائو بود.
- مرحله بازبینی (Review): تیمی متشکل از ۴۱ مشارکتکننده نامبرده در حوزههای ریاضی، مهندسی و محققان ارشد (PI)، کدهای تولید شده را بازبینی و آنها را در یک کتابخانه عمومی سازماندهی کردند.
جزئیات کتابخانه PrimeGapsLib
کتابخانه عمومی حاصل، یعنی PrimeGapsLib، اکنون میزبان قضیه ۲۴۶ است، اما دستاوردهای این کتابخانه فراتر از این عدد شاخص است:
- کرانهای متعدد: علاوه بر کران ۲۴۶، این کتابخانه کران ۶۰۰ مینارد را نیز رسمیسازی کرده است.
- چالش تأیید: این مجموعه شامل یک چالش مستقل است که تنها بر پایه Mathlib بنا شده است. در این چالش، جایگاه اثبات خالی گذاشته شده تا هر کسی که به ابزار مقایسهگر Lean دسترسی دارد، بتواند بهطور مستقل تأیید کند که اثباتها با قضایای بیانشده مطابقت دارند.
- نیازمندیهای محاسباتی: شرکت هشدار داده است که بررسی کامل این اثباتها ممکن است چندین ساعت زمان ببرد، هرچند نسخههای کاهشیافته که دو نتیجه دیگر را پوشش میدهند، در عرض چند دقیقه اجرا میشوند.
زیرساخت در برابر دستاوردهای تکموردی
این دستاورد در سالی رخ میدهد که ادعاهای زیادی درباره توانایی هوش مصنوعی در انجام ریاضیات در سطح پژوهشی مطرح شده است. اما اکثر این ادعاها به اثباتهای کوتاه یا نمرات بنچمارکهای مسابقاتی محدود میشوند. Axiom Math در این فضا جسورانه عمل کرده و ادعا میکند که AxiomProver مسائل باز قبلی و چندین مسئله قدیمی اردوش (Erdős) را حل کرده است که برخی از آنها در مجلات داوریشده منتشر شدهاند.
این نتیجه با دستاوردهای قبلی هوش مصنوعی در ریاضیات متفاوت است؛ برای مثال، شرکت Math, Inc. از عامل Gauss خود برای اثبات نتایج بستهبندی کره مارینا viazovska در ابعاد ۸ و ۲۴ (که منجر به مدال فیلدز او شد) استفاده کرده بود.
سیدهارث هاریاران، دانشجوی دکتری دانشگاه کارنگی ملون که رهبری تلاشهای انسانی برای طرح کلی پروژه بستهبندی کره را بر عهده داشت و اکنون کارآموز Axiom Math و مشارکتکننده در پروژه ۲۴۶ است، استدلال میکند که PrimeGapsLib دستاوردی جامعتر است. دلیل او این است که Axiom برای «قابلیت استفاده مجدد» ساخته است. بهجای یک رسمیسازی تکموردی از یک اثبات واحد، این سیستم یک کتابخانه نگهداریشده از نتایج را ایجاد کرده که هدف آن حمایت از پژوهشهای آینده است.
این چرخش نشان میدهد هوش مصنوعی از حل تمرینهای مجزا به سمت ساخت زیرساختهای رسمی مورد نیاز برای پژوهشهای آینده حرکت میکند. ادعای توانمندی در اینجا نه بر اساس نمره بنچمارک، بلکه بر اساس مصنوعات عمومی و قابل اجرا — یعنی طرح کلی، کد Lean و چالش مقایسهگر — استوار است.
فراتر از نظریه اعداد
کن اونو، ریاضیدان مؤسس، این پروژه را آزمایشگاهی برای هدفی بزرگتر میبیند. او معتقد است اگر ویژگیهای نرمافزاری — مانند اینکه آیا یک برنامه متوقف میشود یا اینکه آیا خروجی آن برای هر ورودی صحیح است — بتوانند بهصورت گزارههای ریاضی دقیق بیان شوند، AxiomProver میتواند کدهای تولید شده توسط هوش مصنوعی را که زیرساختهای جهانی را اداره میکنند، بهصورت رسمی تأیید کند.
اونو هشدار میدهد که جهان به سمتی میرود که سیستمهای حیاتی در امور مالی، امنیت و زیرساختها بر اساس کدهایی اجرا شوند که هیچ انسانی آنها را نخوانده است. او میگوید: «هوش مصنوعی اینجاست و ما دیگر نمیتوانیم چشمپوشی کنیم — رسمیسازی اثباتها، آزمایشگاهی برای حل چیزی است که به نظر من مهمترین چالشی خواهد بود که در مواجهه با هوش مصنوعی با آن روبرو میشویم.»
در حال حاضر، خروجی این پروژه یک طرح کلی با ۴۱ نویسنده و یک اثبات ماشینتأیید شده است که نشان میدهد اعداد اول با فاصله ۲۴۶ از یکدیگر هرگز تمام نمیشوند. این اثر به عنوان عمیقترین قطعه از ریاضیات پژوهشی است که تاکنون یک سیستم هوش مصنوعی توانسته است از ابتدا تا انتها بررسی کند.
گام بعدی شما
- اگر پژوهشگر ریاضی یا مهندس نرمافزار هستید، کتابخانه PrimeGapsLib را در Lean 4 بررسی کنید تا با ساختار رسمیسازی پژوهشی آشنا شوید.
- ابزار مقایسهگر Lean را برای تأیید مستقل اثباتهای ارائه شده امتحان کنید.
- بررسی کنید که چگونه میتوان ویژگیهای کد برنامهنویسی شما را به گزارههای ریاضی برای تأیید رسمی تبدیل کرد.
اما تأثیر این رویکرد بر امنیت کدهای زیرساختی جهان حتی حیاتیتر است — به تحلیل ما دربارهی ایمنی مدلهای استدلالی مراجعه کنید.
گفتگو