Apie Theorem.chat
Theorem.chat imasi matematinį reikalavimą ir bando jį išspręsti. Jūs pareiškiate pretenziją, ir standartą, kurį ji turi atitikti. AI modelių grupė – tiek, kiek norite, iš kurio pardavėjo norite – atakuoja jį, ir dar vienas Modelis teisėjai. Tada argumentas yra formalizuotas Lean 4 prieš Mathlib, ir Lean branduolys nusprendžia, ar tai yra įrodyta. Šis paskutinis žingsnis yra produktas.
Kodėl branduolys, o ne kitas modelis
Užduoti modelį sunku klausimą ir jūs gaunate sklandų atsakymą, ar jis yra teisingas, ar ne. Klausti keletą ir jie dažnai sutinka, kuris jaučiasi patvirtinimas ir nėra: modeliai dalintis mokymo duomenis ir dalintis aklus taškus. Antrasis modelis tikrinant pirmąjį vis dar yra tos pačios rūšies sprendimą, ir ji gali būti kalbama apie apvalus. Lean branduolys negali. Ji arba gauti pareiškimą iš aksioma ir Mathlib, arba ji neturi įtakos, ir pasitikėjimas neturi įtakos rezultatą.
Paprastai būdai, kaip suklastoti formalus įrodymas yra tikrinamas ir atmetamas. Įrodymas, kad palieka skylę su sorry, vienas, kuris kreipiasi į native_decide padaryti branduolys imtis skaičiavimo dėl pasitikėjimo, arba vienas, kad tyliai pristato naują aksioma, yra aptinkamas ir atmetamas, o ne skaičiuojama kaip sėkmė.
Ką iš tikrųjų gali padaryti grupė
Argumentas yra pigus dalis. Panelė dirba su literatūra — arXiv, OpenAlex, Crossref — todėl žinomas rezultatas yra nurodytas, o ne iš naujo iš naujo prastai. Ji turi SageMath ir PARI/GP skaičiavimo, Z3 ir CVC5 SMT sprendimo, OEIS ieškoti nustatyti seką ji yra pastatyta, ir smėlio dėžės Python aplinkos be tinklo prieigos. Spektaklis gali būti bandomas su dešimt tūkstančių atvejų, kol kas nors praleidžia apvalą bando įrodyti, kad tai, ir priešpriešinis pavyzdys nedelsiant užbaigia diskusiją.
Įrodymai, o ne iškalba
Atitiktis nėra vertinama pagal argumentų kokybę. Pretenzijos yra suskirstytos į priėmimo kriterijus, o kriterijus yra nustatomas tik tada, kai kai kažkas už jį gali būti patikrintas trečiosios šalies: šaltinis su nurodyta atitinkama ištrauka, arba kodas, kuris buvo faktiškai įvykdytas su realia išeiga. Atsakytojas pakartotinai patikrina, kad prieš priimant sprendimą įrodymai yra pateikti, ir jis negali deklaruoti, kad prieš tai atitikmuo užbaigtas, kol kriterijus vis dar yra atviras.
Tu nustatai barą
Standartas yra jūsų pasirinkti, ir teisėjas turi jį tiesiogine prasme. Paklausti, ką atsargus ekspertas priimti, ir jūs gaunate, kad. Paprašyti pilną atskaityti argumentą su kiekviena prielaida nurodyta ir jums priimti prieš tai vietoj. Prašyti už barą prizą pateikti susiduria, ir sąžiningas rezultatas paprastai yra tiksli sąskaita, kur skydas sumažėjo trumpas – kuris yra verta daugiau nei patikimas pretenzijos jums turėtų patikrinti save vis tiek.
Tai ne mašina, kuri sprendžia problemas.Tai mašina, atsisakanti leisti argumentui praeiti, kaip nustatyta, kai ne, ir kuri tiksliai nurodo, kuris žingsnis nepavyko.
Nepavykęs formalizavimas yra naudingas rezultatas
Kai Lean nebus uždaryti įrodymą, jūs gaunate tikslų tikslą, kuris lieka. Praktikoje, kad beveik visada yra vieta, kur neformalus argumentas buvo rankinio valymo – žingsnis visi skaitant prose versija būtų ``a praeities. Šis tikslas tada buvo perduotas bet kokia vieta yra geriausiai jį atakuoti, kartu su tuo, kas jau buvo bandyta, ir nieko kita. Modeliai stresas, kai jie įstrigę, atstatant save už visą kainą; išdavimas vieną konkretų klausimą vietoj to paprastai atblokuoja dalis žetonų.
Ilgas darbas išlieka
Kiekvienas lemma skydas nustato eina į bendrą ledger su savo įrodymais, todėl rezultatai yra parašyta kartą ir niekada iš naujo, ir mirusiųjų galai yra įrašyti taip niekas eina atgal į juos. Rungtynės paleisti serverio pusėje ir sustabdyti švariai – dėl biudžeto, dėl teikėjo atjungimo, arba dėl to, kad jūs uždarė kortelę – ir atnaujinti tiksliai, kur jie sustojo.
Tai ne tam, kad
Theorem yra atskaitytinis žodis. Ši svetainė yra pastatyta matematikos, logika, teorinės kompiuterinės mokslo, teorinės fizikos ir ekonomikos teorija — sritys, kuriose pretenzija yra sprendžiama įrodymu. Empīriški klausimai biologijos, medicinos, chemijos ar socialinių mokslų negamina teoremai, jie gamina išvadas, ir jokios formalizavimo suma bus nuspręsti juos. Mūsų sesuo svetainė referee.chat eina tą patį skydelio ir referento procesas be Lean žingsnis, tiksliai šių klausimų.
referee.chat – ta pati mintis, kai kalbama apie empirinius reikalavimus