Maidir le Theorem.chat
Glacann Theorem.chat éileamh matamaiticiúil agus déanann sé iarracht é a shocrú. Luaitear an t-éileamh, agus an caighdeán a chaithfidh sé a chomhlíonadh. Painéal de mhúnlaí AI - mar go leor is mian leat, ó cibé díoltóirí is mian leat - ionsaí air, agus ceann amháin níos mó réiteoirí samhail. Ansin tá an argóint foirmiúil i Lean 4 i gcoinne Mathlib, agus cinneann an eithne Lean cibé an bhfuil sé cruthaithe. Is é an táirge an chéim dheireanach sin.
Cén fáth a bhfuil eithne, agus ní samhail eile
Iarr ar samhail ceist chrua agus gheobhaidh tú freagra líofa cibé acu atá sé ceart nó nach bhfuil. Iarr roinnt agus aontaíonn siad go minic, a mhothaíonn cosúil le daingniú agus nach bhfuil: samhlacha roinnt sonraí oiliúna agus pointí dall a roinnt. Tá an dara samhail a sheiceáil an chéad fós ar an gcineál céanna breithiúnas, agus is féidir é a labhairt timpeall. Ní féidir leis an eithne Lean. Díorthaíonn sé an ráiteas ó na axioms agus Mathlib, nó ní dhéanann sé, agus níl aon éifeacht ag muinín ar an toradh.
Déantar na gnáthbhealaí chun cruthúnas foirmiúil a bhréagnú a sheiceáil agus a dhiúltú. Déantar cruthúnas a fhágann poll le sorry, ceann a dhéanann achomharc chuig native_decide chun an eithne a dhéanamh ríomh ar iontaoibh, nó ceann a thugann axiom nua isteach go ciúin, a bhrath agus a dhiúltú seachas a chomhaireamh mar rath.
Cad is féidir leis an bpainéal a dhéanamh i ndáiríre
Is é an chuid saor a argóint. Oibríonn an painéal leis an litríocht - arXiv, OpenAlex, Crossref - mar sin luaitear toradh ar eolas seachas athdhíorthaigh go dona. Tá SageMath agus PARI/GP aige le haghaidh ríomhaireachta, Z3 agus CVC5 le haghaidh réiteach SMT, OEIS lorg chun seicheamh a thóg sé a aithint, agus timpeallacht Python sandboxed gan rochtain ar líonra. Is féidir toimhde a thástáil i gcoinne deich míle cás sula gcaitheann duine ar bith babhta ag iarraidh é a chruthú, agus críochnaíonn frithshampla an plé láithreach.
Fianaise, ní eloquence
Ní dhéantar comhoiriúnacht a scóráil ar cháilíocht argóintí. Déantar an t-éileamh a bhriseadh síos ina chritéir ghlactha, agus ní shocraítear critéar ach amháin nuair is féidir le tríú páirtí rud éigin taobh thiar de a ath-sheiceáil: foinse leis an sliocht ábhartha luaite, nó cód a rinneadh i ndáiríre lena fhíor-aschur. Ath-seiceáil an réiteoir an fhianaise sin féin roimh rialú, agus ní féidir leis an gcomhoiriúnacht a dhearbhú críochnaithe fad is atá critéar fós oscailte.
Leag tú an barra
Is é an caighdeán atá agat a roghnú, agus tá an réiteoir sé literally. Iarr ar cad a bheadh saineolaí cúramach glacadh leis agus a fhaigheann tú sin. Iarr ar argóint iomlán díorthach le gach toimhde a luaitear agus a fhaigheann tú a mheas in aghaidh sin in ionad. Iarr ar an mbarra bheadh aighneacht duais aghaidh, agus is é an toradh macánta de ghnáth cuntas beacht ar an áit a thit an painéal gearr - a bhfuil fiú níos mó ná éileamh muiníneach a bheadh agat a sheiceáil féin ar aon nós.
Chun a bheith soiléir faoi: ní meaisín é seo a shocraíonn fadhbanna oscailte, meaisín é a dhiúltaíonn argóint a chur ar aghaidh mar a shocraítear nuair nach bhfuil sí, agus a insíonn duit go díreach cén chéim a theip.
Is é foirmiú teipthe an t-aschur úsáideach
Nuair nach mbeidh Lean dúnadh an cruthúnas, gheobhaidh tú an sprioc cruinn go bhfuil fós. I gcleachtas go bhfuil beagnach i gcónaí ar an láthair ina raibh an argóint neamhfhoirmiúil lámh-waving — an chéim gach duine ag léamh an leagan próis a bheadh nodded anuas. Go sprioc a thabhairt ansin ar láimh do cibé suíochán is fearr a chur chun ionsaí air, chomh maith leis an méid atá iarracht cheana féin, agus aon rud eile. Samhlacha thrash nuair a bhíonn siad greamaithe, ath-léiriú iad féin ar chostas iomlán; ag dul ceist amháin ar leith in ionad unblocks de ghnáth le haghaidh codán de na comharthaí.
Maireann obair fhada
Téann gach lemma a bhunaíonn an painéal isteach i mórleabhar comhroinnte lena chruthúnas, mar sin scríobhtar torthaí uair amháin agus ní athdhíorthaítear iad, agus déantar críocha marbh a thaifeadadh ionas nach dtéann aon duine ar ais isteach iontu.Matches reáchtáil taobh freastalaí agus sos glan - ar bhuiséad, ar mhífheidhm soláthraí, nó toisc gur dhún tú an cluaisín - agus atosú go díreach nuair a stop siad.
Cad nach bhfuil sé seo le haghaidh
Is focal díorthach é teoirim. Tá an suíomh seo tógtha do mhatamaitic, loighic, ríomheolaíocht theoiriciúil, fisic theoiriciúil agus teoiric eacnamaíoch — réimsí ina socraítear éileamh trí chruthúnas. Ní tháirgeann ceisteanna eimpíreacha sa bhitheolaíocht, sa leigheas, sa cheimic nó sna heolaíochtaí sóisialta teoirimí, táirgeann siad torthaí, agus ní chinnfidh aon mhéid foirmiúcháin iad. Ritheann ár suíomh deirfiúr referee.chat an próiseas céanna painéal-agus-mharcála gan an chéim Lean, do na ceisteanna sin go díreach.
referee.chat — an smaoineamh céanna, le haghaidh éilimh eimpíreach