{"entities":{"Q2323449":{"pageid":2334192,"ns":120,"title":"Item:Q2323449","lastrevid":53518502,"modified":"2026-01-25T03:28:02Z","type":"item","id":"Q2323449","labels":{"en":{"language":"en","value":"Formally verifying the solution to the Boolean Pythagorean triples problem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7100460"}},"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":"Q2323449$B3B0C656-0BCB-4AE0-9B83-6C71DB087494","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ea016276a7229fc5bd9b90acf41f9021f5972329","datavalue":{"value":{"text":"Formally verifying the solution to the Boolean Pythagorean triples problem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2323449$38A8296F-83A2-4E53-978E-29790C23FF4F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b5f48cd25208ba4e5ebb582aeff29af7c2a57379","datavalue":{"value":"1468.68318","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$5385DCF6-6323-40BD-94D8-077144227873","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"019239a5b99c9161ce4389de57414c8f40f605b4","datavalue":{"value":{"entity-type":"item","numeric-id":340573,"id":"Q340573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$4EB76C4F-157A-4D23-9ECF-828E3DED4AE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0ee03ce229dce1ad90ba116368ba88145bf746ab","datavalue":{"value":{"entity-type":"item","numeric-id":340574,"id":"Q340574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$AFD6D357-FC42-48CF-AE90-CF6F25F2B462","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"41df06f4fe4133fafd7ede4eda94dd022be9bb8e","datavalue":{"value":{"entity-type":"item","numeric-id":1430295,"id":"Q1430295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$183D43D3-9EAE-4735-8F31-27AEAD4FD4B0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$2389EA56-3DBA-468D-AFAE-AAEA642478E4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2bb2730e245e69026d7d337b11c937cb60d6f2b0","datavalue":{"value":{"time":"+2019-09-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2323449$7EC4BFC5-D6CF-4138-8ACE-99545FE4933A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$EA9132E1-07D4-4EB0-A83F-9A1317E2ED60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b4b251e34f965e85a4a30c5d646e0bae1192967","datavalue":{"value":"05D10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$A7A17905-8686-4412-8647-338C7AE663F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$E3B233B1-6387-4514-915F-1BBBE0F69964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$0821A1C3-E73E-4370-BA11-E39E59FF1807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$E8E01E61-CBE9-423A-B9AE-1273CB6B57D9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8a71439f25df29ba80eb11fe42a109dab6379082","datavalue":{"value":"7100460","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$13691AB9-25F0-4EC8-8DC7-B68BD34E56AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2323449$78AF2071-642C-44BE-85C8-B7D074B2AD86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a6e5bf2570672d6081dda12f743144f94ef06c5","datavalue":{"value":"large-scale proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2323449$F6524526-4961-4A4A-B8EC-FAB401DAB6CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2323449$0839CEDA-EED0-4450-8AAD-14D3497AB6E0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"2361c16ee0a0e59aab80891f2da2639f4768e382","datavalue":{"value":"Q114226107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$C182EB73-B39A-4248-83D9-809EB66F7240","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":"Q2323449$B5E08A00-127C-4D92-B79E-3D747D81E737","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":"Q2323449$A499F799-0296-48B8-904F-5DD65515B253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6afb9e05f24776a03d7fcd415baf7b99112468c9","datavalue":{"value":{"entity-type":"item","numeric-id":34519,"id":"Q34519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$0DB182C0-464D-41C5-B0E0-D66FF78DD8D9","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":"Q2323449$86E505F7-3704-4149-AE6B-C524DF3F0840","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ab8132f8be4966eaa49aed3347b9efa1ff28206b","datavalue":{"value":"https://doi.org/10.1007/s10817-018-9490-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q2323449$1A386774-52A1-4129-A325-7F2C11213E62","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4e3eee32deebad067b8a0dd922a3b33a213f5cfb","datavalue":{"value":"W2898484043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$21E7DDB9-45BA-4D87-A386-03110143237B","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":"Q2323449$1D2C388C-6539-4D66-A215-A91DB31D5EED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22c708f9a64c92fd4de4427f3b37941fff68141d","datavalue":{"value":{"entity-type":"item","numeric-id":3094178,"id":"Q3094178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$44D8A0C1-9777-4C31-A3E0-789679D54C98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7948d2ae997be513a92df2486b836c4e1eaa12","datavalue":{"value":{"entity-type":"item","numeric-id":5667480,"id":"Q5667480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$EDB2A606-7394-42F0-94CE-C16F47AAA422","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$2D64502F-0555-47FE-9992-1AB36C055CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$CF267AE0-1FF9-42CB-AC37-EDB875342D77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"396f6e5a94e4529ded42ebcec00efd56ba5fcab0","datavalue":{"value":{"entity-type":"item","numeric-id":1694569,"id":"Q1694569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$0618B1A5-BAD9-4A63-B679-5EF7F4A55494","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34ebe1bc84eda0376295f6ea90448cdc06c0b0db","datavalue":{"value":{"entity-type":"item","numeric-id":4645756,"id":"Q4645756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$34CE02A4-95D7-40AB-8952-95A0FA50B292","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab83b1b19d0d1f2edb00c19581e9d2bc2bed683d","datavalue":{"value":{"entity-type":"item","numeric-id":5464663,"id":"Q5464663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$9CA62DCA-10F0-4D2B-8B41-1FADD2BD31F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$0D483E82-ABC7-4E39-B23F-F1B471887E20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7c0d90ace913bd2dea9660b876d2d3d064b10bb","datavalue":{"value":{"entity-type":"item","numeric-id":2364109,"id":"Q2364109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$57A33E6C-E3CD-4EBE-AD2D-205D53FEB2BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"841607f8962f1bb2ff862f4fb0ee44966183bba9","datavalue":{"value":{"entity-type":"item","numeric-id":4586077,"id":"Q4586077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$81246879-E75D-4D8C-A3F3-DF9BD026EB80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7012bf2c8e1ba10cf9896acdd463864da284937a","datavalue":{"value":{"entity-type":"item","numeric-id":2818017,"id":"Q2818017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$4BDD0B87-33B1-40A0-8E32-DB84AFFBEC80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bcb0e71d083cf8486de0b4db45626afe5608e21","datavalue":{"value":{"entity-type":"item","numeric-id":3557074,"id":"Q3557074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$2C949B94-E1A5-4E95-B36B-E58BEFA10F4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fdfc9df2b22ccfe710854f5a13d2c017a857dca","datavalue":{"value":{"entity-type":"item","numeric-id":892235,"id":"Q892235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$4F4EF944-E5C7-4D11-BAC0-7E596C01EE76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e4aed9b8c360dba198361b37afc63de7b6c5158","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$8F6437AC-BDA8-407F-A851-A503014E7BD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b0e3385edfc17f41009a6fcefae201a99378f81","datavalue":{"value":{"entity-type":"item","numeric-id":4444404,"id":"Q4444404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$79090EE2-07CA-460A-A384-EA3C9D3D8C6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20a8d1807727f460772d228e59e0090da8175877","datavalue":{"value":{"entity-type":"item","numeric-id":3507450,"id":"Q3507450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$18DA7351-6F7D-4790-842B-49F764A01F7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b58d0abcd9e4d9a58c0a0e5204160a728cc8f","datavalue":{"value":{"entity-type":"item","numeric-id":4645727,"id":"Q4645727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$ED558884-A94B-4F99-A117-45D2F262B334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd36dae5803e0965ad10705e59b8bf6df76adb51","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2323449$EBAE4FAC-BF9C-4C4D-B040-13A95A6DD50F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"26e873cf544da7ee5e7b9f9d68d84599ccc7d280","datavalue":{"value":"10.1007/S10817-018-9490-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2323449$105450B1-7A13-4AEA-B86A-1CA07EC222B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8dbf993b7f17811830765c9730740b5c9d079ed0","datavalue":{"value":{"entity-type":"item","numeric-id":4645756,"id":"Q4645756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ba816d622c4f15c7e62f0140fa34f5e75971b16","datavalue":{"value":{"amount":"+0.9417228698730468","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":"Q2323449$13EC6D97-4E5D-4B10-8F7D-3554089D5887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c46791f725727301390062ee9067b8c556baabe2","datavalue":{"value":{"entity-type":"item","numeric-id":2818017,"id":"Q2818017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c24885bf5fc458a283de64bd482344a11b46588","datavalue":{"value":{"amount":"+0.8460621237754822","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":"Q2323449$6380F2C1-A932-4FEB-A9EE-5F83E8A10B00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6e92bb1e52dcbe4b71fbb4fb8a9dabdf590a402","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b598eb8b36be9de978b83a46b4d73a5af63cfba5","datavalue":{"value":{"amount":"+0.6750873327255249","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":"Q2323449$C9E35380-2496-42B4-AB8A-115934017ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e4ff4effde45de5ad7280333af6c6339508a949","datavalue":{"value":{"amount":"+0.6640399694442749","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":"Q2323449$C1BFB4DF-8293-404F-B449-F4DCAF5308B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"229fe24d9eb2e29f12beb6699f750b1db9dc03d9","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5273cfa31e5f58b87f23c0ff64bbf1f04786039","datavalue":{"value":{"amount":"+0.6627291440963745","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":"Q2323449$34E384B4-EF89-411A-8F46-E95637095575","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2323449","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2323449"}}}}}