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 тохиолдол дээр туршиж болно, эсрэг жишээ нь яриаг шууд дуусгана.
Шүүмжлэл биш, нотолгоо
Тоглоомын чанарыг аргументын чанараар үнэлэхгүй. Тоглоомын чанарыг хүлээн авах шалгуураар үнэлдэг бөгөөд шалгуур нь зөвхөн гуравдагч этгээдийн баталгаажуулсан, тухайлбал, эх сурвалж, холбогдох өгүүлбэр, эсвэл кодыг бодит үр дүнтэй нь гүйцэтгэсэн тохиолдолд л шийдэгддэг. Шүүгч шийдвэр гаргахаас өмнө энэхүү баталгааг дахин шалгадаг ба шалгуур нь нээлттэй байгаа үед тохирохыг дуусгавар гэж зарлах боломжгүй.
Та хэмжүүрийг тогтоосон
Стандарт нь таны сонголт бөгөөд шүүгч үүнийг шууд утгаар нь барьдаг. Нэмэлт асуулт асууж, та үүнийг олж авах болно. Бүх таамаглалыг багтаасан бүрэн дүгнэлт асууж, та үүнийг эсэргүүцэж шүүгдэнэ. шагнал өгөхөд тулгарах бэрхшээлийг асууж, үнэнч үр дүн нь ихэвчлэн таны өөрөө шалгах ёстой найдвартай дүгнэлтээс илүү үнэ цэнэтэй, хэрэв та үүнийг олж авсан бол, таныг хэр их алдаж байгааг тодорхойлох болно.
Энэ нь нээлттэй асуудлыг шийддэг машин биш. Энэ нь шийдэгдээгүй аргументыг шийдэгдсэн гэж хүлээн зөвшөөрөхгүй, мөн ямар алхам алдаатайг танд зааж өгдөг машин юм.
Үгүй болсон хэлбэржүүлэлт нь ашигтай гарчиг юм
Хэрэв Lean- ийн баталгаа нь дуусаагүй бол, та үлдсэн зорилгоо олж авна. Практик дээр энэ нь ихэвчлэн маргааныг гараараа дохиж байгаа газар байдаг - энэ нь зохиолын хувилбарыг уншсан бүх хүн толгойгоо сэгсэрч өнгөрөх алхам юм. Энэ зорилго нь үүнийг дайрах хамгийн тохиромжтой байранд, аль хэдийн туршсан зүйлтэй хамт, өөр юу ч байхгүй. Модельүүд түгжээд байвал, бүрэн үнээр дахин илэрхийлэх; харин тодорхой асуулт өгвөл ихэвчлэн тэмдэгтүүдийн хэсэгт блокыг арилгах.
Хэт урт ажил
Панелийн тогтоосон бүх леммүүд нь баталгаатайгаар хуваалцсан дансанд ордог, ингэснээр үр дүнг нэг удаа бичиж дахин гаргахгүй, түгжрэлүүдийг тэмдэглэж хэн ч буцаж орохгүй. Тоглоомууд серверийн талд явагдаж, төсвийн дагуу, үйлчилгээ үзүүлэгч тасрах үед, эсвэл та хавтсыг хаасан үед цэвэрхэн түр зогсож, зогсож байсан газраас нь үргэлжлүүлнэ.
Энэ нь юуг зааж өгөхгүй вэ
Теорема бол дүгнэлттэй үг юм. Энэ сайт нь математик, логик, онолын компьютерийн шинжлэх ухаан, онолын физик, эдийн засгийн онол - эдгээр салбарт дүгнэлтийг баталгаажуулахад зориулагдсан юм. Биологи, анагаах ухаан, химийн шинжлэх ухаан, нийгмийн шинжлэх ухааны туршилтын асуултууд нь теорема гаргаж ирдэггүй, харин дүгнэлт гаргадаг бөгөөд ямар ч хэлбэржүүлэлт шийдэж чадахгүй. Манай найз сайт referee.chat нь яг л энэ асуултуудад Lean алхмыг ашиглахгүйгээр адилхан panel- and- referee процессыг ажиллуулдаг.