{"entities":{"Q6648159":{"pageid":14259314,"ns":120,"title":"Item:Q6648159","lastrevid":95679746,"modified":"2026-06-05T09:34:00Z","type":"item","id":"Q6648159","labels":{"en":{"language":"en","value":"Formalizing finite Ramsey theory in Lean 4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7953760"}},"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":"Q6648159$02D8F12A-54C4-499D-B89A-8987718DC001","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0bf6ce73b75f8f5c6f93c8ac3f23fe89ec457f09","datavalue":{"value":{"text":"Formalizing finite Ramsey theory in Lean 4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6648159$1648FB7F-269A-447A-861A-2CA948982EFE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e14f127651b79415411d709fbac717f5e1edc2e3","datavalue":{"value":"10.1007/978-3-031-66997-2_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6648159$F539EE9B-BE02-4FD7-AAE4-27054DB00CAB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0032e47507cdddb70771dd3b5d22ff8b2fe522f","datavalue":{"value":{"entity-type":"item","numeric-id":2051796,"id":"Q2051796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$59F6263C-6809-4034-A934-5667381EFAB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"de0461f113f34dd5ae38b4047c25f04ce3f9ebc0","datavalue":{"value":{"entity-type":"item","numeric-id":6648158,"id":"Q6648158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$20244BFA-445F-4115-AEAC-8FA992C91E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2d1fadcd5ad7fffd9648e4500f4cbd7347e1f33c","datavalue":{"value":{"entity-type":"item","numeric-id":6458507,"id":"Q6458507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$3FF046A0-C357-44FC-A374-0ABE06F2C313","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ccff15d9590e90858f5b15c952f30abae81c0114","datavalue":{"value":{"time":"+2024-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6648159$30FBF881-7957-4588-8CFB-E04AA85FC583","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"51b7800ccceb407b4c9aa81c10252a3a04dbfebf","datavalue":{"value":"68Vxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6648159$841A977C-BEA6-4B33-8A53-3ACBE28B4F99","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2ce2b03037adebedb84ae4f4e8673b011bf3d395","datavalue":{"value":"7953760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6648159$9965CDAD-B8AD-49F6-9A37-553BE6E60D6E","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":"Q6648159$16D2AAD4-96D5-4782-AED9-73F94F6E5483","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c3f5d6931f34b6cb61ea0d9e21b0db31cabd630","datavalue":{"value":{"entity-type":"item","numeric-id":3619878,"id":"Q3619878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$1F5EA466-A367-4354-8966-DCEE12184F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab929c474f6191a6b9764b4a6b4e6045c76d6b2f","datavalue":{"value":{"entity-type":"item","numeric-id":5138449,"id":"Q5138449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$18D06F1B-164C-4BB7-A05A-8D78E6D98618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2abbcba5eb8179d91d3514fec4c140f1da00e5ce","datavalue":{"value":{"entity-type":"item","numeric-id":5338793,"id":"Q5338793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$2FDD726E-E3A1-4F31-984C-FF29358C9CCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee63d0a112698cff8798f2125e3c1c3efdaff042","datavalue":{"value":{"entity-type":"item","numeric-id":1143432,"id":"Q1143432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$BC24967A-A551-44FF-8E90-0C17B7E99E4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"911dc472b42385440ffea56836f44f396d27035a","datavalue":{"value":{"entity-type":"item","numeric-id":2553974,"id":"Q2553974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$B6F8E826-D7F7-471D-A0B1-D7ABAC713E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3647fe00e3b83141b14436c1949063f538c83988","datavalue":{"value":{"entity-type":"item","numeric-id":3997075,"id":"Q3997075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$7F9074BB-2479-498A-8AFA-028F904EF375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82d3089399d36a7bbc48ab2d19e8bf56dc79deee","datavalue":{"value":{"entity-type":"item","numeric-id":5847742,"id":"Q5847742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$81DA5C25-E7B2-4BB9-A253-0F9AFCD666DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8ea0dbc94fcc949376136ff176ea3805b3c37f8","datavalue":{"value":{"entity-type":"item","numeric-id":870059,"id":"Q870059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$C741CE64-00B4-4795-81D6-EE38603B2297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a30bc125421999969ba2f186689a9c83cd75ca08","datavalue":{"value":{"entity-type":"item","numeric-id":3546251,"id":"Q3546251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$EE0968C6-0838-4953-BFFD-2748516431BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6db714be85ebdc099302c438fed04e7aa8f92771","datavalue":{"value":{"entity-type":"item","numeric-id":6159369,"id":"Q6159369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$2A036C77-1A78-42B4-A752-37B41FCFA4F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0439d8d4a0092c4e49af8b7a3ba4edcd0d59c397","datavalue":{"value":{"entity-type":"item","numeric-id":436623,"id":"Q436623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$4AC2C724-14E4-41F8-A1CD-799B75130301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c571423fc795d1f4ba9cbbd6d26f2561165df37e","datavalue":{"value":{"entity-type":"item","numeric-id":1834559,"id":"Q1834559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$8A4D653F-F21C-4CA0-96EA-ADA336C949EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"779dd2590cf3135d7aa727c38aea77d3bae5e723","datavalue":{"value":{"entity-type":"item","numeric-id":1470108,"id":"Q1470108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$0A348621-0A48-425A-BDB3-DB3B09B0F705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6648159$62CD96BA-8270-4D9D-83E1-21F6A4EFDF9C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing finite Ramsey theory in Lean 4","badges":[]}}}}}