{"entities":{"Q448975":{"pageid":450742,"ns":120,"title":"Item:Q448975","lastrevid":51550757,"modified":"2026-01-18T18:07:28Z","type":"item","id":"Q448975","labels":{"en":{"language":"en","value":"A case study in formalizing projective geometry in Coq: Desargues theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6080927"}},"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":"Q448975$7BF9ABA5-023A-4E58-BDC9-F7D07C717F32","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ecad4b26b822896cb9a2f5f56d881ad6a2a0516e","datavalue":{"value":{"text":"A case study in formalizing projective geometry in Coq: Desargues theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q448975$438772CC-F0DB-435B-BF73-FC65EEE46791","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7f13669eec7aa7936846143a034af1bd1a250885","datavalue":{"value":"1248.68449","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$A294C5C4-B7B4-4B72-8D15-24E9FCBB7C39","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"77d146ed87b25a3f218b4b3975707f6be569c62c","datavalue":{"value":{"entity-type":"item","numeric-id":448974,"id":"Q448974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$A10D6446-63AA-4F92-B508-9137B01EFA28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7154e8ca53ace223b8c5be019b7f4f775aab0292","datavalue":{"value":{"entity-type":"item","numeric-id":294376,"id":"Q294376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$942FC7C5-282C-4A74-AD29-ADDC82100C00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4f67aad00a911cdfd4a5f73b3962a1f5be1f7e5","datavalue":{"value":{"entity-type":"item","numeric-id":294371,"id":"Q294371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$26F59CFA-6E2B-407E-99F1-10AB880E524C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"285beb29e5e30a7ba8792191178d7f52682884ef","datavalue":{"value":{"entity-type":"item","numeric-id":175378,"id":"Q175378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$E42A90EE-4FE8-4D8E-B0EE-255FD06094C7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5eb7c028e513adb70517d5dc7c8a025b4004820b","datavalue":{"value":{"time":"+2012-09-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q448975$7E78935C-A267-4D34-B2C4-03E02A81C0E2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$9BB2B7E8-2DD7-41B8-8233-FD587AFD9299","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"08240126a81e33f43f6f0d84216dc8557b00da58","datavalue":{"value":"51A30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$08DF9BB7-6C29-47C8-AAC3-929F2716D841","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"41caf1d31fd97d693c3cadf81601a3b501f96ff0","datavalue":{"value":"6080927","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$0A7DF209-AA5A-4055-AED3-96364942628D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c529886f574ea1f57bdfe9e9ecded94714c4dfa","datavalue":{"value":"Desargues","type":"string"},"datatype":"string"},"type":"statement","id":"Q448975$61BE1627-1FA4-48C2-8ED7-557C8F1A3C3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e85686c88b6675116cec177bbafff890f9021164","datavalue":{"value":"rank","type":"string"},"datatype":"string"},"type":"statement","id":"Q448975$CE06A7EC-8552-489F-9E6E-CF379875362A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"619cec4664a98d8c81850d161b273c3520446471","datavalue":{"value":"projective geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q448975$3AEEFC6D-3086-49FD-83B7-A9035AB803B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q448975$11026C20-B56B-4C82-8FC8-D1F1A224D7EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a459f207ac4678061ae63e081ebfaf6a0762c49b","datavalue":{"value":"Hexamys","type":"string"},"datatype":"string"},"type":"statement","id":"Q448975$CC764746-4B43-474F-8186-C6B647BE1243","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":"Q448975$666C8D04-A0E1-49EA-9F45-E15670ECD899","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":"Q448975$D22E59AB-805C-4732-AB5A-394874BF7525","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d9345d0a6bb36ca28f4606a456bd32a410ef0876","datavalue":{"value":"https://doi.org/10.1016/j.comgeo.2010.06.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q448975$96E45DDC-8246-4CA1-9C33-0D029AD1B295","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f9844a06f6635f564dde1d33b9adf26c1bd28d6d","datavalue":{"value":"W2054653818","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$D6221A79-30AE-48FE-991D-E2867A7FA690","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$343F370E-CD3C-49BA-AC02-A1AB24A7A9AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5791688c0d08cb0956d2f1e861eee0a36c47d237","datavalue":{"value":{"entity-type":"item","numeric-id":2471743,"id":"Q2471743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$2D63742E-45ED-4217-99CE-6A87F0BEEB08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56561891c6904c5a2dfd08a9117937b91fb7bf32","datavalue":{"value":{"entity-type":"item","numeric-id":4763522,"id":"Q4763522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$6ECF77AF-C224-4AA2-9401-24B09D1321AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35fe0ff4126b55269ba5f7d4c75ba79f8b86b712","datavalue":{"value":{"entity-type":"item","numeric-id":1888445,"id":"Q1888445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$A29037AC-99D6-42D4-A8E0-7513CB194145","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2c6fc65716ca53b4df443be754d1a7c89f6f684","datavalue":{"value":{"entity-type":"item","numeric-id":4857780,"id":"Q4857780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$576CA499-2867-4792-A799-82EE3DD9BA8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"304bbbea7e709f84aad610e1815b85b69d728ea5","datavalue":{"value":{"entity-type":"item","numeric-id":3766390,"id":"Q3766390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$FF2FF27A-5450-48AC-853C-494F0C48DE5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13bac5997d9caf8368bd9ff9b5cd7ba88aa6b14b","datavalue":{"value":{"entity-type":"item","numeric-id":4531863,"id":"Q4531863"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$876D4D0D-58A9-498A-84AE-68D68C116568","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98589d6fa667da17f782a55cd2dc8c33d4dbf671","datavalue":{"value":{"entity-type":"item","numeric-id":5308710,"id":"Q5308710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$9A24C47B-DC21-458A-AEBC-97CB6C930FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50194ca3b7c353b09bf7a69176aa9a9155660faf","datavalue":{"value":{"entity-type":"item","numeric-id":3003228,"id":"Q3003228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$52E182FE-6DF6-4FCC-A163-A6CEF66C1AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f3e2ce8ad7eb4c407ea1e2b45c8988243819268","datavalue":{"value":{"entity-type":"item","numeric-id":3422212,"id":"Q3422212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$9D83FB11-D76F-4204-ACFD-98EB3CB75DA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5296a1d08321e3fc28ff882325d64dbe74172a0a","datavalue":{"value":{"entity-type":"item","numeric-id":3003232,"id":"Q3003232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$3356F917-A9D5-4B5E-AD2A-023B4C0E2F44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36d7991ac9e7cdf85ee75bde2eeaeec3be8a2a07","datavalue":{"value":{"entity-type":"item","numeric-id":3559773,"id":"Q3559773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$C406A029-D402-41A1-BC7B-8E8969B244EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fc41f2b2a8aa0d1d1987dc920f043ef4c6d51ab","datavalue":{"value":{"entity-type":"item","numeric-id":3422215,"id":"Q3422215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$1BEBDCE8-60A0-4059-A18B-77FC53A8F5D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"540adcc9e46ea420a940154aee39f09e6ab0a966","datavalue":{"value":{"entity-type":"item","numeric-id":5464649,"id":"Q5464649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$5BE55880-4B60-480F-B70F-9E36071D462D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc182df8b38eb530d99faf472b90c793492a26d2","datavalue":{"value":{"entity-type":"item","numeric-id":5453489,"id":"Q5453489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q448975$0F9C0751-AA5F-441E-ACCD-AF71C0D7F897","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"18aff9307657e043b1c4aa2a14f9a2f452a13150","datavalue":{"value":"10.1016/J.COMGEO.2010.06.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q448975$45118C2B-CBA8-490A-8646-4AA5DCCC12BF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d54bed5461dfeb3ada4aeb652d634bd759c55c96","datavalue":{"value":{"entity-type":"item","numeric-id":3003232,"id":"Q3003232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59944297738486900667ba9aa92efa5aef29dd77","datavalue":{"value":{"amount":"+0.890132486820221","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":"Q448975$19E6B196-FE07-411A-B340-CA22DBD21E25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1bf28bfe52028ed618bbaa8952574102140b299","datavalue":{"value":{"entity-type":"item","numeric-id":2631964,"id":"Q2631964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"68fa3d1073eb905e56df5ac73d448d3ca804b14f","datavalue":{"value":{"amount":"+0.8467321991920471","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":"Q448975$3007D983-0478-4D26-8B55-32E648642E4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"adbf9b5719c13218db616f95f2a4a5f325af358f","datavalue":{"value":{"entity-type":"item","numeric-id":6108812,"id":"Q6108812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78831e615e035fde5b990f517f518b4ef2d7909a","datavalue":{"value":{"amount":"+0.8286571502685547","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":"Q448975$B1E38D09-ADE8-481F-A3AF-001CC4F66F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ef53f70cbd81d284a07ee397ebb0af124af9fd5","datavalue":{"value":{"entity-type":"item","numeric-id":3102734,"id":"Q3102734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22ea6646cd3c73747e0411babdbf1e2bd080c238","datavalue":{"value":{"amount":"+0.8073019981384277","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":"Q448975$E2E06218-190F-4E47-B51D-08359BFE2CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4d26e55b2d0676f92a5f1135769d3cdb3b111fb","datavalue":{"value":{"entity-type":"item","numeric-id":2471743,"id":"Q2471743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0db2f5107875128a6ef6235ec733aef70a1b131","datavalue":{"value":{"amount":"+0.8070576190948486","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":"Q448975$F45457BE-AB19-48EF-8518-7E204DC20936","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:448975","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:448975"}}}}}