סוכני בינה מלאכותית פשוט בדקו במחשב את ההוכחה הארוכה ביותר בהיסטוריה של המתמטיקה הסיווג של קבוצות פשוטות סו…

סוכני בינה מלאכותית פשוט בדקו במחשב את ההוכחה הארוכה ביותר בהיסטוריה של המתמטיקה הסיווג של קבוצות פשוטות סופיות אורך כ-15,000 עמודים, שנכתבו על ידי כ-100 מתמטיקאים במשך עשרות שנים. תוך 24 ימים, צוות אקסיומות הצביע על נחילי סוכני AI והפך את כל ההוכחה ל-רזה, שפה שבה מחשב מאמת כל צעד הגיוני. התוצאה היא כ-43.1 מיליון שורות קוד. סוכנים תבעו משימות, העבירו חלקים חסרים לסוכנים אחרים ואיגדו את עבודתם במאגר אחד. הם גם מצאו בעיות אמיתיות בהוכחה שפורסמה. רובן היו שגיאות הקלדה ושגיאות טבלה, אבל אקסיומה אומרת שהיה צורך לתקן 34 סטיות. לשלב אחד בטיעון משנת 1986 היו דוגמאות נגד, אז הסוכנים בנו מסלול חדש על רעיונות משנת 1976 והוכיחו תוצאה חדשה של תיאוריה קבוצתית לאורך הדרך. תיאורטיקנים של קבוצות שעבדו על ההוכחה המקורית יעצו על החלקים הקשים ביותר.