‏🤖 فرمالیزه شدن پروژه Stacks در زبان Lean

‏شرکت Axiom موفق شد پروژه Stacks، دایره‌المعارف ۷۵۰۰ صفحه‌ای هندسه جبری، را به ۱۶ میلیون خط کد قابل‌بررسی توسط ماشین در زبان Lean تبدیل کند. این پروژه که بزرگترین کتابخانه یکپارچه و قابل‌استفاده مجدد Lean محسوب می‌شود، تمام تعاریف، لم‌ها و قضایای این حوزه را با تگ‌های چهار کاراکتری منحصربه‌فرد فرمالیزه کرده است.

‏ویژگی‌های فنی این دستاورد عبارتند از:
‏* شامل ۶۲,۹۷۵ فایل مجزا و ۶۶۳,۰۹۰ اظهارنامه منطقی.
‏* امکان ردیابی وابستگی‌های بین قضایا و استفاده از نتایج اثبات‌شده برای تحقیقات جدید.
‏* نمایش تعاملی به صورت یک نقشه سه‌بعدی از گراف‌های وابستگی ریاضی.

‏این تیم همچنین هفته گذشته قضیه طبقه‌بندی گروه‌های ساده متناهی (CFSG) را با استفاده از ده‌ها عامل هوش مصنوعی طی ۲۴ روز به ۴۳.۱ میلیون خط کد Lean تبدیل کرد. هسته Lean با بررسی این اثبات‌ها، صحت منطقی آن‌ها را تضمین می‌کند.

🇮🇷 - هوش مصنوعی و علم داده به فارسی
تلگرام | بله | ایتا | ارتباط با ما

#Stacks_Project #Lean_Prover