Mizar 수학 라이브러리(MML) 미자르 기사 구성, 다음 두 기사는 이 데이터 세트의 기초를 형성합니다.

• 내장된 개념
• 타르스키-그로텐디크 집합 이론의 공리 미자르 수학 라이브러리(MML)는 미자르 언어에 기반한 수학적 형식주의 라이브러리로, 많은 저자와 유지 관리자에 의해 오랜 세월에 걸쳐 구축되었습니다. 미자르 언어는 수학적 정리, 증명 및 관련 개념을 설명하는 컴퓨터가 읽을 수 있는 언어입니다. 미자르 수학 라이브러리에는 논리, 대수, 분석, 기하학 등 광범위한 수학 분야를 포괄하는 정형화된 수학적 정리와 증명이 포함되어 있습니다. 이 라이브러리의 목표는 자동화된 정리 증명과 형식적 추론을 위한 견고한 수학적 기반을 제공하는 것입니다. 지금까지 미자르 언어 시스템은 거대한 미자르 수학 라이브러리를 형성했으며, 이는 향후 수학과 관련 문제에 대한 논의를 위한 좋은 토대를 마련했습니다.