Readable Formalization of Euler’s Partition Theorem in Mizar

DOI10.1007/978-3-319-20615-8_14zbMath1417.68214OpenAlexW2260911901MaRDI QIDQ3453116

Karol Pąk

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-20615-8_14

zbMATH Keywords

Euler's partition theoremlegibility of proofsoperations on languages

Mathematics Subject Classification ID

Related Items (1)

Accessing the Mizar Library with a Weakly Strict Mizar Parser

Uses Software

• Mizar
• MML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Flexary operations
• Topological manifolds
• Methods of lemma extraction in natural deduction proofs
• Tentative Experiments with Ellipsis in Mizar
• On Duplication in Mathematical Repositories
• Theorem Proving in Higher Order Logics
• Flexary Operators for Formalized Mathematics

This page was built for publication: Readable Formalization of Euler’s Partition Theorem in Mizar