אױף Theorem.chat
Theorem.chat נעמט אַ מאטעמאטיק־טענה און װעט זיך באַװוּנדערן צו דערװײַזן עס. דו װײַזסט אױף די טענה, און די סטאַנדאַרד װאָס זי מוז טרעפן. אַ װײַז פֿון AI־מאָדלן — וויפֿל דו װילסט, פֿון וועלכער װעלט דו װילסט — װעט אױפֿשטײַגן, און אַ מער מאָדעל װעט אױפֿשטײן. דערנאָך ווערט דער אױספֿיר פֿאָרמאַליזירט אין Lean 4 קעגן Mathlib, און דער Lean־קערן באַשטימט צי עס איז באַװוּנדערט. דער װײַטער שריט איז דער פּראָדוצירט
װאָס פֿאַר אַ קערן, און ניט אַ אַנדער מודל
Ask a model a hard question and you get a fluent answer whether or not it is right. Ask several and they often agree, which feels like corroboration and is not: models share training data and share blind spots. A second model checking the first is still the same kind of judgement, and it can be talked round. The Lean kernel cannot. It either derives the statement from the axioms and Mathlib, or it does not, and confidence has no effect on the outcome.
די געוויינטלעכע אופֿן צו פֿײַל אַ פֿאָרמאַלן באַװעגונג איז געװײנטלעכט און ניט געװען אַרײַנגעלאָזט. אַ באַװעגונג װאָס לאָזט אַ הױז מיט sorry, אױף װאָס מען װעט native_decide צו מאַכן דעם קערן צו נעמען אַ באַהאַנדלונג אױף דערװײַלונג, אױב ניט אַװעקצושטעלן אַ נײַע אקטיװיטעט, איז ניט געװײנטלעכט און ניט געװײנטלעכט, אױסגעלוקט װי אַ הצלחה
װאָס דער פּעניל קען טאַקע טאָן
Arguing is the cheap part. The panel works with the literature — arXiv, OpenAlex, Crossref — so a known result is cited rather than re-derived badly. It has SageMath and PARI/GP for computation, Z3 and CVC5 for SMT solving, OEIS lookup for identifying a sequence it has constructed, and a sandboxed Python environment with no network access. A conjecture can be tested against ten thousand cases before anyone spends a round trying to prove it, and a counterexample ends the discussion immediately.
װײַזונג, ניט װײַזונג
א שײך איז ניט געװײנטלעך אױף דער טענה־קוואַליטעט. דער קײן איז צעטיילט אין צונעמען קריטעריײן, און אַ קריטעריײן איז נאָר אױסגעפֿירט װען עפּעס הינטער אים קען אױסגעפֿירט ווערן אױף נײַע אופֿן דורך אַ דריטן פּאַרטיי: אַ מקור מיטן רעלאַטיוון ציטירטן װעג, אָדער קאָד װאָס איז טאַקע אױסגעפֿירט װי דער אמתער אױסגאַבע. דער ריכטער װײַזט זיך אױס מיט דעם אױסגאַבע אױף נײַע אופֿן אױף זיך אױף איידער ער װײַזט אױס, און ער קען ניט דערקלערן אױס, אַז דער שײך איז ענדיקט װען אַ קריטעריײן איז נאָך אױפֿגעפֿירט
איר האָט אויסגעקליבן דעם װײַז
דער סטאַנדאַרד איז אייער צו אויסקלײַבן, און דער ריכטער האַלט עס בײַם וואָרט. פֿרעגט פֿאַר וואָס אַ זאָרגנדיקער עקספּערט וואָלט אָננעמען און איר באַקומען דאָס. פֿרעגט פֿאַר אַ גאַנץ דעדוקטיווע אַרגומענט מיט יעדער אַנטפּלעקונג געזאָגט און איר באַקומען געריכט קעגן אַז אין אָרט. פֿרעגט פֿאַר די ברעג אַ פּריז אָנצופֿירן וואָלט טרעפן, און די אמתע רעזולטאַט איז יוזשאַוואַלי אַ פּינטלעך באַריכט פון וווּ די פּאַנעל איז אַרײַנגעפֿאַלן קורץ — וואָס איז מער ווערט ווי אַ זיכערע טענה איר וואָלט האָבן צו קאָנטראָלירן זיך אַליין ווידער
צו זײַן קלאָר: דאָס איז ניט אַ מײַזל װאָס װעט װײַזן אױפֿגעהײבטע פּראָבלעמען. דאָס איז אַ מײַזל װאָס װעט ניט װײַזן אײן אַרגומענט װי װײַזן װען עס איז ניט װײַזן, און װאָס װעט װײַזן װאָסער שריט איז דורכגעפֿאַלן
אַ דורכפֿאַלענע פֿאָרמאַליזאַציע איז דער ניצלעך אַרײַנשרײַב
װען װײַל װײַל ניט װעט אַרײַנשרײַבן דעם װײַז, װעט מען באַקומען דעם װײַזן ציל װאָס איז װײַזן. אין דער פּרווון איז דאָס כּמעט שטענדיק דער אָרט װוּ דער אינפֿאָרמעלע אױפֿגײד האָט זיך געװײַנט — דער שריט װאָס אַלעמען װאָס לײענט די פּראָזע־װירוס וואָלט געניכט. דער ציל ווערט דעמאָלט איבערגעגעבן צו דער אָרט װאָס איז בײַטסטע צו אױפֿשטײַגן, צוזאַמען מיט װאָס איז שוין געװען געפּרוּװט, און ניט װידער. מאָדעלן װײַזן זיך אױס װען זיי זײַנען פֿאַרבײַ, װײַזן זיך אױף אײן פֿולער צאָל; װען מען װײַזט אַ ספּעציפֿישע פֿראַגע װײַזט זיך אױס פֿאַר אַ ברײט פֿון די װײַזונגען
װײַטער־אַרײַנשרײַב
װידערצוצושטעלן
װאָס דאָס איז ניט פֿאַר
טעאָרעמ איז א װערד װאָס װעט אױסשרײַבן. די וועבזײַט איז פֿאַר מאַמעטאַטיק, לאַדזשיק, טעאָרעטישע קאָמפּיוטער־וויסנשאפט, טעאָרעטישע פיזיק און עקאָנאָמישע טעאָריע — פעלד װוּ א קײן איז אױסגעפֿירט דורך אַ באַװײַזונג. אײן־פֿאַר־אײן פֿראַגעס אין ביאָלאָגיע, מעדיצין, כימיע אדער געזעלשאפטלעכע װײַסענישן װעלן ניט װײַזן טעאָרעמס, זיי װעלן װײַזן געפֿינט, און קײן פֿאָרמאַליזאַציע װעט זיי ניט באַשליסן. אונדזער שוועסטער־װײַסװײַז referee.chat װעט װײַזן די זעלבע װײַזונג־איבער־איבער־פּראָצעס אָן דעם װײַסן שריט, פֿאַר די זעלבע פֿראַגעס.