{"entities":{"Q3454108":{"pageid":5233508,"ns":120,"title":"Item:Q3454108","lastrevid":52405976,"modified":"2026-01-22T14:06:13Z","type":"item","id":"Q3454108","labels":{"en":{"language":"en","value":"The Lean theorem prover (system description)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515520"}},"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":"Q3454108$5B0DD455-A3D5-4259-B0A9-EBFE21E65BDD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"28da9e5ac065260a90c9d51d410c13bac84d606a","datavalue":{"value":{"text":"The Lean Theorem Prover (System Description)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454108$BF3F8394-142D-4CFD-B925-D2D975FAB7B9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"16eb158d728855d2a872a834364af0d1a7239b09","datavalue":{"value":"1465.68279","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$44F7BD61-28A7-4ED7-B487-928C24500A2C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a797d9edf8d7546f7524a355f489b18b0bedfcb8","datavalue":{"value":"10.1007/978-3-319-21401-6_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$8E609822-F66F-4B07-8CCA-A1B7874484F7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"899468d0fe4ec0ae9c5ef91b63881ae72bf40a46","datavalue":{"value":{"entity-type":"item","numeric-id":438532,"id":"Q438532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$1C32D605-FF78-4B3C-AB34-168437972ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7463120a9e955f48ddb24bcc00e63bd6fcf27d63","datavalue":{"value":{"entity-type":"item","numeric-id":2926662,"id":"Q2926662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$AE079D6E-3C6E-48A1-B540-BD12AD8C8EDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"834b9908deaa5f43ae5b55e2029a1dd9a50ccc06","datavalue":{"value":{"entity-type":"item","numeric-id":287376,"id":"Q287376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$88E15CE6-2F2C-4262-BC4E-85BCD65BE025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dc9f7061148c184d156fce1cd302b98949f36de","datavalue":{"value":{"entity-type":"item","numeric-id":1687767,"id":"Q1687767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$7F0808C0-98B9-4F98-AD79-C9BBE3765CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ed91f18c49a16f542aacf01077ba8073712fd1e","datavalue":{"value":{"entity-type":"item","numeric-id":1687768,"id":"Q1687768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$83BA06CD-C5DC-42A5-8806-65092895D1A7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$44D724D7-3637-4D94-83EC-54DD1D8E2A43","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454108$9B55452D-8EE2-42A2-A620-9B2251B3F46A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f6b2dfce9432df5ff5ad1f95aaa0e61493658d9a","datavalue":{"value":"https://figshare.com/articles/journal_contribution/The_Lean_Theorem_Prover_system_description_/6492815","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454108$F5C25B58-868A-454D-B2A5-CC43A2E69066","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$7962E637-D70F-4F62-B6DA-D674B77C605E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$26F56A04-3BB1-4E78-B732-F9949BFA796E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d7cb6000b2dc5fb8dd1bb3bdee09fb0435b7b588","datavalue":{"value":"6515520","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$56290A80-3844-4F07-892F-C4179AD49B37","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$BA56246E-E568-47D5-ADB0-874A69E406B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$3E6FDAA1-B561-45F0-A8B6-5A42D3336D1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$49C0316F-01F6-49A1-9496-1C7E9ACCE237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$042C9615-CF3D-4401-A440-3C37CCCE9236","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$9E737377-A7EF-4C8E-9D35-DF269FAA5B5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$1E81B095-A828-4B4F-BF10-F3D41CB50FA8","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":"Q3454108$07F4E742-D7C6-4559-8B06-58F0C83B91D3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5c9695837eb7907245c27c2dfea1c4b95fb850df","datavalue":{"value":"W1464569014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454108$BFB4FBA5-9861-4BE2-AC74-85C0D8657155","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe1455cc5dda38390654a9baeba09eedb655d2e","datavalue":{"value":{"entity-type":"item","numeric-id":5200015,"id":"Q5200015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$87751A89-90D9-4B21-B1B4-7480D58BAB33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$ADADFD6C-CFF4-4BA0-9282-2BC2523641D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0191c8d55bfb13f05e230de930538ee944fa6808","datavalue":{"value":{"entity-type":"item","numeric-id":1336951,"id":"Q1336951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$B54BDA35-B20C-4A5E-89F2-3DC7B524A838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97aac3e9983bb038948e2fba3a98c71cc7d8d801","datavalue":{"value":{"entity-type":"item","numeric-id":5757920,"id":"Q5757920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$2D338987-41F7-49FA-A233-464D96D0AB05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$282B137B-5233-41D0-8FA6-1036A132FD2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d380a2f18f4b02ba06d230258197a946757b5301","datavalue":{"value":{"entity-type":"item","numeric-id":2891520,"id":"Q2891520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$E6C3C220-CB07-417B-A713-0A4CA2F78ADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1cb314be56584c4a3b78c42d4c6a1e8e149e010","datavalue":{"value":{"entity-type":"item","numeric-id":3649136,"id":"Q3649136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454108$2298509C-EF08-41F8-8DA4-0C75031CE077","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5240345605b6df958dc529fb8dc1a54b30d31b3","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9fcc52052e96e38b0562caa3c79a748080f2959","datavalue":{"value":{"amount":"+0.7955777049064636","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":"Q3454108$B5C071DE-C59B-4C83-B4B5-6CF2923B7EBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1ddbb86d140ec3223259a8a03fe1927db75bf35","datavalue":{"value":{"entity-type":"item","numeric-id":4539627,"id":"Q4539627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af4585cccfaba9f70628e1eee49a4510d5f5d0ef","datavalue":{"value":{"amount":"+0.7523141503334045","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":"Q3454108$DA1C3F89-AFBD-401C-AE12-09E752160B3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdade178ac9ba6848e51f8546460e812ce1b68c5","datavalue":{"value":{"entity-type":"item","numeric-id":5200015,"id":"Q5200015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6dbb0bd09940a72d601b6aec88eba13f066fff7d","datavalue":{"value":{"amount":"+0.7499289512634277","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":"Q3454108$3943A2B5-E807-4866-8714-BB19A6356308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a02b2bfea1c5f47cd601f5ce8d9525ee86d87fe","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb262b3abc036d001a858dd4121cf60e5850fb40","datavalue":{"value":{"amount":"+0.749499499797821","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":"Q3454108$6F05DEBF-AC53-45A6-A211-3709EF70649E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16b4ad2e93424e9b6828135c36f028dc0dcc0af4","datavalue":{"value":{"entity-type":"item","numeric-id":2219381,"id":"Q2219381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45783489d25287d08462d56368de86ab0e45b8e1","datavalue":{"value":{"amount":"+0.7489942908287048","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":"Q3454108$06ABBF8A-6ADA-4638-A898-8AFE7E673637","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3454108","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3454108"}}}}}