Theorem.chat орчим
Theorem.chat математикийн дүгнэлт авч түүнийг шийдэх гэж оролддог. Та дүгнэлт, стандартыг нь тодорхойлно. Таны хүссэн тооны, ямар ч үйлдвэрлэгчээс ирсэн AI загварууд үүнийг дайрч, нэг загвар нь шүүгчээр ажиллана. Дараа нь аргументыг Lean 4- Mathlib- тэй харьцуулан Lean 4- Mathlib- ийн хооронд илэрхийлж, Lean kernel нь үүнийг баталгаажуулах эсэхийг шийднэ. Сүүлд нь гарсан үр дүн нь Theorem.chat- ийн үр дүн юм.
Яагаад өөр загвар биш, харин kernel-ийг сонгох ёстой вэ?
Модельээс хүнд асуулт асуувал зөв эсэх нь тодорхой хариулт гарна. Заримдаа хэд хэдэн асуулт асуухад тэд санал нэгддэг, энэ нь баталгаажуулалт мэт санагдана, гэхдээ тийм биш: загварууд сургалтын мэдээллийг хуваалцаж, хараагүй талуудыг хуваалцдаг. Эхнийх нь шалгасан хоёр дахь загвар нь яг адилхан шүүлт бөгөөд үүнийг хэлэлцэж болно. Lean kernel- ийн хувьд тийм биш. Энэ нь аксиом болон Mathlib- аас дүгнэлт гаргадаг, эсвэл гаргадаггүй, найдвартай байдал нь үр дүнд нөлөөлөхгүй.
Формаль баталгаажуулалтыг хууран мэхлэх уламжлалт арга нь шалгагдана. sorry-тэй нийцэхгүй, native_decide-д хандаж kernel-ийг итгэхүйц тооцоолол хийхийг шаардах, эсвэл шинэ аксиомыг нууцаар оруулсан баталгаажуулалт нь амжилттай гэж тооцогдохгүйгээр илрүүлж, үгүйсгэгддэг.
Панелийн хийж чадах зүйл
Сэтгэл хөдлөл нь үнэгүй хэсэг юм. Панель нь arXiv, OpenAlex, Crossref зэрэг ном зохиолуудтай ажилладаг тул сайн мэддэг үр дүнг буруугаар дахин үүсгэхээс илүүтэй иш татах нь дээр. Энэ нь тооцоолол хийхэд SageMath ба PARI/GP, SMT шийдэхэд Z3 ба CVC5, бүтээгдсэн урсгалыг тодорхойлох OEIS хайлт, сүлжээний нэвтрэлтгүй sandboxed Python орчныг агуулдаг. Нэг таамаглалыг хэн нэгэн үүнийг батлах гэж оролдохоос өмнө 10,000 тохиолдол дээр туршиж болно, эсрэг жишээ нь яриаг шууд дуусгана.
Шүүмжлэл биш, нотолгоо
match нь аргументын чанарын хувьд оноо авдаггүй. Энэ нь хүлээн авах шалгуураар хуваагддаг ба шалгуур нь зөвхөн гуравдагч этгээдийн эргэн шалгах боломжтой бол л шийдвэрлэгдэнэ: эх сурвалж нь холбогдох хэсгийг иш татан, эсвэл код нь бодит үр дүнтэй нь гүйцэтгэгдсэн. Шүүгч шийдвэрлэхээс өмнө энэхүү баримтыг дахин шалгадаг ба шалгуур нь нээлттэй байгаа үед match- ийг дууссан гэж зарлах боломжгүй.
Та хэмжүүрийг тогтоосон
Стандарт нь таны сонголт бөгөөд шүүгч үүнийг шууд утгаар нь барьдаг. Нэмэлт асуулт асууж, та үүнийг олж авах болно. Бүх таамаглалыг багтаасан бүрэн дүгнэлт асууж, та үүнийг эсэргүүцэж шүүгдэнэ. шагнал өгөхөд тулгарах бэрхшээлийг асууж, үнэнч үр дүн нь ихэвчлэн таны өөрөө шалгах ёстой найдвартай дүгнэлтээс илүү үнэ цэнэтэй, хэрэв та үүнийг олж авсан бол, таныг хэр их алдаж байгааг тодорхойлох болно.
Энэ нь нээлттэй асуудлыг шийддэг машин биш. Энэ нь шийдэгдээгүй аргументыг шийдэгдсэн гэж хүлээн зөвшөөрөхгүй, мөн ямар алхам алдаатайг танд зааж өгдөг машин юм.
Үгүй болсон хэлбэржүүлэлт нь ашигтай гарчиг юм
Хэрэв Lean- ийн баталгаа нь дуусаагүй бол, та үлдсэн зорилгоо олж авна. Практик дээр энэ нь ихэвчлэн маргааныг гараараа дохиж байгаа газар байдаг - энэ нь зохиолын хувилбарыг уншсан бүх хүн толгойгоо сэгсэрч өнгөрөх алхам юм. Энэ зорилго нь үүнийг дайрах хамгийн тохиромжтой байранд, аль хэдийн туршсан зүйлтэй хамт, өөр юу ч байхгүй. Модельүүд түгжээд байвал, бүрэн үнээр дахин илэрхийлэх; харин тодорхой асуулт өгвөл ихэвчлэн тэмдэгтүүдийн хэсэгт блокыг арилгах.
Хэт урт ажил
Панелийн тогтоосон бүх леммүүд нь баталгаатайгаар хуваалцсан дансанд ордог, ингэснээр үр дүнг нэг удаа бичиж дахин гаргаж авахгүй, мөн түгжрэлүүд нь тэмдэглэгддэг тул хэн ч үүнийг дахин бичиж болохгүй. Matches серверийн талд ажилладаг ба чимээгүйхэн зогсоно - төсөв, үйлчилгээ үзүүлэгч гэмтсэн, эсвэл та хавтсыг хаасан - мөн зогсож байсан газраас нь үргэлжлүүлнэ.
Энэ нь юуг зааж өгөхгүй вэ
Теорема бол дүгнэлттэй үг юм. Энэ сайт нь математик, логик, онолын компьютерийн шинжлэх ухаан, онолын физик, эдийн засгийн онол - эдгээр салбарт дүгнэлтийг баталгаажуулахад зориулагдсан юм. Биологи, анагаах ухаан, химийн шинжлэх ухаан, нийгмийн шинжлэх ухааны туршилтын асуултууд нь теорема гаргаж ирдэггүй, харин дүгнэлт гаргадаг бөгөөд ямар ч хэлбэржүүлэлт шийдэж чадахгүй. Манай найз сайт referee.chat нь яг л энэ асуултуудад Lean алхмыг ашиглахгүйгээр адилхан panel- and- referee процессыг ажиллуулдаг.