http://hdl.handle.net/11320/8761 Thu, 12 Mar 2026 23:12:54 GMT 2026-03-12T23:12:54Z http://hdl.handle.net/11320/19740 Tytuł: Elementary Number Theory Problems. Part XIX Autorzy: Pąk, Karol Abstrakt: In this paper, we present formal solutions to twelve problems selected from Wacław Sierpiński’s book 250 Problems in Elementary Number Theory. The selected problems are: 108, 112–114, 118–119, 127, 129, 130, and 132–134 formalized in the Mizar system. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19740 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19737 Tytuł: Elementary Number Theory Problems. Part XVIII Autorzy: Grabowski, Adam Abstrakt: In this paper another seven problems from Wacław Sierpiński’s book “250 Problems in Elementary Number Theory” are formalized, using the Mizar formalism, namely: 53, 61, 81, 90, 100, 156, and 167. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19737 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19732 Tytuł: Elementary Number Theory Problems. Part XVII Autorzy: Korniłowicz, Artur; Naumowicz, Adam Abstrakt: This paper furthers the formalization of problems from Wacław Sierpiński book “250 Problems in Elementary Number Theory” in the Mizar system. The selected twelve items are 37, 101, 115, 117, 145, 157, 159, 161–163, 165, and 169. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19732 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19594 Tytuł: Conway’s Normal Form in the Mizar System Autorzy: Pąk, Karol Abstrakt: This paper presents a formal definition of the Conway normal form, a structured representation uniquely suited to characterising surreal numbers by expressing them as sums within a hierarchically ordered group. To this end, we formalise the first sections of the chapter The Structure of the General Surreal Number in Conway’s book. In particular, we define omega maps and prove the existence and uniqueness of the Conway name for surreal numbers. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19594 2025-01-01T00:00:00Z