به نقل از نیچر، قضیه آخر فرما، یکی از مشهورترین نتایج ریاضی نیمقرن اخیر، برای نخستین بار با استفاده از نسخهای پیشرفته و آزمایشی از چتبات هوش مصنوعی کلود به کدی تبدیل شده که توسط رایانه قابل راستیآزمایی است.
الکس کونتوروویچ، نظریهپرداز اعداد در دانشگاه راتگرز در نیوجرسی، میگوید اینکه یک ماشین توانسته کار ریاضیدانان انسانی را به یک اثبات ۱۳ میلیون خطی و کاملا قابل اعتماد تبدیل کند، واقعا مغزم را منفجر کرد.
شرکت آنتروپیک، سازنده کلود، که در سانفرانسیسکو مستقر است، این دستاورد را در روز چهارم سپتامبر اعلام کرد. این مدل پروژهای را که پیشبینی میشد تکمیل آن برای انسانها ۱۰ سال زمان ببرد، در تنها ۱۱ روز به پایان رساند.
این نتیجه نشان میدهد که هوش مصنوعی احتمالا نقش مهمتری در بررسی و راستیآزمایی کار ریاضیدانان و همچنین تولید استدلالهای جدید ریاضی ایفا خواهد کرد.
با سرعت فعلی پیشرفت، دیگر چندان دور از ذهن نیست که هوش مصنوعی به زودی بتواند تمام کتابخانه دانش ریاضی را بررسی کند و حتی شاید مشخص شود که برخی از نتایج شناخته شده ریاضی اشتباه هستند.
کوین بازارد، ریاضیدان امپریال کالج لندن، میگوید: دو سال پیش، چنین چیزی یک خیال بود.
ریاضیدانان شگفتزده شدهاند
ریاضیدانان به طور فزایندهای از سرعت پیشرفت تواناییهای هوش مصنوعی در ریاضیات شگفتزده شدهاند. یکی از این تواناییها، مشخص کردن اثباتها است؛ یعنی تبدیل استدلالهای ریاضی که به زبان طبیعی نوشته شدهاند به کدی رسمی که رایانه بتواند صحت آن را تایید کند. این کار معمولا با استفاده از زبان برنامهنویسی Lean انجام میشود.
در ماه فوریه نیز هوش مصنوعی در زمینه رسمیسازی به دستاورد مهم دیگری رسید؛ زمانی که توانست کار مارینا ویازوفسکا، برنده مدال فیلدز، درباره کارآمدترین روشهای چیدن کرهها در فضاهای هشتبعدی یا ۲۴بعدی را به صورت رسمی تایید کند.
اما بازارد میگوید پروژه مربوط به قضیه آخر فرما از نظر پیچیدگی در سطح کاملا متفاوتی قرار دارد. او میگوید: این کار شاید یک مرتبه دشوارتر بود. …
