کل Stacks Project به Lean ترجمه شد
هوش مصنوعیClaude Opus 5.5خلاصهٔ کامل‌تر
شرکت Axiom اعلام کرده کل Stacks Project رو به Lean برگردونده. Lean یه زبان برنامه‌نویسی‌ه که توش اثبات ریاضی رو می‌نویسی و کامپیوتر چک می‌کنه درسته یا نه. Stacks Project یه مرجع متن‌باز حدوداً ۷۵۰۰ صفحه‌ای‌ه که پایه‌های هندسهٔ جبری مدرن رو جمع کرده. خروجی حدود ۱۶ میلیون خط کد هست و طبق ادعای Axiom بزرگ‌ترین کتابخونهٔ یکپارچه از ریاضیات رسمی‌شده تا امروزه.
این پروژه رو Johan de Jong از دانشگاه کلمبیا سال ۲۰۰۵ شروع کرد و صدها ریاضی‌دان توی این دو دهه با اثبات و مثال بهش اضافه کردن. نویسنده می‌گه de Jong اونو مثل یه پروژهٔ نرم‌افزاری مثل Linux kernel مدیریت کرده: هر قضیه یه tag چهارحرفی ثابت داره و هر قدم دقیقاً به tagهایی که بهشون وابسته‌ست اشاره می‌کنه. یعنی ساختارش از قبل شبیه یه کتابخونهٔ اثبات رسمی بوده. نسخهٔ Lean هم همین tagها رو نگه داشته و هر declaration به متن اصلی لینک میشه.
چرا این کار مهمه؟ به گفتهٔ Axiom، وقتی AI داره با سرعتی بیشتر از توان بررسی آدم‌ها استدلال ریاضی تولید می‌کنه، چک کردن خودکار ضروری میشه. توی هندسهٔ جبری یه اثبات امروزی ممکنه قبل از شروع اصل حرفش به زنجیرهٔ بلندی از قضیه‌ها توی جبر جابه‌جایی، schemeها، sheafها و cohomology تکیه کنه. تا حالا این زیرساخت توی Lean و کتابخونهٔ Mathlib وجود نداشت. حالا هر کسی که بخواد قضیهٔ جدیدی رو رسمی کنه، می‌تونه این تعریف‌ها رو مستقیم import کنه.
نویسنده می‌گه این کار بیشتر از اون‌که ریاضی باشه، مهندسی سیستم بوده. اگه هزاران ایجنت AI بدون هماهنگی کار کنن، دو تا ایجنت ممکنه برای یه مفهوم دو تعریف ناسازگار بسازن. Lean هر دو فایل رو جدا قبول می‌کنه، ولی بعداً نمی‌شه کنار هم ازشون استفاده کرد. برای همین Axiom یه سیستم سلسله‌مراتبی از ایجنت‌ها با نقش‌های مشخص ساخته. یه بخش مهمش هم ممیزی چندایجنتی و مقایسه با متن اصلی بوده، تا مطمئن بشن هر جملهٔ رسمی دقیقاً همون معنای متن اصلی رو داره.
توی این مسیر، سیستم چند ده جمله توی Stacks Project پیدا کرده که اصلاح لازم داشتن: فرض‌های جاافتاده، حالت‌های مرزی توی positive characteristic، و ادعاهایی که به اون کلیت درست نبودن. ایجنت‌ها برای این‌ها مثال نقض ساختن، فرض درست رو اضافه کردن یا راه دیگه‌ای برای اثبات قضیهٔ اصلی پیدا کردن. de Jong اخیراً خواسته فعلاً pull request یا کامنت تولیدشده با AI به مخزن اصلی فرستاده نشه، و Axiom می‌گه همهٔ اصلاحات رو توی مخزن خودش نگه می‌داره.
نکات کلیدی:
- کل Stacks Project، حدود ۷۵۰۰ صفحه، به حدود ۱۶ میلیون خط کد Lean تبدیل شده
- tagهای ثابت Stacks حفظ شدن و متن و کد Lean کنار هم توی stacks.axiommath.ai قابل دیدنه
- کار با یه سیستم سلسله‌مراتبی از ایجنت‌های AI و ممیزی خودکار وفاداری به متن انجام شده
- چند ده جمله با فرض جاافتاده یا ادعای بیش از حد کلی پیدا و با مثال نقض اصلاح شدن
- این پروژه بعد از رسمی‌سازی Classification of Finite Simple Groups در ۲۷ اکتبر ۲۰۲۶ اومده
- نسخهٔ Lean پروژه‌ای مستقل و متن‌بازه و به مخزن اصلی Stacks چیزی نمی‌فرسته
