شرکت Axiom Math نسخه‌ای بررسی‌شده با ماشین از پروژهٔ استکس (Stacks Project)، یکی از مراجع مهم و متن‌باز هندسهٔ جبری، منتشر کرده است. در این صورت‌بندی، ریاضیات پروژه به حدود ۱۶ میلیون خط کد Lean تبدیل شده که برنامه‌ای برای بررسی برهان‌ها، آن را گام‌به‌گام ارزیابی می‌کند. آکسیوم می‌گوید پژوهشگران و عامل‌های هوش مصنوعی می‌توانند هنگام ساخت برهان‌های صوری تازه، از این نتایج به‌عنوان کتابخانه‌ای به‌هم‌پیوسته استفاده کنند.
تعداد صفحه‌های اعلام‌شده در منابع کمی متفاوت است: TechCrunch شمار آن‌ها را حدود ۷٬۶۵۴ صفحه گزارش می‌کند، در حالی که آکسیوم پروژه را حدود ۷٬۵۰۰ صفحه توصیف می‌کند. جان دی‌یونگ، ریاضی‌دان دانشگاه کلمبیا، این مرجع را در سال ۲۰۰۵ آغاز کرد و ریاضی‌دانان طی دو دهه آن را گسترش دادند. کار آکسیوم پژوهش‌های موجود را به شکل صوری درآورده است؛ این به معنای آن نیست که عامل‌های هوش مصنوعی ریاضیات زیربنایی را مستقلاً کشف کرده‌اند.
چرا کتابخانه‌ای به‌هم‌پیوسته اهمیت دارد؟
کتابخانهٔ برهان فقط به این دلیل مفید نیست که تک‌تک قضیه‌هایش بررسی شده‌اند؛ برهان‌های بعدی هم می‌توانند از آن‌ها و وابستگی‌هایشان استفاده کنند. آکسیوم می‌گوید برچسب‌های ثابت پروژهٔ استکس را حفظ کرده و اعلان‌های Lean را به بخش‌های متناظر در متن اصلی پیوند داده است. وب‌سایت شرکت نیز به خوانندگان امکان می‌دهد متن را کنار کد ببینند و بررسی کنند نتایج به یکدیگر چه وابستگی‌هایی دارند.
این موضوع به‌ویژه در هندسهٔ جبری اهمیت دارد؛ جایی که یک برهان ممکن است به زنجیره‌ای طولانی از ایده‌ها در حوزه‌هایی مانند جبر جابجایی، طرح‌ها، چف‌ها و همولوژی وابسته باشد. آکسیوم می‌گوید پیش از انتشار این کتابخانه، زیرساخت Lean برای صورت‌بندی صوری هندسهٔ جبری مدرن بسیار محدودتر بود. کتابخانهٔ این شرکت نقطهٔ شروعی در اختیار پژوهشگران می‌گذارد تا مجبور نباشند برای هر پروژه، آن مبانی را دوباره صورت‌بندی کنند.
پایه‌ای برای برهان‌ها و نرم‌افزارهای آینده
آکسیوم می‌گوید عامل‌هایش به‌صورت موازی کار کردند تا هزاران قضیه را ترجمه، اثبات و یکپارچه کنند. TechCrunch گزارش می‌دهد که شرکت چارچوبی کلی در اختیار عامل‌ها گذاشت تا خودشان کارهایی را برای انجام پیدا کنند و آکسیوم همچنین مدل‌های ویژهٔ ریاضیات خود را آموزش داد. این شرکت می‌گوید کتابخانهٔ نهایی بزرگ‌ترین کتابخانهٔ یکپارچه و قابل‌استفادهٔ مجدد از ریاضیات صورت‌بندی‌شده است؛ این توصیف آکسیوم از محصول خود است.
از همین نوع بررسی در حوزه‌هایی مانند طراحی تراشه و تأیید نرم‌افزار هم استفاده می‌شود. آکسیوم استدلال می‌کند که مبانیِ بررسی‌شده و قابل‌استفادهٔ مجدد می‌توانند به عامل‌های هوش مصنوعی کمک کنند هنگام نوشتن کدهای بیشتر، سامانه‌های قابل‌اعتمادتری بسازند. اما این انتشار فقط درستیِ صورت‌بندی صوری پروژهٔ استکس را بررسی می‌کند، نه هر ادعای ریاضی یا قطعه‌نرم‌افزاری را که یک سامانهٔ هوش مصنوعی ممکن است در آینده تولید کند.
چرا مهم است
این کتابخانه برای ریاضی‌دانان حوزهٔ هندسهٔ جبری، نتایج بررسی‌شده‌ای فراهم می‌کند که می‌توانند به‌جای بازسازی همان مبانی در Lean، دوباره از آن‌ها استفاده کنند. این کار صورت‌بندی صوری این مرجع را تأیید می‌کند، اما نشان نمی‌دهد که برهان‌ها یا کدهای آیندهٔ تولیدشده با هوش مصنوعی، بدون بررسی قابل‌اعتماد خواهند بود.
