מתמטיקה, המבוססת באופן מסורתי על בניית הוכחות שורה אחר שורה, עוברת מהפך הודות לבינה מלאכותית. כלים חדשים, המכונים AI "טייסי משנה", מתחילים לעזור באופן פעיל למדענים לפתח ראיות, ולפתוח סיכויים לפתרון בעיות שבעבר נראו מחוץ להישג יד.
מבוסס במכון הטכנולוגי של קליפורניה נמצא בפיתוח אחד מ"טייסי המשנה" הללו. כלי זה מציע באופן אוטומטי את השלבים הבאים בהוכחות, ועוזר לך להשלים משימות ביניים ולבנות קשרים לוגיים בין אלמנטים גדולים יותר. תכונה חשובה היא שכל האפשרויות המוצעות נבדקות ושגיאות מתבטלות הודות לשימוש במערכת רָזֶה המיישמת לוגיקה מתמטית קפדנית.
Lean, שהולכת וגוברת בפופולריות בקרב מתמטיקאים, מאפשרת לעצב הוכחות מתמטיות באמצעות קידוד. גישה זו מבטלת שגיאות שעלולות להתרחש עם סקירה ידנית וממכנת אימות של נכונות ההצהרות. עם זאת, הצורך לפרט אפילו הצהרות ברורות יכול להיות עתיר עבודה, מה שעצר עד כה את האימוץ ההמוני של כלים כאלה.
הפיתוח של "טייסי המשנה" של AI מתקדם גם בפרויקטים אחרים כמו AlphaProof ו- AlphaGeometry 2, שכבר מציגים תוצאות מרשימות, למשל באולימפיאדת המתמטיקה הבינלאומית. עם זאת, לפתרון בעיות במורכבות הגבוהה ביותר הדורשים ניתוח מעמיק, המערכות עדיין נחותות מאנשים. עם זאת, מומחים מצפים שבשנים הקרובות טכנולוגיות אלו יגיעו לרמה הדרושה לפתרון בעיות מסוג זה.
השילוב של "טייסי משנה" של AI מבטיח לשנות לא רק את תהליך ההוכחה, אלא גם את הדרך שבה מתמטיקאים מקיימים אינטראקציה. במקום העבודה המסורתית של קבוצות קטנות של עמיתים, השימוש ב-AI יכול לאפשר לצוותים גדולים לפרק בעיות מורכבות לחלקים ולפתור אותן יחד באמצעות שותפויות בין אדם למכונה. זה עשוי להאיץ את ההתקדמות בפתרון בעיות מתמטיות גלובליות, כולל בעיות מפורסמות בפרס המילניום כמו P vs NP.
שינויים אלו הושוו למהפכה שנגרמה בעקבות הופעת המחשבונים האלקטרוניים, אשר פשטה מאוד חישובים מורכבים. בעתיד, בינה מלאכותית תוכל לאפשר למדענים להתמקד בהיבטים הקשים ביותר של המתמטיקה, להפוך את החלק השגרתי של העבודה לאוטומציה ולעודד שיתוף פעולה עמוק יותר בקהילה המדעית.
