{"entities":{"Q3690258":{"pageid":5720164,"ns":120,"title":"Item:Q3690258","lastrevid":50225300,"modified":"2026-01-13T14:02:30Z","type":"item","id":"Q3690258","labels":{"en":{"language":"en","value":"The use of machines to assist in rigorous proof"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3913722"}},"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":"Q3690258$DA3CD0CB-275C-45A1-A7B8-8212B1C60FC5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4b3a602b71e2b45a41f920882322365b29d73c3a","datavalue":{"value":{"text":"The use of machines to assist in rigorous proof","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3690258$4E3F073C-EB18-45AA-A332-B8293B5F2C3C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"05c75ba6b8f047ad54bb3f832226d57c71c06769","datavalue":{"value":"0572.68078","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3690258$7953B0BB-2B41-42CA-BBFD-47A2099CE666","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e136bbdda99981f780084921153c27ffb0ef7a8b","datavalue":{"value":{"entity-type":"item","numeric-id":3028582,"id":"Q3028582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3690258$6370384A-9ADB-45EC-90CE-93D76E9F71C9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3690258$60BBD16B-ECC5-49B7-BFCD-F2DF6644C878","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3690258$7E7453F5-B692-4185-BD59-C3DC2003DDA3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0a278e459fe3e6b3092b67b66be19a980a7b6a92","datavalue":{"value":"3913722","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3690258$6C0C8DF0-392A-4518-8FFF-16D8BF632C93","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"109c4221e7144572a3068b441e19092443735f31","datavalue":{"value":"computer assisted proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$1E98C451-2A0E-4BCB-9C58-332033E61432","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c80ecf21428f980362763aa3ec34b156b15c6fc","datavalue":{"value":"tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$3316CFCF-DC56-4ED1-B57A-B473024C87D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98b5b5a4f0c825ea91b5dc8ad46045a364b8968b","datavalue":{"value":"strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$B72F7539-5029-44F7-B2FA-AF8100A46A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9013265de525fdccb23da84af340da3a3f223ce7","datavalue":{"value":"algorithmic metalanguage","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$45B5AA72-33E1-4BEB-91B8-D08513B1D099","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"23328227337a3cafe924ff36301e08c88820342a","datavalue":{"value":"combinators","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$60370405-CB28-4BF4-B2D7-C43C5805BC53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d973ab3bba156ca63ad940ced10b1c8103ddff7a","datavalue":{"value":"elementary theory of goal-seeking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$012B415F-7343-4E1E-8172-CC5642C3B874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba1edfc01aec62ce1a4c141fe539d5cca3ffe26f","datavalue":{"value":"ancestry graph","type":"string"},"datatype":"string"},"type":"statement","id":"Q3690258$C2EE7C0A-465A-4C4E-8434-75604890BC88","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"08d0f7cb40ff2483df37c37d4baed93c13bb91e7","datavalue":{"value":{"entity-type":"item","numeric-id":1801221,"id":"Q1801221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3690258$AD0DB73F-4A28-44B4-8F6C-E69FA0985E71","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":"Q3690258$180CC7B9-DBA2-4D27-9972-787D98A9BF97","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"37280857397dc5084f3dc9e34202324b3ba21b92","datavalue":{"value":"https://doi.org/10.1098/rsta.1984.0067","type":"string"},"datatype":"url"},"type":"statement","id":"Q3690258$7329CC7B-00E7-4D98-8205-CD00CC801AB8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3946b905f6af03d95568fcd9668a6b410028e353","datavalue":{"value":"W2176475346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3690258$A2F5AE28-C084-4906-92E5-2248BEE0099E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"be9a1fea3f8c7b4428ddab0333adb58974432efe","datavalue":{"value":"10.1098/RSTA.1984.0067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3690258$19AA1082-BEF9-4BD1-B4B7-4786867D0E71","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e618eb39125574d30bf91fc8f948062d548b67f0","datavalue":{"value":{"entity-type":"item","numeric-id":3812289,"id":"Q3812289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eaf8bf8ef52141515f721b60b5ec86e502e7a4c9","datavalue":{"value":{"amount":"+0.742239773273468","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":"Q3690258$EB4154B4-77C9-4FC3-91A5-747C6385813C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ef6f8cd8718f1d64bdad3d35d2a8750a28f6eb9","datavalue":{"value":{"entity-type":"item","numeric-id":3759967,"id":"Q3759967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba35b795e50c284c65369851d0c71f94b93afbb1","datavalue":{"value":{"amount":"+0.7363765239715576","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":"Q3690258$C244331E-322E-4471-BB01-A4EC6B722E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c63bfe35d7420fdcebc1b80fdd6d3c92457c19b0","datavalue":{"value":{"entity-type":"item","numeric-id":4906868,"id":"Q4906868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"587b277cbd0de06c845f6dd22a6fef8a8fd32a02","datavalue":{"value":{"amount":"+0.7352257966995239","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":"Q3690258$FA1FD0A1-902F-4D6E-983C-0A0F2114988F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c0254df9f4f76cad0ec1855a19e97bfce6ef1bb","datavalue":{"value":{"entity-type":"item","numeric-id":2988059,"id":"Q2988059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6943d6359cb98dee68bf1760d27ac41ecdbb0e8","datavalue":{"value":{"amount":"+0.7318205833435059","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":"Q3690258$E8297AA1-0496-4D00-B505-89E830907554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dc42060a3c506d7dd41e1120918b2d738a6ec64","datavalue":{"value":{"entity-type":"item","numeric-id":1601835,"id":"Q1601835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae6579c701c5512169e56e440ea2739950b7ca88","datavalue":{"value":{"amount":"+0.729760468006134","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":"Q3690258$E07A6C39-9299-4A07-80C9-B17B97579389","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3690258","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3690258"}}}}}