Körülbelül Theorem.chat
Theorem.chat veszi a matematikai követelést, és megpróbálja rendezni. Ön megállapítja az igényt, és a szabványnak meg kell felelnie. A panel AI modellek · annyi, amennyit csak akar, attól, hogy az eladók azt akarja, hogy • megtámadja, és még egy modellbírák. Ezután az érv formalizálódik Lean 4 szemben Mathlib, és a Lean kernel dönti el, hogy ez bizonyított-e. Ez az utolsó lépés a termék.
Miért egy kernel, és nem egy másik modell
Kérdezd meg a modellt egy kemény kérdés, és kapsz egy folyékony választ, hogy helyes-e vagy sem. Kérdezz meg több és gyakran egyetértenek, amely úgy érzi, mint megerősítő és nem: modellek megosztani képzési adatok és megosztás vak foltok. Egy második modell ellenőrző az első még mindig ugyanaz a fajta ítélet, és lehet beszélni kerek. A Lean kernel nem. Ez vagy származik a nyilatkozat az axioms és Mathlib, vagy nem, és a bizalom nincs hatással az eredményre.
A hivatalos bizonyíték hamisításának szokásos módjait ellenőrzik és elutasítják. A sorry-es lyukat elhagyó bizonyítékot, amely native_decide-re szól, hogy a rendszermagot a bizalomra számítsa, vagy egy olyant, amely csendben bevezet egy új axiómát, inkább észlelik és elutasítják, mint sikernek számítsák.
Mit tehet a panel?
A vita az olcsó rész. A panel működik a szakirodalomban ~ arXiv, OpenAlex, Crossref ~ így ismert eredmény idézik inkább, mint újra rosszul. Ez a SageMath és PARI/GP a számítás, Z3 és CVC5 SMT megoldás, OEIS keresési azonosítás egy szekvenciát épített, és egy homokozós Python környezet nélkül hálózati hozzáférés. A találgatás lehet tesztelni tízezer esetben, mielőtt bárki költ egy kört, hogy megpróbálja bizonyítani, és egy ellenpélda véget ér a vita azonnal.
Bizonyíték, nem ékesszólás
A mérkőzés nem az érvelés minőségét mutatja. Az igény az elfogadási kritériumokra bontható, és a kritérium csak akkor kerül rendezésre, ha egy harmadik fél újra ellenőrizheti azt: egy forrás a vonatkozó szakasz idézett, vagy kód ténylegesen végrehajtott valós kimenet. A bíró újra ellenőrzi, hogy maga a bizonyíték előtt dönt, és nem tudja bejelenteni a mérkőzés befejeződött, amíg egy kritérium még nyitott.
Te állítottad be a bárt.
A szabvány a tiéd, hogy válassz, és a bíró tartja szó szerint. Kérje, hogy mit egy gondos szakértő elfogadná, és kapsz, hogy. Kérjen egy teljes deduktív érv minden feltételezése, és akkor elítélik, hogy helyette. Kérje a bár egy díjat benyújtani szembesülne, és a becsületes eredmény általában egy pontos beszámoló arról, hogy a panel esett rövid • amely többet ér, mint egy magabiztos követelés akkor is ellenőrizni magát.
Hogy világos legyen: ez nem egy olyan gép, amely megoldja a nyitott problémákat. Ez egy olyan gép, amely nem hajlandó hagyni, hogy egy vita elsimuljon, amikor nincs, és ez pontosan megmondja, melyik lépés nem sikerült.
A sikertelen formalizálás a hasznos kimenet
Amikor Lean nem zárja be a bizonyítékot, kapsz pontos célt, hogy továbbra is. A gyakorlatban, hogy szinte mindig a helyszínen, ahol az informális érvelés volt kézzel hullámzó • a lépés mindenki olvassa próza verzió lenne bólintott múlt. Ez a cél akkor átadjuk, hogy melyik hely a legjobb hely támadni, valamint amit már próbáltak, és semmi más. Modellek ütés, amikor beragadtak, újra a teljes költségen; halad egy konkrét kérdés helyett általában oldja meg a blokkok egy töredéke a zsetonokat.
A hosszú munka túléli
Minden lemma a panel megállapítja megy egy közös főkönyv a bizonyíték, így az eredmények egyszer vannak írva, és soha nem újra származó, és a zsákutcák rögzítjük, így senki sem sétál vissza őket. Gyufák fut szerver oldalán, és szünet tisztán költségvetés, a szolgáltató kimaradás, vagy mert zárt a fül • és folytassa pontosan ott, ahol megálltak.
Mi ez a nem
A Theorem egy deduktív szó. Ez a weboldal matematika, logika, elméleti számítástudomány, elméleti fizika és gazdasági elmélet számára készült • olyan területek, ahol a követelés bizonyítással rendeződik. A biológia, orvostudomány, kémia vagy társadalomtudományok kérdései nem adnak elméleteket, hanem eredményeket hoznak, és nem sok formalizálás dönti el őket. A nővérünk oldalunk referee.chat-ben ugyanazzal a panel-és-megkeresett eljárással fut a Lean lépés nélkül, pontosan ezekért a kérdésekért.