Am Theorem.chat
Mae Theorem.chat yn cymryd datganiad mathemategol a'i geisio ei ddatrys. Rydych chi'n nodi'r datganiad, a'r safon mae'n rhaid iddo ei gwrdd. Mae panel o fodel AI - cymaint ag y dymunwch, o unrhyw werthwyr rydych chi'n eu hoffi - yn ei ymosod, a model arall yn ei farnu. Wedyn mae'r honiad yn cael ei ffurfweddu yn Lean 4 yn erbyn Mathlib, a'r cnewyllyn Lean yn penderfynu a yw wedi'i brofi. Y cam olaf yw'r cynnyrch.
Pam cnewyllyn, a ddim model arall
Gofynnwch i ddull cwestiwn anodd a chewch ateb llyfn os yw' n iawn neu beidio. Gofynnwch i rai a maent yn aml yn cytuno, sy' n teimlo fel cadarnhad ac nid yw: rhannu data hyfforddi a rhannu mannau damweiniol. Mae ail ddull yn gwirio' r cyntaf yn dal yn yr un math o farn, a gellir siarad amdano. Ni all y cnewyllyn Lean. Mae' n deillio' r datganiad o' r axiomau a Mathlib, neu nid yw, ac nid oes gan ymddiriedaeth unrhyw effaith ar y canlyniad.
Mae'r ffyrdd arferol o ffagio profion swyddogol yn cael eu gwirio a'u gwrthod. Mae profion sy'n gadael twll gyda sorry, un sy'n apelio at native_decide i wneud i'r cnewyllyn wneud cyfrifiad ar ymddiriedaeth, neu un sy'n cyflwyno axiom newydd yn llym, yn cael eu canfod a'u gwrthod yn hytrach na'u cyfrif fel llwyddiant.
Beth y gall y panel ei wneud yn wir
Y rhan rhataf yw dadlau. Mae'r panel yn gweithio gyda'r llenyddiaeth - arXiv, OpenAlex, Crossref - felly dywedir canlyniad a wyddys yn hytrach na'i ail-ddiffinio'n wael. Mae ganddo SageMath a PARI/GP ar gyfer cyfrifo, Z3 a CVC5 ar gyfer datrys SMT, OEIS ar gyfer chwilio am ddilyniant y mae wedi ei adeiladu, a amgylchedd Python sandboxed heb fynediad rhwydwaith. Gellir profi dybiaeth yn erbyn deugain mil o achosion cyn i unrhyw un dreulio rownd yn ceisio ei brofi, a gorffennir y trafodaeth yn syth gan wrth-example.
Evidence, not eloquence
Ni sgorir cydweddiad ar ansawdd yr ymresymiadau. Mae'r honiad yn cael ei rannu i fesurau derbyn, a dim ond pan gellir ail-gadarnhau rhywbeth tu ôl iddo gan drydydd parti y caiff y meini prawf ei ddatrys: ffynhonnell gyda'r darn perthnasol wedi ei ddyfynnu, neu godau a weithredwyd yn wir gyda'i allbwn gwir. Mae'r barnwr yn ail-gadarnhau'r dystiolaeth ei hun cyn penderfynu, ac ni all ddweud bod y cydweddiad wedi gorffen tra bod meini prawf yn agored.
Chi sy'n gosod y bar
Mae' r safon yn eich dewis chi, a' r barnwr yn ei chadw' n llyfn. Gofynnwch am yr hyn y byddai arbenigwr gofalus yn ei dderbyn a chewch chi hynny. Gofynnwch am ddadl ddeductive llawn gyda phob rhagdybiaeth yn cael ei dynodi a chewch chi ei beirniadu yn erbyn hynny yn lle. Gofynnwch am y bar y byddai anfoniad gwobr yn wynebu, a' r canlyniad gwir yw yn aml cyfrif cywir o ble aeth y panel i lawr - sy' n werth mwy na dyfarniad cysurus y byddech chi' n ei wirio eich hunan beth bynnag.
I fod yn glir am hyn: nid yw hwn yn beiriant sy' n datrys problemau agored. Mae' n beiriant sy' n gwrthod gadael i ymresymiadau fynd heibio fel wedi' u datrys pan nad ydynt, ac sy' n dweud wrthych yn union pa gam a fethodd.
Ffurfio methu yw'r allbwn defnyddiol
Pan na fydd Lean yn cau' r dystiolaeth, cewch y nod cywir sy' n weddill. Yn ymarferol, mae' r nod yn aml yn y lle lle roedd y dadl anffurfiol yn chwythu' r dwylo - y cam y byddai pawb yn darllen y fersiwn proffwydol wedi cnoi drosto. Yna rhoddir y nod i' r sedd sy' n cael ei lleoli orau i ymosod arno, ynghyd â' r hyn sydd wedi' i geisio eisoes, a dim byd arall. Mae modelau' n torri pan maen nhw' n dal, yn ail- osod eu hunain ar gost llawn; mae pasio un cwestiwn penodol yn lle hynny yn aml yn datgloi am ddarn o' r tocynnau.
Mae gwaith hir yn goroesi
Mae pob lemma y gosod y panel yn mynd i gyfrif cyfranedig gyda'i brofion, felly mae'r canlyniadau yn cael eu ysgrifennu unwaith ac yn cael eu hail- gynhyrchu byth, a'r diweddfaoedd yn cael eu cofnodi fel nad oes neb yn mynd yn ôl i mewn iddynt. Rheda cydweddiadau ar ochr y gweinydd ac yn seibio'n lân - ar gyllideb, ar ddiffyg darparwr, neu oherwydd eich bod wedi cau'r tab - ac yn ailgychwyn yn union lle aethant i ben.
Beth nad yw hyn ar gyfer
Mae theorem yn air deductive. Mae'r safle yma wedi ei adeiladu ar gyfer mathemateg, rhesymeg, gwyddoniaeth cyfrifiadurol ddamcaniaethol, ffiseg ddamcaniaethol a theori economaidd - meysydd lle mae datganiad yn cael ei ddatrys gan brofi. Nid yw cwestiynau empirig yn y biolegol, meddygaeth, cemeg neu'r gwyddorau cymdeithasol yn cynhyrchu theorems, maent yn cynhyrchu canfyddiadau, ac ni fydd unrhyw faint o ffurfweddu yn eu penderfynu. Mae ein safle chwaer referee.chat yn rhedeg yr un broses panel-a-chyflwynydd heb y cam Lean, ar gyfer y cwestiynau hyn yn union.