تا امروز، دنیای اثبات ریاضی با هوش مصنوعی (Formal Reasoning) در جبر و نظریه اعداد پیشرفتهای خیرهکنندهای داشته، اما «هندسه» همیشه به دلیل پیچیدگیهای تصویری، چالشبرانگیز بود. حالا با معرفی فریمورک جدیدی به نام Euclean، این سد شکسته شده است!
این پروژه با ارائه بزرگترین دیتاسیت رسمی هندسه در زبان برنامهنویسی Lean، توانسته به دقت فوقالعادهای در اثبات مسائل هندسی رقابتی برسد. Euclean به مدلهای هوش مصنوعی کمک میکند تا به جای روشهای سنتی، مستقیماً در بستر استاندارد Mathlib به استدلال منطقی بپردازند.
این یعنی یک گام بزرگ دیگر به سمت سیستمهای اثبات ریاضیِ متحد و هوشمند که دیگر برای شاخههای مختلف ریاضی، به ابزارهای جداگانه نیاز ندارند. 🧠✨
نویسی
منبع: arXiv AI