{"entities":{"Q2988059":{"pageid":2998783,"ns":120,"title":"Item:Q2988059","lastrevid":79669508,"modified":"2026-05-06T14:26:56Z","type":"item","id":"Q2988059","labels":{"en":{"language":"en","value":"Machine-checked mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6720705"}},"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":"Q2988059$A07C03C2-41B3-4628-9A90-7FADB05962B4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5f2db0fc2aaf7ca74a0d2840004bb64a74141bd3","datavalue":{"value":"1375.68101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$DFBE0DE5-729E-42AF-92EC-A517C5345618","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"379ac4e8dcb87cc7060e4dba787e250b7104d056","datavalue":{"value":{"entity-type":"item","numeric-id":512133,"id":"Q512133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2988059$ABF6F456-5D75-4227-A4AF-3616621259FF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"46a30028c10f94c4944c801c86f2de5dd37da0f3","datavalue":{"value":{"time":"+2017-05-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2988059$5A53979E-61B4-4BFA-907A-2379E99E3887","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$C3D9DCE0-FEC1-4B6F-AF93-DE741342E18A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"855dfff3c52593115343606bc2418a3b17e5a003","datavalue":{"value":"01A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$A94176A4-5F9C-4A51-8230-6DD6465F0B47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$C2AE7ECF-6ABB-4403-BC76-D04A7F56318A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$FF333883-C714-486B-A252-8D835A318826","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"32f844b29ec95675af73e92c46e1946b431d1874","datavalue":{"value":"6720705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2988059$68AE3A41-F1AF-4C44-BAFA-0FE00A32E7A9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2988059$67F9590C-91E3-44D0-8C4B-FD0EE0FE65D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55caf05c57404ab910cf1d6d785d791abcc73ea3","datavalue":{"value":"formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2988059$4982C583-6D49-43CD-A133-FDA64BC66A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2988059$CA0FA19D-E94B-401F-89EE-51487E9BEF0E","rank":"normal"}],"P1463":[{"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":"Q2988059$39C68939-83E0-4488-98A4-81366EDCDDDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2988059$5F8889B5-EDF9-4316-8B9B-AE9228998A93","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":"Q2988059$ACF051AE-DF66-4FA6-BFA9-629CB4CFD2F4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0294760f1d9e02f3b58308b62577466725c8d719","datavalue":{"value":{"entity-type":"item","numeric-id":1040001,"id":"Q1040001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51150d4fbf274ea6cf97b0befacf56029774a37b","datavalue":{"value":{"amount":"+0.7866520881652832","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":"Q2988059$B1339BB0-F383-49B7-980B-D6FCD4C7A313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3402ca78550be85cdc6de3757cefccaa74df2e2f","datavalue":{"value":{"entity-type":"item","numeric-id":4664201,"id":"Q4664201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"205ad8403b39c8e315d2ca7cb186c345b770a9d0","datavalue":{"value":{"amount":"+0.7662050724029541","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":"Q2988059$F360DA29-23F0-4EC6-970F-7872C70A1416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"698e157db28629ef10c9bedc71d22dda03a2adfb","datavalue":{"value":{"entity-type":"item","numeric-id":3602565,"id":"Q3602565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e80497ba70606e0bfa05c78db8c0c643a49af1e","datavalue":{"value":{"amount":"+0.7625735998153687","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":"Q2988059$3BACAB5D-F966-4316-9EFE-E0BB53361040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5caf9de33d1799cb19ca4a87514a35fe4bcf1918","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65893a72e27d9010f729c8420875d0abb03625fd","datavalue":{"value":{"amount":"+0.7576843500137329","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":"Q2988059$8E2E9073-9201-4D0F-AB62-D1D7DDF5B08F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8723d99d255de6ea7ab820a8d5f35e9ef29f213a","datavalue":{"value":{"entity-type":"item","numeric-id":6095201,"id":"Q6095201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5788ce0a31dcf1a6cd8aef13a2c8e0392175761f","datavalue":{"value":{"amount":"+0.7563523054122925","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":"Q2988059$8AE97451-0DCC-4564-830A-F45486F749C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Machine-checked mathematics","badges":[]}}}}}