{"entities":{"Q6572537":{"pageid":14183692,"ns":120,"title":"Item:Q6572537","lastrevid":95765258,"modified":"2026-06-05T09:43:46Z","type":"item","id":"Q6572537","labels":{"en":{"language":"en","value":"A complete, mechanically-verified proof of the Banach-Tarski theorem in ACL2(r)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7881118"}},"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":"Q6572537$8D3755AB-3E6F-49F1-997F-09826B8B96F4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b9947b199b920af194233254beb798958dc5e76e","datavalue":{"value":{"text":"A complete, mechanically-verified proof of the Banach-Tarski theorem in ACL2(r)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6572537$1E464609-F50D-4366-AF53-7ADC50E9772E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d22fe5700702e33e3110e169f721b257d657390a","datavalue":{"value":{"entity-type":"item","numeric-id":6572536,"id":"Q6572536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572537$C03B5133-31DE-44B8-B364-AB0D295DF2D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53de145c1476af14e05c31ec8165f08e3c85436f","datavalue":{"value":{"entity-type":"item","numeric-id":230813,"id":"Q230813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572537$61F73CF7-685C-4C47-8C24-C466D9F690E3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7dae1a09e0b079923de71e99f58f11ff9161f5ec","datavalue":{"value":{"time":"+2024-07-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6572537$38EF5432-5BFC-4E33-87DC-BA3061FF3C58","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$6458D068-2835-4F15-B583-6655DA3AD454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$301BD736-8266-4AC9-B3B6-25744E2271B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2f1459d5951e049c51abbc0d85c8bd47bc411fa9","datavalue":{"value":"03E25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$DAF0AD0C-7BE9-4BDF-B894-8BC97453B895","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e478659c80ac196196a2283c8b16b79c8d8cd8d5","datavalue":{"value":"20E05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$3B1442A4-3CE6-4E03-A485-F375520BEC46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1d03248d03059e970bb6bce2ee9e31dfa76e4fd6","datavalue":{"value":"20H15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$F74A08AF-0184-4C8F-8BC9-DB0170A363B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d5ae9e2988e76d371f7e87b79bcd004ea2b80f64","datavalue":{"value":"51M20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$1FBBC82B-B1F1-43FA-8F94-1F0C8EED5AB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$825465DA-CA7E-4781-9782-6C160BD5840B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"166aa01488ff73659354d974e998a210d91ab396","datavalue":{"value":"7881118","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$A4F91546-F56D-4C9A-B337-507F290DA3A1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e53205031360cad8d1fbc5da72ad0197870a4743","datavalue":{"value":"ACL2(r)","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572537$2C93C975-3416-4E83-96AF-736DF3C612D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d01dd079e16eabb999ba826c5f48e3278d6b4aa","datavalue":{"value":"Banach-Tarski theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572537$3FAE338A-AA97-4185-945E-9BF0392F82B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"606852dbd1afd25d6e4db30e5eb1730624c372ff","datavalue":{"value":"rotations","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572537$8BB771C4-734A-431E-B124-B68CD838029E","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":"Q6572537$C2331D94-D59E-4A30-8068-FB7A76D23C6A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1c1a5852c533cbf7fca7dab42fc4831e4cb306fa","datavalue":{"value":"10.4230/LIPICS.ITP.2022.5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572537$0B3101AC-9AC1-488A-8E48-262B1978CDBA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a55a2bb5b3b9fad87ae56b599b0b2b416a957b0","datavalue":{"value":{"entity-type":"item","numeric-id":5195284,"id":"Q5195284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"631a59250c858ced92780b81ec8c187fc812ee1e","datavalue":{"value":{"amount":"+0.8915309906005859","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":"Q6572537$9CD7DF49-1864-4B37-A317-5DEB8E97AA64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e580b79bff341b3180ea22db9d0cb7de3531b2c0","datavalue":{"value":{"entity-type":"item","numeric-id":1110810,"id":"Q1110810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88f5aa9cc92e2af775956302e13790ef4019d3e7","datavalue":{"value":{"amount":"+0.816127359867096","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":"Q6572537$2B1AA3F5-9AC0-4DA0-9F6B-A98CDAD6514D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4987925cd393ab13d787178b4c692ad3eff729b","datavalue":{"value":{"entity-type":"item","numeric-id":6659920,"id":"Q6659920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78e4a6e51917917e33f80a2885f304a4a4976e89","datavalue":{"value":{"amount":"+0.7478237152099609","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":"Q6572537$34A7DA5C-A40D-4F03-AF4B-F5B9E5B07EF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce6df8f738a2ef8e31015cf0101dd5e4cfb3fd1f","datavalue":{"value":{"entity-type":"item","numeric-id":3687182,"id":"Q3687182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de2f03b8b060d4a3925e01cf55cdecb538672d61","datavalue":{"value":{"amount":"+0.7362826466560364","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":"Q6572537$95458174-9FF2-46C0-9011-8AC6B507993B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07701598eecddb8bac79f2dcf1e71e341a508501","datavalue":{"value":{"entity-type":"item","numeric-id":5718696,"id":"Q5718696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec41cb9320c5d8bbcdcc6d88056fc21ba23a8bfc","datavalue":{"value":{"amount":"+0.7247000336647034","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":"Q6572537$77E7324E-7717-4E4B-9DCE-90208EA87A76","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A complete, mechanically-verified proof of the Banach-Tarski theorem in ACL2(r)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_complete,_mechanically-verified_proof_of_the_Banach-Tarski_theorem_in_ACL2(r)"}}}}}