متامث

متامث (به انگلیسی: Metamath) زبانی برای توسعه تعاریف و برهان‌های ریاضیات صوری^[1] همراه با بررسی برهان و پایگاه داده در حال رشدِ هزاران قضایای اثبات شده با پوشش نتایجی مرسوم در منطق، نظریه مجموعه‌ها، نظریه اعداد، نظریه گروه‌ها، جبر، آنالیز و توپولوژی است همچنین موضوعاتی در فضاهای هیلبرت و منطق کوانتومی.^[2]

متامث
Metamath

توسعه‌دهنده(ها)	نرمن مگیل
مخزن	github.com/metamath/metamath-exe
سیستم‌عامل	لینوکس، ویندوز، مکینتاش
در دسترس به	آنسی سی
مجوز	پروانه عمومی همگانی گنو (کریتیو کامنز اختصاصی برای پایگاه داده)

منابع

1. متامث چیست؟ نرمن مگیل، صفحه خانگی متامث.
2. بیشترین برهان‌های اخیر بایگانی‌شده در ۳ فوریه ۲۰۲۰ توسط Wayback Machine، مگیل، نرمن.

پیوند به بیرون

• متامث: وبگاه رسمی.
• ریاضیدانان دربارهٔ متامث چه نظری دارند: نظراتی بر متامث.