Theorem.chat ግምገማ
Theorem.chat የቁጥር ጥያቄን ይወስዳል እና ለመፍታት ይሞክራል. ጥያቄውን እና ደረጃውን መሟላት አለበት. የ AI ሞዴሎች ፓነል - እንደፈለጉ ብዙ ፣ ከፈለጉት ሻጮች - ይቃወማል ፣ እና አንድ ሞዴል የበለጠ ተከራካሪ. ከዚያም Lean 4 በ Mathlib ላይ ግልጽ ነው ፣ እና የሊን ኮርኔል የተረጋገጠ ነው ወይስ አይደለም የሚወስን. ይህ የመጨረሻው ደረጃ ምርት ነው ፡፡
ለምን የካርኔል እና ሌላ ሞዴል አይደለም
ሞዴል አስቸጋሪ ጥያቄ ጠይቅ እና ትክክል ወይም አይደለም ከሆነ ፈጣን መልስ ያገኛሉ. ብዙዎች ይጠይቁ እና ብዙውን ጊዜ ይግባባሉ, ይህ እንደ ማስረጃ እና አይደለም: ሞዴሎች የልማት መረጃን እና የግልጽ ቦታዎችን ይጋራሉ. ሁለተኛ ሞዴል የመጀመሪያውን የሚፈተሽ አሁንም የፍርድ ዓይነት ነው, እና ሊነጋገሩ ይችላሉ. የ Lean ኮርነል አይችልም. ወይም ከ axioms እና Mathlib መግለጫን ያመጣል, ወይም አያደርግም, እና እምነት በውጤቱ ላይ ምንም ተጽዕኖ የለውም.
የቀድሞው የግልጽ ማስረጃን ለመቅጠል የተለመዱ መንገዶች ይመረመራሉ እና ይቃወማሉ. sorry ጋር ግድግዳ የሚተው ማስረጃ፣ native_decide ን በመጠየቅ ኬርኔል በታማኝነት ላይ መቁጠር እንዲወስድ የሚያደርግ ወይም አዲስ ክስዮምን በደስታ የሚያቀርብ፣ ይመረመራል እና እንደ ውጤት ከመቆጠብ ይልቅ ይቃወማል
ፓነሉ ምን ማድረግ እንደሚችል
መከራከር የቀላል ክፍል ነው. ፓነል በጽሑፍ ጋር ይሠራል - arXiv, OpenAlex, Crossref - ስለዚህ የተታወቀ ውጤት መጥፎ በሆነ መንገድ ከሚመጣው ይልቅ የተጠቀሰ ነው. ለቁጠባ SageMath እና PARI/GP, Z3 እና CVC5 ለ SMT መፍታት, OEIS ፈልግ ለተከታታይ ለይቶ ለማወቅ, እና sandboxed Python አካባቢ ያለ ኔትወርክ መዳረሻ. አንድ ጥርጣሬ በአንድ ሰው ለማሳየት ለመሞከር አንድ ዙር ከመውሰድ በፊት በደመ ሺህ ጉዳዮች ላይ ሊሞከር ይችላል, እና counterexample ውይይቱን በፍጥነት ያጠናቅቃል.
ማስረጃ፣ ተናጋሪነት አይደለም
ተመሳሳይ በጥያቄ ጥራት ላይ አይቆጠርም. ጥያቄው ወደ ተቀባይነት መስፈርቶች ይቀየራል, እና መስፈርት ብቻ ነው ተከታትሎ ነገር ኋላ ሦስተኛ ወገን ሊሆን ይችላል ጊዜ ይከሰታል: ምንጭ ጋር የተያያዘ ክፍል የተጠቀሰው, ወይም ኮድ በእውነቱ ጋር እውነተኛ ውጤት ጋር ተካሂዷል. ተከታዩ በፊት ፍርድ ማስረጃውን በራሱ ይቆጣጠራል, እና መስፈርት ገና ክፍት ነው ጊዜ ተመሳሳይ ተከታትሎ ሊሆን አይችልም.
ባር
የምርጫው ደረጃ የእርስዎ ነው፣ እናም ፍርድ ቤቱ በቃላት ያስተላልፋል. ጥብቅ ባለሙያ የሚቀበልበትን ነገር ይጠይቁ እና ያንን ያገኛሉ. የተገለጸው ሁሉንም ጥርጣሬዎች የሚይዝ የተሟላ ግልጽነት የሚጠይቅ ክርክር ይጠይቁ እና በእሱ ላይ ትፈርዳላችሁ. የሽልማት ቀርቦት የሚጋፈጥበትን ባር ይጠይቁ፣ እና እውነተኛው ውጤት በብዛት የፓነሉ የት ረዘም ያለ ጊዜ ወስዶ እንደነበር ትክክለኛ መግለጫ ነው - ይህም ከራስዎን ማረጋገጥ ከሚያስፈልግዎት ከማረጋገጫ በላይ ዋጋ ያለው ነው.
ስለእርሱ ለመረዳት: ይህ የከፈቱ ችግሮችን የሚፈታ ማሽን አይደለም. ይህ ያልሆነበት ጊዜ መከራከሪያን እንደተፈታ የሚፈቅድ ማሽን ነው, እና ያ የትኛው እርምጃ ተሳስቷል ብለው በትክክል ያሳያችኋል.
የፈተናው ውጤት
ሌን ማስረጃውን ሲያዘጋጅ፣ የሚቀረው ትክክለኛ ዓላማን ማግኘት ይችላሉ። በተግባር ግን ይህ ሁልጊዜ የግልጽነት ክርክር እጅ-መነፋት የነበረበት ቦታ ነው - የፕሮስ ቅርጸት ማንኛውም ሰው ማንበብ የሚችልበት እርምጃ ኋላ ላይ ይነሳል። ይህ ዓላማ ከዚያ በኋላ ለየትኛውም መቀመጫ ለተቃወሙት በጣም የተሻለ ቦታ ነው፣ ከዚህ በፊት የተሞከረውን እና ሌላ ምንም ነገር ጋር። ሞዴሎች ተከማችተው ሲገቡ ይደመሰሳሉ፣ በሙሉ ዋጋ ራሳቸውን በራሳቸው ይቀይራሉ፤ በምትኩ አንድን ትክክለኛ ጥያቄ መውሰድ በዋነኝነት ለቶኬኖች ክፍል ለመክፈት ይዘጋል ፡፡
የረጅም ጊዜ ስራዎች
ሌማ እያንዳንዱ ፓነል የሚፈጥረው ወደ ተጋራ መጻሕፍት ጋር ማስረጃው ይሄዳል, ስለዚህ ውጤቶች አንድ ጊዜ ይጻፋሉ እና ፈጽሞ re-derived, እና dead ends ይመዝገቡ ስለዚህ ማንም ወደ እነርሱ ተመልሶ ይሄዳል. ጨዋታዎች ሰርቨር-በኩል ይሮጡ እና ንጹህ አቁም - በገንዘብ, በ provider ወቅት, ወይም ምክንያቱም እርስዎ መክፈቻ - እና ቀጥል በትክክል እነርሱ ከተቆሙበት ቦታ.
ይህ ለ
ቴዎሬም ተቀባይ ቃል ነው. ይህ ጣቢያ ለ ቁጥሮች, ሎጂክ, ቴዎሪ ኮምፒውተር ሳይንስ, ቴዎሪ ፊዚክስ እና ኢኮኖሚ ቴዎሪ - መስኮች ውስጥ አንድ ጥያቄ በ ማስረጃ የተፈታ ነው የተገነባ. empirical ጥያቄዎች በ biology, medicine, chemistry ወይም ማህበራዊ ሳይንስ ቴዎሬሞች አይፈጥሩም, እነርሱ ውጤቶች ይፈጥራሉ, እና ምንም መጠን የ formalization እነርሱን ይፈርማል. የእኛ እህት ጣቢያ referee.chat ተመሳሳይ ፓነል-and-referee ሂደት ያለ ሌን እርምጃ, ለ እነዚህ ጥያቄዎች በትክክል ይሠራል.