شرکت آنتروپیک اعلام کرد که یکی از مدلهای داخلی این شرکت با استفاده از پلتفرم prove2.me موفق شده اثبات کامل آخرین قضیه فرما را در زبان لین رسمی کند. این دستاورد، آخرین قضیه باقیمانده در لیست ۱۰۰ چالش معروف فریب ویدایک را تکمیل کرد و به این چالش ۲۰ ساله پایان داد. اثبات ارائه شده توسط آنتروپیک مبتنی بر استدلال دارمون، دایاموند و تیلور از سال ۱۹۹۵ است و شامل بیش از ۱۳.۴ میلیون خط کد میشود. این پایگاه کد بسیار حجیم است و کامپایل آن روی یک ماشین با ۹۶ هسته، نزدیک به ۲۰ برابر کتابخانه ریاضی لین زمان میبرد. در حالی که جامعه ریاضی از درست بودن این قضیه مطمئن بود، این رسمیسازی گام بزرگی در استفاده از هوش مصنوعی برای مسائل پیچیده ریاضی محسوب میشود.