{"entities":{"Q5894305":{"pageid":7932916,"ns":120,"title":"Item:Q5894305","lastrevid":97658423,"modified":"2026-06-05T15:10:45Z","type":"item","id":"Q5894305","labels":{"en":{"language":"en","value":"Preface to the special issue: Interactive theorem proving and the formalization of mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5961492"}},"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":"Q5894305$0785C289-27AF-4AC1-9A05-0E39B690D184","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"10153424e3878e88f748b9de39c13a22fb93b39a","datavalue":{"value":{"text":"Preface","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5894305$EAA2AFFE-B24E-4BC7-9B39-54DC4029E2F8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"127872043cf98cb56bd068101eb10bf9d3a83911","datavalue":{"value":"1276.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$D92499F9-04E4-49B7-81DB-39FC3E05CCE7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1b458247d70dac1a8c5142794c8220effc48e677","datavalue":{"value":"10.1017/S0960129511000235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$646E8EDB-BC81-4706-A8B1-E4EA1485BD02","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4f9facad47142ae6aca78e42226d987a134e9bf3","datavalue":{"value":{"entity-type":"item","numeric-id":789175,"id":"Q789175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$859F7256-8F10-4FF3-B008-CBA5D912E8A7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$13DD5241-EA97-4E87-913E-EB0C9501C88B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5412e51208588a3303ff1411a4274ccfb0b7d7d6","datavalue":{"value":{"time":"+2011-10-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5894305$60AC47F4-9B96-4353-B1D0-3E25A114772C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$00EE8706-EC7D-49DD-8183-C3E977940397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$1077AE43-1BA3-4068-8FAC-0F0820FB833C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$3C13E675-8B97-4C72-83A3-A82C3BD72076","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$B720CD3B-1009-4EEE-83CD-34568E99E40E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bea0b4a5e5ecffdadbc9bba9aa8e16ed5dc71d49","datavalue":{"value":"5961492","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5894305$987FD9FE-763F-489D-8843-329148136257","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":"Q5894305$A940BB5E-DA0E-4492-A5BA-117398FDA472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$B07F1AD5-D4E3-4292-8A2A-5381A020A3AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$B2E5F73B-993D-43BA-A716-8C21D8D57B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$12F0B36E-6CBF-45C0-A7F9-198C122138F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$53EEC8DE-2C7E-4FC3-A61E-278AB86B3C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$D8BB01BA-DCFC-48F3-90C1-94633FAD9F2A","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":"Q5894305$101EAAFB-B236-4A6C-AD64-4A6A42FA95DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$D9180FA1-8B84-4F39-AC7D-D746315A6923","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e916eb1dc395e3830d6317d3e8aefcb052d11440","datavalue":{"value":{"entity-type":"item","numeric-id":21785,"id":"Q21785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$422DB4C5-D72D-4690-9798-7ACB7A18AC22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$737A1E4C-3E12-4F39-AD80-186139D95F4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5894305$10E0AD2E-3CA7-434F-A99F-B97F0923462A","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":"Q5894305$BD5B96DB-02E2-49B1-94F9-5CCF573FAED3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c32f2cbb8a453222b98cdf0e974734e0b4ea4a11","datavalue":{"value":{"entity-type":"item","numeric-id":5094469,"id":"Q5094469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74c9b32ccd5b9977d68eb62945f861793b400e41","datavalue":{"value":{"amount":"+0.8635554313659668","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":"Q5894305$BC2CCFB8-BBB5-4C82-9BC9-A189B71A9619","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a2d401ee2c3a4bcc1deb76485d6fce7bc4a822f","datavalue":{"value":{"entity-type":"item","numeric-id":1961912,"id":"Q1961912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a38a13cfebbb76ad1cda67ae5a43cfe4bba737e","datavalue":{"value":{"amount":"+0.794797420501709","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":"Q5894305$6FDB4972-3D1D-42A2-A43B-E238F5FFFC2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc268baf51e6f99f0ec7fc0e4bd70830f2cc4651","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8194932ea40d53d85db3c867394676a075bdb679","datavalue":{"value":{"amount":"+0.7926008105278015","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":"Q5894305$3DF47776-0EA8-497F-9EB3-5D045696783A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ad36f3705405dbee6b572ca63239431d46e256f","datavalue":{"value":{"entity-type":"item","numeric-id":4263839,"id":"Q4263839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47b437f267b5ad7768ec0813a3055ace204565cb","datavalue":{"value":{"amount":"+0.7907387614250183","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":"Q5894305$7DE7A4E3-BCE4-4813-9CCC-049B96FBC53A","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":"f117e164ed3259ce0eb02bde3ca01f89b0273a3a","datavalue":{"value":{"amount":"+0.7809348702430725","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":"Q5894305$E4BA12CD-F3CF-466D-B2A9-C2180F9037E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Preface to the special issue: Interactive theorem proving and the formalization of mathematics","badges":[]}}}}}