Theorem.chat golaý
Theorem.chat bir matematikal talap alar we ony çözmek üçin synanyşar. Siz talapy we standarty bellemelisiňiz. AI modelleriň bir paneli - isleýäniňizçe köp, isleýäniňizçe satyjylardan - oňa hüjüm eder, we bir modelden başga bir model münberçi. Soňra argüment Lean 4 bilen Mathlib arasynda resmileşýär, we Lean kernel onuň subut edilişini karar eder. Bu soňky ädim önümdir.
Näme üçin kernel, başga model däl
Modele çylşyrymly sorag soraň we siz dogry ýa-da ýalňyşdygy barada dogry ýa-da dogry däl jogap alarsyňyz. Birnäçe sorag soraň we olar köplenç ylalaşarlar, bu bir ýardam ýaly duýulýar we däl: modeller tälim maglumatlary paýlaşýar we görmeýän ýerleri paýlaşýar. Ikinji model birini barlap, şol bir pikire eýedir, we bu gürleşip bolar. Lean kernel başarmaz. Ol ýa aksiomlardan we Mathlib-den sözi alyp gelýär, ýa-da etmez, we ynam netijä täsir etmeýär.
Bir resmi subutnamany ýalanlamak üçin ulanylýan usullar barlanýar we ret edilýär. sorry bilen bir gap gaçan subutnama, native_decide'e seslenýän bir subutnama kerneli bir hasapny berjaý etmek üçin ynamly etmek üçin, ýa-da sessiz bir täze aksiomy getiren bir subutnama, tapylyp we kabul edilmekden beter ret edilýär.
Paneliň hakykatda ne edýändigi
Argumentation is the cheapest part. Panel works with literature - arXiv, OpenAlex, Crossref - so a known result is quoted rather than badly re-derived. It has SageMath and PARI/GP for computing, Z3 and CVC5 for SMT solving, OEIS search 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 immediately ends the discussion.
Eşidýän, sözleňok
A match argumentiň hilinden baha berilmändir. Bu arz kabul etmek şertine bölünýär we bir şert diňe arkasynda bir zat üçünji bir tarap tarapyndan tekrar barlansa çözlenir: bir çeşme degişli sözler bilen sözlenilipdir, ýa-da kod hakykatda öz hakykatda çykan bilen işledilipdir. Reýder karar bermekden öň bu delilleri tekrar barlaýar we bir şert aç bolsa match'i tamamlanan diýip yglan edip bilmez.
Sen bary goýýarsyň
Standart siziň saýlamak üçindir we hakim ony sözme-söz saklaýar. Bir ünsli ekspert kabul etjek zady soraň we siz ony alarsyňyz. Her bir çaklamalar bilen dolu bir deduktiw argument soraň we siz onuň ýerine garşysyna höküm edilýärsiňiz. Bir baýragyň hödürleniljek bary soraň we dogry netije arada paneliň näçe az düşenini anyk bir beýany bolup dur - bu bir ynamly iddiadan has gymmatly, siz öz-özüňizi barlamak gerek bolarsyňyz.
Bu barada aýanlyk üçin: bu açyk meseleleri çözýän maşyn däl. Bu bir argumenti çözlen ýaly geçmekden ýüz öwürýän maşyn, eger ol çözülmän bolsa, we size nädip hata edeniňizi aýdyp berýär.
Bir formalizasiýa faýlsyzlyk bilen tamamlandy we peýdaly çykdajy
Lean subutnamany baglamaýan bolsa, siz galan dogry maksaty alarsyňyz. Praktikada bu her wagt resmi däl argumentiň el-waşlap duran ýeridir - her kim proza wersiýasyny okaýan bolsa, bu ädimden geçjekdir. Bu maksat soňra, oňa hüjüm etmek üçin iň gowy ýere, öňden synlan zat bilen, we başga hiç zat bilen, geçýär. Modeller, olar çakylan wagty, özlerini doly baha bilen tekrarlap, çakylan wagty, özlerini doly baha bilen tekrarlap, bir belli soragy geçmek, adatça, tokenleriň bir bölek üçin blokadyň açylmagyny üpjün edýär.
Uzak iş gaýd eder
Paneliň berjaý eden her bir lemmasy öz subutnamasy bilen paýlaşylan bir kitapça girer, şoňa görä netijeler bir gezek ýazylyp hiç wagt tekrarlanmaz, we ölü endiler ýazylýar, şoňa görä hiç kim olara dolanyp gelmez. Matches serwer tarapy işleýär we arassa durdur - býujetde, bir berijiniň öçüşi ýa-da siziň täbi ýapmak üçin - we dogry durdurylan ýerinden dowam eder.
Bu näme üçin däl
Teorem bir deduktiw söz. Bu saýt matematika, manyk, teorik kompýuter ylym, teorik fizika we ekonomik teoriýa üçin gurlan - bir iddianyň subutnama bilen çözülen meýdançalar. Biologiýa, derman, himiya ýa sosial ylymlarda empirik soraglar teoremleri döretmez, olar tapylanlary döretýär we hiç bir formalizasiýa olary çözmez. Biziň dogan saýtymyz referee.chat şol soraglar üçin Lean adımsyz şol panel-and-referee prosesi işledýär.