{"entities":{"Q5875424":{"pageid":7904975,"ns":120,"title":"Item:Q5875424","lastrevid":39654627,"modified":"2024-12-30T16:43:26Z","type":"item","id":"Q5875424","labels":{"en":{"language":"en","value":"Nine Chapters of Analytic Number Theory in Isabelle/HOL."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649965"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$ED70428F-148B-445C-817B-7319BA30524B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc3155209aecfa73c406ca3d6ea19dfb5eb798dd","datavalue":{"value":{"entity-type":"item","numeric-id":1791157,"id":"Q1791157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$20C7A51E-8FAB-432D-B16A-B4E83EE0A80D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875424$4123F890-FDB5-4EB2-B856-54240AED5411","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875424$916E1E3B-41C4-4E22-B153-44040E218ADA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"98ddb7e313d140096795791c3568b8daeb6c3921","datavalue":{"value":"7649965","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875424$A5D991F1-9543-4621-870E-C4DD56A1381A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$0D4883FE-5387-41BB-9615-D6ECCBEB9B75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$D0068617-9D85-40EC-A297-43231430DE00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4983ee388360aa6d77a5bb4cd218f7e3573a9363","datavalue":{"value":"analytic number theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$96531893-9DC0-425A-B138-AF823561138B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf9020b9cf738e3dc19adb35ae396c6478d2142c","datavalue":{"value":"number theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$6361A485-9BF5-41A7-8AB2-BD00540C3585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c90052b79d472afc6bfc44d1250cd9c59bb553ea","datavalue":{"value":"arithmetical function","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$F69F3D90-1E66-4F13-B093-1DC71FA8AFA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e702beeab19844cbc60c3d9b962beebdf4e9ea5c","datavalue":{"value":"Dirichlet series","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$E0B00520-C953-447C-9357-BA769921DAA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"952f21178d1a225b51df1682ef92b4d9e390d96b","datavalue":{"value":"prime number theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$28F278E6-E58C-4E3C-8804-4B6D83FE0747","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f41bbdeeaaf4eb7df48d73e5af15a656f5bb0a6e","datavalue":{"value":"Dirichlet's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875424$1C494FCD-4DC9-4BA6-9258-1A83AD6F378B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$C0BEB3AC-2C23-40A5-87A2-7B7FF7732804","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$CE87FFC2-6E9C-4FD0-8455-64D323871337","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$C7EEFE66-64F5-45DE-996E-411F138B3711","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3f446977c174b9f0a9fb7d0514dfac4131ec3df8","datavalue":{"value":"https://doi.org/10.4230/LIPIcs.ITP.2019.16","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875424$53651F59-9FCD-42E3-894D-EFB334699EAE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8b202c7e1092d696f5b1bd21713f846c4e4e8087","datavalue":{"value":"W2978388704","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875424$A9C30C60-EF49-4AAD-B825-72F7A8B2ABEC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"db96022487e3570cb71f73c53e0631e122df0137","datavalue":{"value":{"text":"Nine Chapters of Analytic Number Theory in Isabelle/HOL.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875424$74659B8C-5FE5-4474-9958-BCDCC9D0B686","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"811e08ac2fdbd0c8d873aede325f67deffb79bca","datavalue":{"value":{"entity-type":"item","numeric-id":5195290,"id":"Q5195290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$4CC636DD-04E9-46FC-8529-B3D435827497","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2f3c84fedec6be5b8f59fef93a6a8632cda3e40","datavalue":{"value":{"entity-type":"item","numeric-id":4101884,"id":"Q4101884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$34520F33-3939-4319-9188-1DC797FCEB33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bc69bc93671b863b16ef6b7eb0a66cb2b8ee6e5","datavalue":{"value":{"entity-type":"item","numeric-id":3995823,"id":"Q3995823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$87F9690A-5BE4-4A00-9087-79F87FD404D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"baa06e98dd2bbc2e50d854d66656326eb2c6a08d","datavalue":{"value":{"entity-type":"item","numeric-id":5195248,"id":"Q5195248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$9676B538-9E00-4B8C-A9FD-E5558C263599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bfb9cfedcdf8209e09850a44ba23684e87646d65","datavalue":{"value":{"entity-type":"item","numeric-id":5277791,"id":"Q5277791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$4B29CA97-0D57-41B4-8B6B-A6B8CACC53C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c83025fc071e2bc20ca08193c00bd567a4b0ddac","datavalue":{"value":{"entity-type":"item","numeric-id":4044652,"id":"Q4044652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$BDEBCAAE-64A1-4AFD-A628-48F81564BD8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$8CC0F9BD-7899-4CE2-A77B-AC2DC857BA12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5630f518c570c62f3ed6099d539c193f62b9f4ef","datavalue":{"value":{"entity-type":"item","numeric-id":5120486,"id":"Q5120486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$6666F602-B734-4F7F-917B-0E8CD5B18B1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92cb4fd1e15339e6018a4d15ba7f11815833f511","datavalue":{"value":{"entity-type":"item","numeric-id":3075240,"id":"Q3075240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$FF0293D7-5410-4729-99B0-CF977541FBF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34f831bdd0445bbb207a58535cee0f990813469d","datavalue":{"value":{"entity-type":"item","numeric-id":2655322,"id":"Q2655322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$58C469C0-AAB8-4114-B434-65B2BF387E33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d360f4c10b4163627f57faa3db163275ea6a011","datavalue":{"value":{"entity-type":"item","numeric-id":5327350,"id":"Q5327350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$8893A83D-C1F4-4450-B3B5-665C445AD05B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9ee6ea22e97285c93f23994425666db287dd0fe","datavalue":{"value":{"entity-type":"item","numeric-id":2303242,"id":"Q2303242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$1BDFD3E0-904B-437E-A17E-6D4AF23A7EC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f864e2d77601e8c917be8073394aaaec47357f3e","datavalue":{"value":{"entity-type":"item","numeric-id":5933539,"id":"Q5933539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$DF0872D4-0CB0-4096-A6FE-97B360307A45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"043d123eea368f4ca41b305129130ac14e8a96a7","datavalue":{"value":{"entity-type":"item","numeric-id":4377812,"id":"Q4377812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$C56AD639-4218-4BAD-AB0B-A198C6B35186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3855af33f4c82abb191ed201f76779d081a2c15c","datavalue":{"value":{"entity-type":"item","numeric-id":3559771,"id":"Q3559771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875424$5D44C2EF-62E9-4563-9079-4311B9FD378A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"88d326a0fe24604949bd38fb9e80916c85284d96","datavalue":{"value":"10.4230/LIPICS.ITP.2019.16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875424$B2733B3E-5742-4B6A-85CB-74619ADCE5BD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875424","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875424"}}}}}