{"entities":{"Q6643006":{"pageid":14254161,"ns":120,"title":"Item:Q6643006","lastrevid":42400333,"modified":"2025-06-15T00:12:20Z","type":"item","id":"Q6643006","labels":{"en":{"language":"en","value":"An extensible user interface for Lean 4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7949117"}},"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":"Q6643006$A4D4DFB6-536A-4545-A096-AE5D15F70F4C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0019f45ce62345147becfc5acd053c25da158c15","datavalue":{"value":{"text":"An extensible user interface for Lean 4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6643006$148607E5-3153-4E09-8D1F-F61511F0A927","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9b787fd7291928cf7d532c00855d94cea20b5856","datavalue":{"value":{"entity-type":"item","numeric-id":2118331,"id":"Q2118331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6643006$B6015DBF-CF43-4435-9EAA-05145D5C92D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c8b130515804cee740998b0f664f3c6c23d65127","datavalue":{"value":{"entity-type":"item","numeric-id":6157244,"id":"Q6157244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6643006$6BB8B2F9-827D-451E-9E3D-FAA7BFB97E1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aefce4072ff7b8c016ef35d01c9736e705e82ce2","datavalue":{"value":{"entity-type":"item","numeric-id":1622973,"id":"Q1622973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6643006$973CEB09-1C88-4A0A-B764-9AE7A977EA8B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b1403ced2efacb118ecfb16a875f7c27f30cf0dc","datavalue":{"value":{"time":"+2024-11-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6643006$A2BA93E1-4B46-41B8-948E-05803C6D879C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6643006$94A20C7C-5024-4297-BF05-AB6C86135832","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74f55facdcb71291519f75d67bbdc76d40985f4f","datavalue":{"value":"7949117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6643006$C241FF2F-96C7-4403-A5BB-44468511EAD1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e5bc49cd8610ce6f7d0777176b15c8db9fe681a","datavalue":{"value":"user interfaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q6643006$270864C7-40C6-4D40-BB4B-BADCE2A51634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf5330db657891298ade39aa15a62df1e1be790f","datavalue":{"value":"human-computer interaction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6643006$8B299AD8-378C-4E90-9D6F-ACD152654A9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q6643006$89AEE210-85D3-4CD1-AE47-76F3AF30D7A0","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":"Q6643006$ACC6E955-7C10-4786-A90A-46EAC58A52D2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"23ecaa943f363cec956df3e5e8d89179dab85414","datavalue":{"value":"10.4230/LIPICS.ITP.2023.24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6643006$6AD7621E-EB59-4DB9-B2E2-E03D982850DC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6643006","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6643006"}}}}}