{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T02:39:34Z","timestamp":1768012774516,"version":"3.49.0"},"reference-count":14,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>In this paper another twelve problems from W. Sierpi\u0144ski\u2019s book \u201c250 Problems in Elementary Number Theory\u201d are formalized, using the Mizar formalism, namely: 42, 43, 51, 51a, 57, 59, 72, 135, 136, and 153\u2013155. Significant amount of the work is devoted to arithmetic progressions.<\/jats:p>","DOI":"10.2478\/forma-2023-0022","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T10:21:34Z","timestamp":1704450094000},"page":"277-286","source":"Crossref","is-referenced-by-count":4,"title":["Elementary Number Theory Problems. Part XII \u2013 Primes in Arithmetic Progression"],"prefix":"10.2478","volume":"31","author":[{"given":"Adam","family":"Grabowski","sequence":"first","affiliation":[]}],"member":"374","published-online":{"date-parts":[[2023,12,31]]},"reference":[{"key":"2025082007064016326_j_forma-2023-0022_ref_001","unstructured":"Leonard Eugene Dickson. History of Theory of Numbers. New York, 1952."},{"key":"2025082007064016326_j_forma-2023-0022_ref_002","doi-asserted-by":"crossref","unstructured":"Adam Grabowski. Elementary number theory problems. Part VI. Formalized Mathematics, 30(3):235\u2013244, 2022. doi:10.2478\/forma-2022-0019.","DOI":"10.2478\/forma-2022-0019"},{"key":"2025082007064016326_j_forma-2023-0022_ref_003","doi-asserted-by":"crossref","unstructured":"Adam Grabowski. Polygonal numbers. Formalized Mathematics, 21(2):103\u2013113, 2013. doi:10.2478\/forma-2013-0012.","DOI":"10.2478\/forma-2013-0012"},{"key":"2025082007064016326_j_forma-2023-0022_ref_004","unstructured":"Adam Grabowski and Christoph Schwarzweller. Translating mathematical vernacular into knowledge repositories. In Michael Kohlhase, editor, Mathematical Knowledge Management, volume 3863 of Lecture Notes in Computer Science, pages 49\u201364. Springer, 2006. doi:10.1007\/11618027 4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15\u201317, 2005, Revised Selected Papers."},{"key":"2025082007064016326_j_forma-2023-0022_ref_005","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153\u2013245, 2010."},{"key":"2025082007064016326_j_forma-2023-0022_ref_006","doi-asserted-by":"crossref","unstructured":"Artur Korni\u0142owicz. Flexary connectives in Mizar. Computer Languages, Systems & Structures, 44:238\u2013250, December 2015. doi:10.1016\/j.cl.2015.07.002.","DOI":"10.1016\/j.cl.2015.07.002"},{"key":"2025082007064016326_j_forma-2023-0022_ref_007","doi-asserted-by":"crossref","unstructured":"Artur Korni\u0142owicz and Adam Naumowicz. Elementary number theory problems. Part V. Formalized Mathematics, 30(3):229\u2013234, 2022. doi:10.2478\/forma-2022-0018.","DOI":"10.2478\/forma-2022-0018"},{"key":"2025082007064016326_j_forma-2023-0022_ref_008","doi-asserted-by":"crossref","unstructured":"Adam Naumowicz. Dataset description: Formalization of elementary number theory in Mizar. In Christoph Benzm\u00fcller and Bruce R. Miller, editors, Intelligent Computer Mathematics \u2013 13th International Conference, CICM 2020, Bertinoro, Italy, July 26\u201331, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 303\u2013308. Springer, 2020. doi:10.1007\/978-3-030-53518-6 22.","DOI":"10.1007\/978-3-030-53518-6_22"},{"key":"2025082007064016326_j_forma-2023-0022_ref_009","doi-asserted-by":"crossref","unstructured":"Adam Naumowicz. Extending numeric automation for number theory formalizations in Mizar. In Catherine Dubois and Manfred Kerber, editors, Intelligent Computer Mathematics \u2013 16th International Conference, CICM 2023, Cambridge, UK, September 5\u20138, 2023, Proceedings, volume 14101 of Lecture Notes in Computer Science, pages 309\u2013314. Springer, 2023. doi:10.1007\/978-3-031-42753-4 23.","DOI":"10.1007\/978-3-031-42753-4_23"},{"key":"2025082007064016326_j_forma-2023-0022_ref_010","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Proth numbers. Formalized Mathematics, 22(2):111\u2013118, 2014. doi:10.2478\/forma-2014-0013.","DOI":"10.2478\/forma-2014-0013"},{"key":"2025082007064016326_j_forma-2023-0022_ref_011","unstructured":"Wac\u0142aw Sierpi\u0144ski. Elementary Theory of Numbers. PWN, Warsaw, 1964."},{"key":"2025082007064016326_j_forma-2023-0022_ref_012","unstructured":"Wac\u0142aw Sierpi\u0144ski. 250 Problems in Elementary Number Theory. Elsevier, 1970."},{"key":"2025082007064016326_j_forma-2023-0022_ref_013","doi-asserted-by":"crossref","unstructured":"Nguyen Xuan Tho. On a remark of Sierpi\u0144ski. Rocky Mountain Journal of Mathematics, 52(2):717\u2013726, 2022. doi:10.1216\/rmj.2022.52.717.","DOI":"10.1216\/rmj.2022.52.717"},{"key":"2025082007064016326_j_forma-2023-0022_ref_014","doi-asserted-by":"crossref","unstructured":"Rafa\u0142 Ziobro. Fermat\u2019s Little Theorem via divisibility of Newton\u2019s binomial. Formalized Mathematics, 23(3):215\u2013229, 2015. doi:10.1515\/forma-2015-0018.","DOI":"10.1515\/forma-2015-0018"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2023-0022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,20]],"date-time":"2025-08-20T07:07:57Z","timestamp":1755673677000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2023-0022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":14,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,12,31]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0022"],"URL":"https:\/\/doi.org\/10.2478\/forma-2023-0022","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}