Tentang Theorem.chat
Theorem.chat nyandak klaim matematikal sarta coba ngarengsekeunana. Anjeun nyatakeun klaim, sarta standar anu kedahna dipasihkeun. Panel model AI - sakumaha seueurna anu anjeun pikahoyong, ti vendor naon waé anu anjeun pikahoyong - ngalawan éta, sareng hiji model langkung ngajual. Saterusna argumen diformalisasi dina Lean 4 ngalawan Mathlib, sareng kernel Lean mutuskeun naha éta dibuktikeun. Langkah pangakhirna nyaéta produk.
Mengapa kernel, lan ora model liyane
Nyahokeun model hiji pertanyaan susah sarta anjeun meunang jawaban alus naha éta bener atawa henteu. Nyahokeun sababaraha sarta maranehna sok satuju, nu ngarasa kawas confirmation jeung teu: model babagi data latihan jeung babagi titik buta. Model kadua ngawatesan nu kahiji masih jenis nu sami tina judgment, sarta éta bisa dibahas. Lean kernel teu bisa. Éta boh ngahasilkeun pernyataan ti aksioma jeung Mathlib, atawa éta teu, sarta percaya teu boga efek dina hasil.
Cara anu biasa pikeun ngadugikeun bukti formal dicek sarta ditolak. Bukti anu ninggalkeun liang sareng sorry, anu ngajual ka native_decide pikeun ngajantenkeun kernel nyandak komputasi dina percaya, atanapi anu sacara diam-diam ngawanohkeun aksioma anyar, ditéwak sareng ditolak tibatan diitung salaku kasuksésan.
Apa sing panel bisa laksanakan
Argumen nyaéta bagian anu murah. Panel damel sareng literatur - arXiv, OpenAlex, Crossref - janten hasil anu dikenal dikutip tibatan diturunkeun deui. Éta ngagaduhan SageMath sareng PARI/GP pikeun komputasi, Z3 sareng CVC5 pikeun SMT solusi, OEIS lookup pikeun ngaidentipikasi urutan anu parantos diwangun, sareng lingkungan Python sandboxed tanpa aksés jaringan. A konjektur tiasa diuji ngalawan sapuluh rébu kasus sateuacan saha waé ngahabiskan waktos pikeun ngabuktikeun éta, sareng conto anu ngalawan ngaakhirkeun diskusi langsung.
Bukti, ora eloquence
Sahiji kasaimbangan henteu dinilai ku kualitas argumen. Klaim dipecah kana kriteria pangtarima, sarta kriteria ngan ditangtukeun lamun aya anu dibelakangna bisa dicek deui ku pihak katilu: sumber kalayan pasagi anu relevan dikutip, atawa kode anu leres-leres dilaksanakeun sareng hasilna anu leres. Pamaréntah ngawatesan buktina sorangan sateuacan ngahukum, sarta henteu tiasa nyatakeun kasaimbangan réngsé nalika kriteria masih dibuka.
Sampeyan ngetung bar
Standar ieu anjeun milih, sarta pangadilan ngawengku eta sacara harfiah. Tanya pikeun naon ahli anu ati-ati bakal nampi jeung anjeun meunang éta. Tanya pikeun argumen deductive lengkep kalawan unggal asumsi dinyatakeun sarta anjeun meunang dihukum ngalawan éta sabalikna. Tanya pikeun bar hiji hadiah submission bakal ngalawan, sarta hasil jujur biasana hiji akun akurat tina dimana panel fallen short - nu leuwih berharga ti hiji klaim percaya anjeun bakal kudu ngawatesan diri.
Pikeun ngajelaskeun: ieu lain mesin anu ngarengsekeun masalah anu dibuka. Ieu mesin anu henteu ngaluarkeun argumen salaku direngsekeun nalika éta henteu, sarta anu ngawartosan anjeun pasti naon léngkah anu gagal.
A formalisasi gagal iku output sing bisa digunakake
Nalika Lean teu bakal nutup bukti, anjeun bakal meunang tujuan anu leres anu tetep. Dina praktekna éta hampir salawasna tempat dimana argumen informal éta tangan-waving - léngkah unggal jalma maca versi prosa bakal geus nodding kaluar. Tujuan éta diteruskeun ka mana waé tempat anu pangalusna ditempatkeun pikeun ngalawan éta, bareng jeung naon anu geus dicoba, jeung teu aya anu sanés. Model thrash nalika aranjeunna cilaka, reiterating sorangan dina biaya lengkep; ngaliwatan hiji patarosan husus sabalikna biasana ngabuka pikeun fraksi tina token.
Long kerja survives
Satiap lemma anu diwangun panelna bakal diasupkeun kana lembar anu dibagikeun kalayan buktina, sahingga hasilna ditulis sakaligus sarta teu pernah diturunkeun deui, sarta jalan buntu dicatat supados teu aya anu balik deui ka aranjeunna. Pareuman dijalankeun dina sisi server sareng ditunda sacara bersih - dina anggaran, dina gangguan panyadia, atanapi kusabab anjeun nutup tab - sareng dilanjutkeun persis dimana aranjeunna dieureunkeun.
Apa sing ora kanggo
Teorema nyaéta kecap deduktif. Situs ieu diwangun pikeun matematika, logika, ilmu komputer teoretis, fisika teoretis sareng teori ekonomi - widang dimana klaim ditetepkeun ku bukti. Pertanyaan empiris dina biologi, médis, kimia atanapi ilmu sosial henteu ngahasilkeun teorema, aranjeunna ngahasilkeun hasil, sareng henteu aya jumlah formalisasi anu bakal mutuskeun aranjeunna. Situs saudara kami referee.chat ngajalankeun prosés panel- sareng-referee anu sami tanpa léngkah Lean, pikeun patarosan anu leres.