محققان در یک دستاورد هیجانانگیز، از یک سیستم هوش مصنوعی برای رسمیسازی (Formalization) اثباتهای ریاضی در محیط «Lean 4» استفاده کردهاند. در این پروژه، هوش مصنوعی با هدایت یک ریاضیدان، توانسته اثباتهای پیچیده مربوط به «معادله ولاسوف» (Vlasov equation) را بدون هیچ خطایی به زبان ماشین ترجمه و تأیید کند.
نکته جذاب اینجاست که نقش انسان در اینجا فقط «هدایت» بوده و هوش مصنوعی بار سنگین اجرای اثباتها را به دوش کشیده است. این پیشرفت نشان میدهد که ترکیب قدرت استدلال انسان و توان اجرایی هوش مصنوعی، چه پتانسیل عظیمی برای پیشبرد علم ریاضیات و اطمینان از درستی قضایا دارد! 🧠✨
منبع: arXiv AI