אופן-איי שחררה כמעט 400 תוצאות מתמטיות ב־700 כתבי יד, וחוקרים יזדקקו לשנים כדי לעכל את זה

מה שמאחורי המספרים

השחרור הפתאומי מכסה קומבינטוריקה, גאומטריה על ענפיה, תורת המספרים, מדעי המחשב התיאורטיים, אלגברה, טופולוגיה, הסתברות ומכניקה סטטיסטית, ופיזיקה מתמטית. היקף החומר גדול עד כדי כך שהחברה פרסמה מדריך ניווט למאגר גיטהאב, ותוכן העניינים בלבד משתרע על כ־40 עמודים. פרופסור אלווארו לוזאנו-רובלדו (Álvaro Lozano-Robledo) מאוניברסיטת קונטיקט אמר לוורג שרק מעבר על רשימת התקצירים "מציף", חוקרים דיווחו שהקריאה הראשונית לקחה להם כשעה.

הבעיה עם האימות

חלק מהתוצאות מלוות בפורמליזציה ב־Lean, שפת תכנות ועוזר הוכחה (proof assistant) שמאפשר אימות חישובי, אבל רק 300 מתוך 719 כתבי יד עברו פורמליזציה, כ־42 אחוז. באיי-איי הודו שהחומרים נמצאים "בשלבי אימות שונים" והבטיחו לעדכן את המאגר בהמשך. מתמטיקאים שהתחילו לחפור מצאו שגם כשיש קוד Lean, האיכות לא אחידה, וההצהרות המאומתות לא תמיד תואמות את הטענות בכתבי היד הנלווים. בדיקת התאמה כזו היא כשלעצמה תהליך ממושך.

מה זה עושה לחוקרים

פרופסור קווין באזארד (Kevin Buzzard) מאימפריאל קולג' לונדון סרק את התחום שלו, תורת המספרים האלגברית, וזיהה רק כשש משפטים ש"בלטו מיד"; מעטים מהם, אם בכלל, נראו פורצי דרך. מעבר לאיכות הנקודתית, עולה חשש עמוק בקהילה: הקריירות של מתמטיקאים עלולות להשתנות בן לילה, והם יצטרכו להפריד בין פתרונות אמיתיים ל"רעש" בזמן שהחברה כבר ממשיכה הלאה. "אם הבינה המלאכותית הייתה נעלמת עכשיו, כמו חייזרים שנחתו ועזבו, היינו חוקרים את זה עשר שנים בניסיון להבין הכול," סיכם אחד החוקרים.

השורה התחתונה

השחרור חסר תקדים בהיקפו, אבל ערכו המדעי עדיין לא ברור, רוב החומר לא עבר אימות מלא, והקהילה תצטרך שנים כדי למפות מה כאן תורם אמיתי ומה סתם נפח. אופן-איי לא מחכה: היא כבר הבטיחה עוד פורמליזציות, וסביר שתשחרר עוד חומרים לפני שהחוקרים יסיימו לעכל את המנה הנוכחית.