{"entities":{"Q6916482":{"pageid":21001306,"ns":120,"title":"Item:Q6916482","lastrevid":84149393,"modified":"2026-05-11T08:49:22Z","type":"item","id":"Q6916482","labels":{"en":{"language":"en","value":"An introduction to mathematical formalization based on lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8105594"}},"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":"Q6916482$3D350768-8A04-448E-BB4D-C98958ED6A8C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"685b8449e9d758564e970ae8f2f7312d5beb98e3","datavalue":{"value":{"text":"An introduction to mathematical formalization based on lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6916482$DD308F78-821E-4FA4-A4E5-C13449DB1B33","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"57fe8d0b005394ece3ea6e92df7d3d1ce752eb11","datavalue":{"value":"10.12286/JSSX.J2024-1273","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6916482$A0FAB899-A6BF-4F5D-AD68-7B8E4D820EFE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"48aae82a72570bba701ce245a09703c18497386a","datavalue":{"value":{"entity-type":"item","numeric-id":6526464,"id":"Q6526464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$2A38F330-1E58-439C-BD42-9ECC9A838BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"959d041b6b148da37ce64ede0ac97938dac137a0","datavalue":{"value":{"entity-type":"item","numeric-id":341316,"id":"Q341316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$F806E13A-348C-4F33-8DDD-C2C758A41884","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70c5eac07e4926fce7a5478d857a57e1b885b9ae","datavalue":{"value":{"entity-type":"item","numeric-id":6665158,"id":"Q6665158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$9C68ABE4-A004-449C-88E2-F784840EE5D7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1be1a084743b7fe843755b397196118f7c063294","datavalue":{"value":{"time":"+2025-10-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":"Q6916482$8DE89916-8639-4360-A4BD-6EA1E1A10F1A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6916482$02F0E898-6822-48DD-98E4-367F3C764DD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"843de71235f44a800ae389e1734df6bb7650efec","datavalue":{"value":"65K10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6916482$CE8D1DC6-EA45-4154-BE13-C76667A0B4C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed10a41ec587cb61dc683f25ef4b3e827c7fee2f","datavalue":{"value":"90C26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6916482$9747E32A-65B4-4F2A-935D-AC037C1823A6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f507d3c74f51c70886426d29189965bf231c25b2","datavalue":{"value":"8105594","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6916482$902AE649-1ECA-415F-A11C-F18DCD9D94D2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q6916482$96DB49E8-5E93-4162-AB88-15BDB186524E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c27024bc3112e6fbf1cca0a9a4aacb8e7e4a77e0","datavalue":{"value":"optimization","type":"string"},"datatype":"string"},"type":"statement","id":"Q6916482$E42CF8BF-1F1B-42D3-961C-EE7F7CE5F535","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ce17008ab87357604ac3f15db7ccdd0e641cf40","datavalue":{"value":"computational mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6916482$452B7873-6F97-47E2-8985-38857A367723","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":"Q6916482$528FC485-8BFD-448C-A065-AA7E4E418F50","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$E1734AD2-EE3B-400A-94F2-BC7AAE78B189","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":"Q6916482$237C138F-71A6-44E7-B6A5-94533BE27B6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$51068CF7-3887-49A5-BC0E-6B7EAD46E22F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6223d1a82a63d3de094ae509c06c9ed081b3d007","datavalue":{"value":{"entity-type":"item","numeric-id":6859985,"id":"Q6859985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$70F8385A-33AB-4BC1-AE23-E8DDBC71F847","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06915d48bbf7054c0453df5751fc3c3ab2864b68","datavalue":{"value":{"entity-type":"item","numeric-id":6860031,"id":"Q6860031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$FB2A41B1-8E51-4DDD-8112-3F6A757C1648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017024655eece3d1dfaadd1daab89ddb6f0e7942","datavalue":{"value":{"entity-type":"item","numeric-id":6642979,"id":"Q6642979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$86A24841-6878-4A00-8F41-C245951B5613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6794f70cca3a930e83d52db00e6ce47d205c33e","datavalue":{"value":{"entity-type":"item","numeric-id":6860028,"id":"Q6860028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6916482$86BD549B-FDF2-4B80-B94E-AC19ABD87271","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An introduction to mathematical formalization based on lean","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_introduction_to_mathematical_formalization_based_on_lean"}}}}}