HyperAI

مجموعة بيانات الرياضيات الميزار

التاريخ

منذ عام واحد

رابط النشر

mizar.org

الترخيص

CC BY 4.0

مساعدة التنزيل

مكتبة الميزار الرياضية (MML) بواسطة مقالات الميزار التكوين، تشكل المقالتان التاليتان الأساس لهذه المجموعة من البيانات.

مكتبة مزار الرياضية (MML) هي مكتبة شكلية رياضية تعتمد على لغة مزار، والتي تم بناؤها على مدى سنوات عديدة من قبل العديد من المؤلفين والمطورين. اللغة الميزار هي لغة قابلة للقراءة بواسطة الحاسوب لوصف النظريات الرياضية والبراهين والمفاهيم ذات الصلة. تحتوي مكتبة مزار للرياضيات على نظريات وإثباتات رياضية رسمية تغطي مجموعة واسعة من المجالات الرياضية بما في ذلك المنطق والجبر والتحليل والهندسة وما إلى ذلك. والهدف من هذه المكتبة هو توفير أساس رياضي متين لإثبات النظريات الآلية والاستدلال الرسمي. حتى الآن، شكل نظام اللغة الميزارية مكتبة رياضية ضخمة، والتي وضعت أساسًا جيدًا للمناقشات المستقبلية حول الرياضيات والقضايا ذات الصلة.