Ax-Prover چارچوبی چندعامله برای اثبات خودکار قضیه‌ها در Lean است

Ax-Prover برای اثبات خودکار قضیه‌ها در Lean طراحی شده و بنا بر چکیدهٔ مقاله، مسائل را در حوزه‌های علمی گوناگون، از جمله ریاضیات و فیزیک کوانتومی، هدف می‌گیرد. این سامانه از مدل‌های زبانی بزرگ برای دانش و استدلال بهره می‌برد و آن‌ها را از طریق Model Context Protocol (MCP) به ابزارهای Lean متصل می‌کند؛ ابزارهایی که درستی صوری برهان‌ها را بررسی می‌کنند. پژوهشگران می‌گویند Ax-Prover می‌تواند مستقل عمل کند یا با متخصصان انسانی همکاری داشته باشد. مقاله ارزیابی سامانه را در مقایسه با مدل‌های زبانی پیشرفته و مدل‌های تخصصی اثبات‌گر، بر پایهٔ دو معیار عمومی ریاضی، شرح می‌دهد؛ اما متن در دسترس جزئیات نتایج این مقایسه را ارائه نمی‌کند.