Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Acewicz, Marcin; Pąk, Karol: Pell’s equation (2017)
- Ford, Ian: Semantic representation of general topology in the Wolfram language (2017)
- Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
- Zhan, Bohua: Formalization of the fundamental group in untyped set theory using auto2 (2017)
- Vlasov, D.Yu.: Smm, the simplified metamath (2012)
- Wiedijk, Freek: Pollack-inconsistency (2012)
- Wiedijk, Freek: A synthesis of the procedural and declarative styles of interactive theorem proving (2012)
- Vlasov, D.Yu.: The language of formal mathematics Russell (2011)
- Wiedijk, Freek (ed.): The seventeen provers of the world. Foreword by Dana S. Scott.. (2005)
- Belinfante, Johan Gijsbertus Frederik: Computer proofs about finite and regular sets: The unifying concept of subvariance. (2003)