Sou Theorem.chat
Theorem.chat pran yon avètisman matematik ak eseye pou rezoud li. Ou deklare avètisman an, ak estanda li dwe satisfè. Yon panel AI modèl — tankou anpil jan ou vle, soti nan nenpòt ki vandè ou vle — atak li, ak yon plis modèl referees. Lè sargumentation se fòmalize nan Lean 4 kont Mathlib, ak Lean kernel deside si li se pwouve. Ke etap dènye a se pwodwi a.
Poukisa yon kernel, e pa yon lòt modèl
Mande yon modèl yon kesyon difisil epi ou jwenn yon repons fluent si li se oswa pa se dwat. Mande plizyè ak yo souvan dakò, ki santi tankou corroboration e se pa: modèl pataje antrenè done ak pataje blind spots. Yon dezyèm modèl verifye premye se toujou menm kalite a jistis, e li ka pale alantou. Lean kernel pa ka. Li oubyen derive deklarasyon an soti nan axioms ak Mathlib, oswa li pa fè, ak konfidans pa gen okenn efè sou rezilta a.
Yon prèv ki kite yon twou ak sorry, yon lòt ki apelye a native_decide pou fè kernel la pran yon konpilasyon sou konfidans, oswa yon lòt ki an sekirite prezante yon nouvo axiome, se detekte ak refize pi plis pase konte kòm yon siksè.
Ki sa panèl la kapab fè
Argumentation se pati a bon mache. Panel la travay ak literati a - arXiv, OpenAlex, Crossref - se konsa yon rezilta konnen se citée pi pito pase re-derived mal. Li gen SageMath ak PARI/GP pou komputasyon, Z3 ak CVC5 pou SMT rezoud, OEIS lookup pou idantifye yon sekwen li te konstwi, ak yon anviwònman sandboxed Python san aksè rezo. Yon konjeksyon ka teste kont dè milye de ka anvan nenpòt moun pase yon toune ap eseye pwouve li, ak yon kont-egzanp fini diskisyon an imedyatman.
Evidans, pa elokite
Yon match pa klase sou bon jan kalite argumentasyon. Aplikasyon an dekonpoze nan kritè asepteman, epi yon kritè sèlman rezoud lè yon bagay dèyè li ka re-kontrollé pa yon twazyèm pati: yon sous ak pasaj ki gen rapò citée, oswa kòd ki te aktyèlman te egzekite ak rezilta reyèl li. Arbitre re-kontrollè sa evidans li menm anvan l ap detèmine, epi li pa ka deklare match la fini pandan yon kritè se toujou louvri.
Ou mete bar la
Standar la se ou a chwazi, ak arbitre a kenbe li literalman. Mande pou sa ki yon ekspè atansyon ta aksepte ak ou jwenn sa. Mande pou yon argumentation deductive konplè ak chak supposition te di ak ou jwenn jije kont san plas. Mande pou bar a yon pri soumèt ta fè fas a, ak rezilta a onè se pafwa yon kont presizyon nan kote panel la te tonbe kout - ki vale plis pase yon reklamasyon konfidans ou ta dwe tcheke tèt ou an menm fason an.
Pou nou pale klèman sou sa: sa pa yon machin ki rezoud pwoblèm ki louvri. Li se yon machin ki refize kite yon argument pase kòm rezoud lè li pa, e sa di w egzakteman ki etap ki pa t 'fèmen.
Yon fòmalize ki pa travay se rezilta a ki itil
Lè Lean pa pral fèmen prèv la, ou jwenn objektif egzak la ki rete. Nan pratik sa a se prèske toujou kote a kote argument informal te hand-waving — etap la tout moun ki li vèsyon an pwoz ta gen nodded pase. Sa a objektif se Lè sa a, te pote soti nan nenpòt ki sitiye se pi byen plase pou l atak li, ansanm ak sa ki te deja eseye, ak anyen lòt. Modèles thrash lè yo rete fidèl, re-enfòme yo nan pri a plen; pase yon kesyon espesifik an plas anjeneral deblotché pou yon fraksyon nan tokens.
Long travay survives
Tout lemma ke panel la etabli ale nan yon liv pataje ak prèv li, se konsa rezilta yo ekri yon fwa epi pa janm re-derived, ak bout yo mouri yo te anrejistre konsa pa gen okenn moun ki ale tounen nan yo. Matche kouri bò serveurs ak pause pwòp - sou bidjè, sou yon fournisseur interruption, oswa paske ou te fèmen tab la - ak retounen egzakteman kote yo te rete.
Ki sa sa pa pou
Sit sa a fèt pou matematik, lojisyèl, informatique teorik, fizik teorik ak teori ekonomik – se sa ki, se yon domèn kote yon pwopozisyon ka fèt pa yon prèv. Kesyon empirik nan bioloji, medikaman, chimi oswa syans sosyal pa pwodwi teorem, yo pwodwi rezilta, epi pa gen okenn kantite fòmalize pral deside yo. Sit nou an sè referee.chat kouri menm pwosesis panel-ak-referee san etap Lean, pou egzakteman sa yo kesyon.