Math

מה זה

מזינים טענה מתמטית מנוסחת היטב בתיבת הטקסט, ואפשר להוסיף גם רקע או הסבר חופשי בשדה נפרד. בוחרים את אורך הפלט המרבי באמצעות סליידר שנע בין 150 ל־4096 טוקנים, ולוחצים על שליחה.

בתגובה מקבלים צ'אט עם ההוכחה, לצד אקורדיון שמכיל את הפלט המלא במבנה JSON ואת קוד ה־Lean4 שנשלף מתוך התשובה. המערכת נשענת על מודלים ממשפחת Kimina Prover, כולל גרסת 8B מזוקקת וגרסת 72B, שפותחו להסקה והוכחת משפטים פורמליים, ומסתמכת גם על הדאטהסט unimath.

מתאים ל

• ניסוח הוכחות ב־Lean4

  תרגום טענות ומשפטים מתמטיים ישירות לשלדי הוכחה פורמליים בקוד Lean4.

• פתרון בעיות מתמטיות

  הפקת שרשרת הסקה לוגית ופורמלית עבור בעיות מתוך דאטהסטים כמו unimath.

• השוואת פלטי מודלים

  בחינת יכולות ההסקה של משפחת מודלי Kimina Prover על ניסוחים שונים.

איפה זה נופל

מודל השפה מייצר קוד והוכחות, אבל הוא אינו מריץ מהדר Lean4 בתוך הדפדפן כדי לוודא מתמטית שההוכחה נכונה. תצטרכו להעתיק את הקוד ולבדוק אותו בעצמכם כדי לוודא שאין בו שגיאות תחביר או לוגיקה. בנוסף, חומרת ה־A10G עשויה להגביל את המהירות בהפקת פלטים ארוכים.

איך משתמשים

מקלידים את המשפט בתיבת הקלט, מכוונים את כמות הטוקנים הרצויה ולוחצים על Send. הממשק מבוסס על סביבת Zero A10G של Hugging Face Spaces, מה שאומר שהמעבד הגרפי מוקצה לפי דרישה. ייתכן שתמתינו כמה שניות להקצאת החומרה לפני שהחישוב יתחיל בפועל, אך אין צורך בהרשמה מיוחדת כדי לבצע בדיקה.

הרישיון

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

• שימוש מסחרי
• שינוי הקוד
• הפצה מחדש

הרישיון המלא ב־Hugging Face ↗