{"entities":{"Q2219408":{"pageid":2230151,"ns":120,"title":"Item:Q2219408","lastrevid":57782268,"modified":"2026-04-02T12:29:06Z","type":"item","id":"Q2219408","labels":{"en":{"language":"en","value":"Maintaining a library of formal mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7298568"}},"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":"Q2219408$F3BE1305-3E23-43F3-B720-49CA4D393AE1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"44e84b1a968620074f935b65e0b4c86a0671737c","datavalue":{"value":{"text":"Maintaining a library of formal mathematics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2219408$5E6251D3-0C74-4B87-988C-FEAA877E4EF1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5f886c4a7df423fd631b5ce8dad3ebc0b332bfc7","datavalue":{"value":"1455.68262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$2A9C6A5A-72EE-4359-BD8B-08CCFBE0DE2C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7e7e824a9454e5bdd0ade3e56b5bf64dafb65440","datavalue":{"value":"10.1007/978-3-030-53518-6_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$4F5DF04E-67DD-4A4A-89F0-B776CB5A0C41","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dc9f7061148c184d156fce1cd302b98949f36de","datavalue":{"value":{"entity-type":"item","numeric-id":1687767,"id":"Q1687767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$D9EB9004-B2DD-4C28-A88C-AC57345E1D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aefce4072ff7b8c016ef35d01c9736e705e82ce2","datavalue":{"value":{"entity-type":"item","numeric-id":1622973,"id":"Q1622973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$21E3BDC4-DC71-4016-9AE2-088BCC9788F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"70ade185f3ecac8f26bbd0db5ba024cb38b4e341","datavalue":{"value":{"entity-type":"item","numeric-id":287377,"id":"Q287377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$F5D85E75-0236-4D5D-9BB8-14295C646B33","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233394734482eba32ed4ee15da745b1ac2b96149","datavalue":{"value":{"time":"+2021-01-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2219408$ED7D3147-07BC-48AC-8CD6-3DFB7B8B5D8F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"29a23641678508c536101617fb93c445ca522965","datavalue":{"value":"https://arxiv.org/abs/2004.03673","type":"string"},"datatype":"url"},"type":"statement","id":"Q2219408$81036D4F-B693-46AB-9AC4-F9FA3268731B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$EF9411F6-78C0-427C-A52A-6C584F12A4EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4c276f6bcfe480cdd0a7a976933d6fd851c1b746","datavalue":{"value":"68V30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$BAFB6B68-9E4D-4671-B49B-8EB2792F587B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b7ad058e70cecbe9bfc68992acb5cf3afaa34317","datavalue":{"value":"7298568","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$EDD1BFC5-53C2-4AF5-A19C-897665C45457","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ece59c48c6b56403e847bffda58343af27541073","datavalue":{"value":"mathlib","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219408$7A8C0E72-BBE4-4A6D-8D2D-EA77073D7076","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d450695369b616b42c44603b7a350d2f04fc108","datavalue":{"value":"formal mathematics library","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219408$D3AF707A-2746-4557-8757-7E1D1B2E315F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b4946ec552e7330fed3653f72092c7dc47bd89f","datavalue":{"value":"library development","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219408$CAAA5814-741E-48D4-BA4A-1F48FE844D12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"311b603be778d5dd21132345c4dd96e9f74dfbaa","datavalue":{"value":"linting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219408$3DFFA40B-2CF6-4573-AF83-444C17767DB0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$5E8C33ED-6B2E-4948-9CB0-563BF5EE6C4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$711CBC76-DCBE-4088-94E3-8AD8C89AC49A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$CF6457B6-A2C3-47BC-A605-6D85FC761032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3566ceaa607ff2880dbbe400f3e2dbce0394438a","datavalue":{"value":{"entity-type":"item","numeric-id":18773,"id":"Q18773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$747FFB44-7783-45FA-B27F-0111B29C4E97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cfc4b80b3c48044062741dc3f6116ad79929c84e","datavalue":{"value":{"entity-type":"item","numeric-id":40235,"id":"Q40235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$B4F1BD7A-3610-465C-9A01-8E719B5A824E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"352070f92a42ab6c0ae16e5d77d8a717bc392ccc","datavalue":{"value":{"entity-type":"item","numeric-id":19847,"id":"Q19847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$29D282FF-05BC-4004-8BC6-90ED0B15D6FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219408$156DC843-D46E-4675-AECD-07DAE71509B3","rank":"normal"},{"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":"Q2219408$E4315483-2825-42A3-8AF6-7D02258963D0","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":"Q2219408$A9865724-6604-4D4C-9572-F0D492F52079","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c346257dee4815eb8e21b43d20cd7efe09faadda","datavalue":{"value":"W3100204936","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219408$B2B7152E-CB6A-4DED-907C-70A67F0B204A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5225a69bdcfcfe29a5db8c4b18a78ef5cb47fe6","datavalue":{"value":{"entity-type":"item","numeric-id":4413892,"id":"Q4413892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e834983cc481ac9506749ccb0a348e9f62f2e012","datavalue":{"value":{"amount":"+0.7506762146949768","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219408$CEB4CF2D-E74F-427F-A847-F45CE74A8F3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4374daf952f95be8e2d6a4ef5e2444e3d0d7712","datavalue":{"value":{"entity-type":"item","numeric-id":1663215,"id":"Q1663215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82871d004166849aef0212f2af68756ebe8f3269","datavalue":{"value":{"amount":"+0.7497628927230835","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219408$A01823BB-81D6-4682-B5F4-A4CC0DE01E6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4f05aee4b3664e67f1ee18f25367507e60b89a0","datavalue":{"value":{"entity-type":"item","numeric-id":5313080,"id":"Q5313080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8096aff4367d154d2d691277a963fc1e18af789","datavalue":{"value":{"amount":"+0.7390912175178528","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219408$25D38B49-A931-4690-B665-305DC9636A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f9b44095d13cd2bcad82afdc067f0870b5d91e6","datavalue":{"value":{"entity-type":"item","numeric-id":5740657,"id":"Q5740657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"309dea1cf6b11902b0fc764f6c8f35df13af2072","datavalue":{"value":{"amount":"+0.7325211763381958","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219408$FA48853B-471B-49C3-915C-96A1F10B1B5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e11b650df2e6b564bded20ddda37e11cb0358967","datavalue":{"value":{"entity-type":"item","numeric-id":5313072,"id":"Q5313072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6dac9d543f55c4c563339dfdb9ec665acab23ebf","datavalue":{"value":{"amount":"+0.7302811741828918","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219408$CE6517BE-ADAF-4E53-92BD-8241A5E8ACFA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2219408","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2219408"}}}}}