{"entities":{"Q6156630":{"pageid":13291178,"ns":120,"title":"Item:Q6156630","lastrevid":58724466,"modified":"2026-04-06T11:46:23Z","type":"item","id":"Q6156630","labels":{"en":{"language":"en","value":"Formalising Szemer\u00e9di's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7695705"}},"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":"Q6156630$E48969E7-2211-4DE4-B588-42421B83CF5A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be0996bc25fb029323f4af5154cf0835d9f3be7a","datavalue":{"value":{"text":"Formalising Szemer\u00e9di's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6156630$17AE141A-B101-4BA5-8CCF-C15F84F0E557","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0771934c4887fa6cdca5c7d66d14a214ab90b74","datavalue":{"value":{"entity-type":"item","numeric-id":2128786,"id":"Q2128786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$F2450A02-D6BD-4025-9B18-2BF19B40146A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"43720d5641a605df4a870ccd696a31d0b30078dc","datavalue":{"value":{"entity-type":"item","numeric-id":472315,"id":"Q472315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$7B656C6B-F265-4098-ADFC-23C85C21E8F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$EE373112-08D1-481E-B8EB-E4E678128BC4","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":"Q6156630$E673AD04-BA16-461E-A178-3E2F21B81104","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e078913baaf6e58e465be4601d94b7e1928c7c65","datavalue":{"value":{"time":"+2023-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6156630$84EF6199-23BF-4EFB-818F-E7E934123A37","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e11e9ce102297acb78ba53eb9efd315cbad1cde5","datavalue":{"value":"https://arxiv.org/abs/2207.07499","type":"string"},"datatype":"url"},"type":"statement","id":"Q6156630$C081EEA7-9FE3-459D-B810-FE6EEB6128A6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$7B020519-C111-4D0E-9BC6-8F4E525C366B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5a3bb76dbd41580d9287ece5137de80ddf22202f","datavalue":{"value":"05C35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$F7C778EA-E5EA-4519-B4A3-CD6A83B69015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58d33fcd5e5cb8a52812aa5e4a2f3f30b5cf0e30","datavalue":{"value":"05A17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$B54CA6FA-8356-4F8D-BE05-433AB15900A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"679ddfba371ea56c373d120bb6ab79b1a5d003aa","datavalue":{"value":"11P81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$0E3277E9-B605-4BB5-B003-F0B71FB52B7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$5F1E26DB-650D-4747-9AC5-0239046452AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$0BEC2E04-52D3-4DD0-B356-8F007078DFE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fee8f2ca1323cad9e9232d7279e663a6ec082a12","datavalue":{"value":"68V35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$E61B7B8C-76B4-44AD-BF0D-212F80E461AB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0d6dcca8cc5a53d27fe233d5e2a817f4b649858","datavalue":{"value":"7695705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$ECC35B0B-C625-4E76-BAC8-F6FBB8EBFC52","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$06CB7945-123A-4191-9542-1AE4186D3CDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$2CD9946F-71C3-43AC-AB8A-9F1C6B457519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78c180ee2d56162da3a93e683315dfd57d39ecfb","datavalue":{"value":"formalisation of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$A0AAD6D8-28B1-47BD-B04C-769F3F84B62C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$CE4B2F6D-B440-4D86-85C8-7F7B65A5FC28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f76c961d13b0be6c6be0a730f3c9f86ee2be4ae6","datavalue":{"value":"additive combinatorics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$552D78D9-3BBE-466A-8DA9-F9D9CCC5DD19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"013a665df3872df6518b386ba286fc369d4eed69","datavalue":{"value":"extremal graph theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$C0FF1AE7-1AB9-435D-9763-F1DEB8C7115B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"19986b8fecb43e8171ffe4a0d4b192174eb7ee8a","datavalue":{"value":"arithmetic progressions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$6B881D1D-5192-403D-9A5B-A0870B67A379","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf9020b9cf738e3dc19adb35ae396c6478d2142c","datavalue":{"value":"number theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156630$7BF7BE7D-397E-4BBD-91D4-E2DBB63AC884","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":"Q6156630$FF2A9B44-FC86-4F36-9961-9C112E2F5DC8","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9bd6599f241f729119fbda7d81701866ea93867e","datavalue":{"value":"Q124823534","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$BD853456-E134-4919-B175-DABE4129113A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"184ede4bc6ed882d79e26c2571ed48b5be9ffdf9","datavalue":{"value":{"entity-type":"item","numeric-id":489922,"id":"Q489922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$713E89DD-FE94-4537-B3DE-D8309171D168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"650620a8abff65a78f27b6d9c816323baf828dab","datavalue":{"value":{"entity-type":"item","numeric-id":2829286,"id":"Q2829286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$A25EA4FC-92C4-4F85-9510-071964116138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8c5f5c617e488fb494238f1e4d7368bf494f4df","datavalue":{"value":{"entity-type":"item","numeric-id":5094473,"id":"Q5094473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$67DF9D9B-9BBC-4A17-A690-F90E346E271B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"def6234784a4e6f6bc65ca083208e450bba27962","datavalue":{"value":{"entity-type":"item","numeric-id":2128787,"id":"Q2128787"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$CEE6A6D5-64F0-4C70-87CF-00A731434E01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04878c17a52366e8b88817dade983f0d014bb75b","datavalue":{"value":{"entity-type":"item","numeric-id":4543625,"id":"Q4543625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$83CBB8B2-49BD-4C3E-A3C5-06FE7C69AB3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74d0f87a7a9c77dbc12879de09aa35c23b818174","datavalue":{"value":{"entity-type":"item","numeric-id":1233943,"id":"Q1233943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$FBAF125E-DA55-46DD-AA57-88696AD2878A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe8baecfc04675db06c9a7aa8134ee8db9a22a91","datavalue":{"value":{"entity-type":"item","numeric-id":1355452,"id":"Q1355452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$CF775F50-3F08-433B-B62C-029FCE2CF6BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9e49449785c72925392b01526a9ab53fe19cc47","datavalue":{"value":{"entity-type":"item","numeric-id":5945509,"id":"Q5945509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$B7124C92-42B5-46EF-9EB0-62C663BE371A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"936e0b8b21c457652556ed6024621c2aebe0087a","datavalue":{"value":{"entity-type":"item","numeric-id":3373662,"id":"Q3373662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$2E31D105-22FA-4678-B053-71B57239DE7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cab85a43c3a2c622940dade0ce475e90ad2f2b75","datavalue":{"value":{"entity-type":"item","numeric-id":2482877,"id":"Q2482877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$FDBEAD15-FD91-4440-80D4-F305F1A0B94A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ff364e631d863b084215c48810e99fa1bfff1cb","datavalue":{"value":{"entity-type":"item","numeric-id":5416079,"id":"Q5416079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$EED917A4-2F2E-4466-A061-0C090F58FC89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61e00816d41bd2d4b67fee36c40563eba3cadf6c","datavalue":{"value":{"entity-type":"item","numeric-id":2389092,"id":"Q2389092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$58624E59-B512-4E45-80F7-AE01221471F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"356dc800ec5cc6252d3d2d475ca06b5e6e231114","datavalue":{"value":{"entity-type":"item","numeric-id":5401732,"id":"Q5401732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$9E27E193-E7DC-4439-BCBB-598D2570BCE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9b07a671811203f6a204d4a2b5c177bf8333da6","datavalue":{"value":{"entity-type":"item","numeric-id":5469145,"id":"Q5469145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$85150358-2D50-4015-8C88-F281FAE46F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$C3E5FDE3-D49D-41B3-87E9-2A56D5155F6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"746c848c1a777ca7c05056491f34cd7aeedd8f44","datavalue":{"value":{"entity-type":"item","numeric-id":2914757,"id":"Q2914757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$E6083205-9F55-435F-BB70-AFAB65979028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"517fc8b23acecbf986165d1288d8b39f955c2983","datavalue":{"value":{"entity-type":"item","numeric-id":2018659,"id":"Q2018659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$606506A7-B147-472D-A399-44574C7DA625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6338bca81e53c965091acbd1f3efe5cc3498527d","datavalue":{"value":{"entity-type":"item","numeric-id":5410136,"id":"Q5410136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$C0A51BDA-A8FB-4A33-A5B6-B0511A964E20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35ee54a9479275c80b01b5f7467a8929c76b76ab","datavalue":{"value":{"entity-type":"item","numeric-id":4810506,"id":"Q4810506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$A54B8141-9022-409E-9322-653567A1DA5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15d52442185806241e37970954310dd2ed59667f","datavalue":{"value":{"entity-type":"item","numeric-id":5817505,"id":"Q5817505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$BB579688-E076-4A6D-B71C-901DD088DF85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"922598857b64c682415741da5fd4eb7cb848d71b","datavalue":{"value":{"entity-type":"item","numeric-id":4200109,"id":"Q4200109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$D529A8D0-1F87-497B-A449-67983569F0BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b430b25e563f4f6fd47d0ca0b91803e6578b04f","datavalue":{"value":{"entity-type":"item","numeric-id":4059028,"id":"Q4059028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$DAA61EBB-84E6-4A74-A6C9-D4EF86A286E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f835549fdf43c55364ed02f061dd539e885bee8","datavalue":{"value":{"entity-type":"item","numeric-id":5480762,"id":"Q5480762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$02E30BEC-E068-45A7-9847-33AC72A62872","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8a0ae6d3ff2feea49f6228ba10747dcdaf49ccaf","datavalue":{"value":"10.1007/S10817-022-09650-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156630$40C80E3B-8187-41C9-893A-1A751591AF49","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156630$CFA904D0-F1C5-4646-84F8-0EEB3F6565FC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6156630","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6156630"}}}}}