About Theorem.chat
Theorem.chat ņem matemātisku prasību un cenšas to nokārtot. Jūs paziņojat prasību, un standartu, kas tai ir jāatbilst. Panelis AI modeļu — cik daudz jūs vēlaties, no kura pārdevēji vēlaties — uzbrūk to, un vēl viens modelis tiesnešiem. Tad arguments tiek oficiāli noteikts Lean 4 pret Mathlib, un Lean kodols nolemj, vai tas ir pierādīts. Šis pēdējais solis ir produkts.
Kāpēc kodols, nevis cits modelis
Uzdot modeli grūti jautājums, un jūs saņemsiet brīvu atbildi, vai tas ir pareizi, vai ne. Uzdodiet vairākas un tās bieži vien piekrīt, kas jūtas kā apstiprinājums un nav: modeļi dalīties apmācības datus un dalīties aklās vietas. Otrais modelis pārbauda pirmo joprojām ir tāds pats spriedums, un to var runāt apaļas. Lean kodols nevar. Tas vai nu izriet no paziņojumu no aksiomas un Mathlib, vai arī tas nav, un uzticība nav ietekme uz iznākumu.
Parastie veidi, kā viltot oficiālu pierādījumu tiek pārbaudīta un noraidīta. Pierādījumu, kas atstāj caurumu ar sorry, viens, kas vēršas pie native_decide, lai kodols veikt aprēķinus par uzticību, vai tāds, kas klusi ievieš jaunu aksioma, tiek atklāta un noraidīta, nevis tiek uzskatīta par veiksmi.
Ko panelis patiesībā var darīt
Arguments ir lēta daļa. Panelis strādā ar literatūru — arXiv, OpenAlex, Crossref — tāpēc zināms rezultāts tiek minēts nevis no jauna radīts slikti. Tas ir SageMath un PARI/GP, lai aprēķinātu, Z3 un CVC5 SMT atrisināšanai, OEIS meklēt, lai identificētu secību, kas ir konstruēts, un smilšu kaste Python vide bez tīkla piekļuves. Pieņēmums var pārbaudīt pret desmit tūkstošiem gadījumu, pirms kāds pavada apaļs mēģina to pierādīt, un pretpiemērs tūlīt beidzas diskusija.
Pierādījumi, nevis daiļrunība
Matching nav vērtēta pēc argumentu kvalitātes. Prasījums tiek sadalīts pieņemšanas kritērijos, un kritērijs tiek nokārtots tikai tad, kad kaut kas aiz tā var tikt atkārtoti pārbaudīts ar trešo personu: avots ar citu attiecīgo fragmentu, vai kods, kas faktiski izpildīts ar tā faktisko rezultātu. Referents atkārtoti pārbauda, ka pats pierādījums ir pieņemts, un tas nevar deklarēt, ka pretruna pabeigta, kamēr kritērijs joprojām ir atvērts.
Tu uzstādīji bāru
Standarta ir jūsu izvēlēties, un tiesnesis tur to burtiski. Jautāt par to, ko uzmanīgi eksperts varētu pieņemt, un jūs saņemsiet, ka. Jautājiet par pilnīgu atskaitošu argumentu ar katru pieņēmumu, kas norādīts, un jūs saņemsiet spriedzi pret to vietā. Lūdziet bāru balvu iesniegšanas saskarties, un godīgu iznākumu parasti ir precīzs konts par to, kur panelis samazinājās īss — kas ir vērts vairāk nekā pārliecināts apgalvojums jums būtu jāpārbauda sevi vienalga.
Lai būtu skaidrs: šī nav mašīna, kas atrisina atklātas problēmas, tā ir mašīna, kas atsakās ļaut strīdiem iet, kā noteikts, ja tā nav, un kas jums skaidri norāda, kurš solis neizdevās.
Neveiksmīga formalizācija ir noderīga izlaide
Kad Lean nebūs slēgt pierādījumu, jūs saņemsiet precīzu mērķi, kas paliek. Praksē, kas ir gandrīz vienmēr vieta, kur neoficiālais arguments bija roku skalošana — solis visi lasot prose versija būtu nodded pagātni. Šis mērķis tiek nodots tad, kurš sēdeklis ir vislabāk novietots, lai uzbruktu to, kopā ar to, kas jau ir izmēģināts, un nekas cits. Modeļi thrash kad tie ir iestrēdzis, atjaunojas par pilnu cenu; izejot viens konkrēts jautājums, nevis parasti atbloķējot bloķēt daļu no žetoniem.
Ilgs darbs izdzīvo
Katra lemma panelis nosaka iet uz kopīgu ledāju ar tās pierādījumu, tāpēc rezultāti tiek rakstīti vienreiz un nekad atkārtoti iegūti, un mirušie gali tiek ierakstīti tā, lai neviens iet atpakaļ uz tiem. Matches palaist serveru pusē un apturēt tīri — par budžetu, par piegādātāju atbīdām, vai tāpēc, ka jūs aizvēra cilni - un atsākt tieši, kur tie apstājās.
Ko tas nenozīmē
Theorem ir atskaitošs vārds. Šī vietne ir izveidota matemātikas, loģika, teorētisko datorzinātņu, teorētisko fiziku un ekonomikas teorija — jomas, kur prasība tiek nokārtota ar pierādījumu. Empīriskie jautājumi bioloģija, medicīnā, ķīmija vai sociālās zinātnes neražo teorēmu, tie rada secinājumus, un nav summa formalizācijas lems tos. Mūsu māsa vietne referee.chat vada to pašu paneli-un referente process bez Lean solis, tieši šiem jautājumiem.