پژوهشگران EasyProver را معرفی کرده‌اند؛ سامانه‌ای که با کمک عامل‌های هوش مصنوعی، گزاره‌ها را در Lean اثبات یا رد می‌کند. Lean زبانی برای نوشتن اثبات‌هایی است که ماشین می‌تواند آن‌ها را بررسی کند. پژوهشگران همچنین Aegis را معرفی کرده‌اند؛ بنچمارکی که مسائل برنامه‌نویسی رقابتی را به وظایف راستی‌آزماییِ مرتبط با پیاده‌سازی‌های Rust تبدیل می‌کند.
در ارزیابی پژوهشگران، EasyProver توانست ۱٬۰۵۴ مورد از ۲٬۰۰۰ گزارهٔ نمونه در Aegis را در مهلت ۳۰ دقیقه‌ای برای هر گزاره اثبات کند. مقاله همچنین از امتیازهای بالای این سامانه در بنچمارک‌های جاافتادهٔ اثبات قضیه خبر می‌دهد؛ پژوهشگران می‌گویند این بنچمارک‌ها به سقف امتیاز نزدیک شده‌اند.
چرا مهم است
برای تیم‌های نرم‌افزاری که بررسی‌های رسمی کد Rust را مدنظر دارند، Aegis وظایفی را در بر می‌گیرد که جزئیاتی مانند تبدیل نوع اعداد صحیح و رفتار هنگام شکست را شامل می‌شوند؛ اما هنوز مشخص نیست EasyProver بتواند کد خود این تیم‌ها را به‌سرعت راستی‌آزمایی کند.
