{"entities":{"Q6481103":{"pageid":13977237,"ns":120,"title":"Item:Q6481103","lastrevid":104425414,"modified":"2026-07-10T19:39:25Z","type":"item","id":"Q6481103","labels":{"en":{"language":"en","value":"proof assistant"},"de":{"language":"de","value":"Maschinengest\u00fctztes Beweisen"}},"descriptions":{"en":{"language":"en","value":"software tool to assist with the development of formal proofs by human-machine collaboration"},"de":{"language":"de","value":"Computerprogramm zur Erzeugung und \u00dcberpr\u00fcfung von mathematischen Beweisen"}},"aliases":{"en":[{"language":"en","value":"interactive theorem prover"},{"language":"en","value":"theorem prover"},{"language":"en","value":"automated theorem prover"}]},"claims":{"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3c6b04cef9cbeaac99f228af5504d6614b55ff3b","datavalue":{"value":"Q11387554","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$0B1744FC-9D4B-4B97-B812-0EEA135B10FC","rank":"normal"}],"P36":[{"mainsnak":{"snaktype":"value","property":"P36","hash":"783a395d892e51fcf8a94ef667f018297aa11efb","datavalue":{"value":{"entity-type":"item","numeric-id":7280099,"id":"Q7280099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$30268F52-D7CA-4962-AF5B-5DB9B5AEFA4D","rank":"normal"}],"P236":[{"mainsnak":{"snaktype":"value","property":"P236","hash":"8528d7a330237e1f259f800883a5ae67c1170a2f","datavalue":{"value":{"entity-type":"item","numeric-id":7280100,"id":"Q7280100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$C5B9C0C3-2C82-4BE0-8B41-55FCA2526630","rank":"normal","references":[{"hash":"e095c1777d78c6310fee7299bfc6f5735414b4b7","snaks":{"P180":[{"snaktype":"value","property":"P180","hash":"0c2cea297152a3f12f4296fca42de18f460a63f3","datavalue":{"value":{"entity-type":"item","numeric-id":56456,"id":"Q56456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"snaks-order":["P180"]}]}],"P253":[{"mainsnak":{"snaktype":"value","property":"P253","hash":"26d27a441bc7f0f28cb674c43714058aa334fcb1","datavalue":{"value":{"entity-type":"item","numeric-id":6481096,"id":"Q6481096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$51BF00FA-4188-4EDB-A8D9-F3477B519503","rank":"normal"}],"P557":[{"mainsnak":{"snaktype":"value","property":"P557","hash":"3f7962866d72d7a299ab5d5114c9ac1b38f4d0b3","datavalue":{"value":{"entity-type":"item","numeric-id":7276377,"id":"Q7276377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$4D4E7530-1D6E-4589-94E6-FEC8441E069F","rank":"normal"}],"P373":[{"mainsnak":{"snaktype":"value","property":"P373","hash":"4c862b7d30584a347af4a2760070947319940567","datavalue":{"value":"13766981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$476F3270-61E6-45C1-98C2-F5165229112E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P373","hash":"ba55f0857a1dd2d2a34443a644f7430c18f845c6","datavalue":{"value":"203265346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$6F06841C-D98F-485C-B444-A3B4B070674E","rank":"normal"}],"P1195":[{"mainsnak":{"snaktype":"value","property":"P1195","hash":"8f675f34797f8ca0ac488dff31174ab1afe3409c","datavalue":{"value":"proof assistant","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$7670C510-D55E-49EF-AC4E-3FA680734B7A","rank":"normal"}],"P239":[{"mainsnak":{"snaktype":"value","property":"P239","hash":"c5836e3f85d5af0f235a82ee2c2024d7280c26ee","datavalue":{"value":"/m/04mw60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$D3B51B9F-E70D-4141-9E2A-DD6E0B4960F3","rank":"normal"}],"P300":[{"mainsnak":{"snaktype":"value","property":"P300","hash":"1894b3e787acc0d8fd3a7298abbd57ab3626d553","datavalue":{"value":"proof-assistant","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$8593E6C3-C746-4225-B8D3-5379637A1C25","rank":"normal","references":[{"hash":"81378df6482feaaeae9e3e0d7518e5ad24aacf97","snaks":{"P56":[{"snaktype":"value","property":"P56","hash":"3b8debd583a15ded2c0cea1d95a22ba400d5a8e4","datavalue":{"value":"https://github.com/topics/proof-assistant","type":"string"},"datatype":"url"}],"P159":[{"snaktype":"value","property":"P159","hash":"5aef604319c5c624f11720b57d6e90d11f040bbd","datavalue":{"value":{"text":"proof-assistant \u00b7 GitHub Topics \u00b7 GitHub","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"}],"P69":[{"snaktype":"value","property":"P69","hash":"fdda3ec550b9b0edfa2f56954e0422581d98220e","datavalue":{"value":{"time":"+2021-07-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"}]},"snaks-order":["P56","P159","P69"]}]}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"912895dee19728fd324b1f32a6a36192448d76f2","datavalue":{"value":"C13766981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$4F346EEF-C4EE-460D-8480-58573062B570","rank":"normal","references":[{"hash":"ada37bfccfef8253f9662eb411a7e44fd3bf600a","snaks":{"P98":[{"snaktype":"value","property":"P98","hash":"d98ff3d8cd81c87263e3f0008a1ae470fbcf55ae","datavalue":{"value":{"entity-type":"item","numeric-id":56612,"id":"Q56612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}],"P69":[{"snaktype":"value","property":"P69","hash":"a8b2a7e9de45fd3832b36f489407e826769f65b6","datavalue":{"value":{"time":"+2022-01-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"}],"P56":[{"snaktype":"value","property":"P56","hash":"f7cf0fc8f94cea909ab2fa761ee0f84fb1ca5b1a","datavalue":{"value":"https://docs.openalex.org/download-snapshot/snapshot-data-format","type":"string"},"datatype":"url"}],"P160":[{"snaktype":"value","property":"P160","hash":"91ab54c6c18e91aab482096dc9616607b7c6ad10","datavalue":{"value":"https://web.archive.org/web/20220125070108/https://docs.openalex.org/download-snapshot/snapshot-data-format","type":"string"},"datatype":"url"}],"P161":[{"snaktype":"value","property":"P161","hash":"bbaf8098d44f14564610a773940f9314d704bd81","datavalue":{"value":{"time":"+2022-01-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"}]},"snaks-order":["P98","P69","P56","P160","P161"]}]},{"mainsnak":{"snaktype":"value","property":"P388","hash":"fecc472c54fc0605add5cb385dfa6dabc05c0865","datavalue":{"value":"C203265346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$DB93DB62-125F-4C25-887B-38B7DB290875","rank":"normal","references":[{"hash":"b61840b5e4c07320c0aa508d1e9d37d18264ae22","snaks":{"P98":[{"snaktype":"value","property":"P98","hash":"d98ff3d8cd81c87263e3f0008a1ae470fbcf55ae","datavalue":{"value":{"entity-type":"item","numeric-id":56612,"id":"Q56612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}],"P69":[{"snaktype":"value","property":"P69","hash":"a8b2a7e9de45fd3832b36f489407e826769f65b6","datavalue":{"value":{"time":"+2022-01-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"}],"P56":[{"snaktype":"value","property":"P56","hash":"f7cf0fc8f94cea909ab2fa761ee0f84fb1ca5b1a","datavalue":{"value":"https://docs.openalex.org/download-snapshot/snapshot-data-format","type":"string"},"datatype":"url"}]},"snaks-order":["P98","P69","P56"]}]}],"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"9e06e40e89cbaba63f67bb397687c3fa4342250b","datavalue":{"value":{"entity-type":"item","numeric-id":56603,"id":"Q56603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$620C68CB-A684-4874-BB90-48D1846EDFB4","rank":"normal"}],"P1364":[{"mainsnak":{"snaktype":"value","property":"P1364","hash":"5b21bac34f1ac34e9a2910097f8c44e3458f2370","datavalue":{"value":"computer-science/theorem-prover","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$2E3DED7D-80D6-48B2-95E5-C25BC27C6100","rank":"normal"}],"P357":[{"mainsnak":{"snaktype":"value","property":"P357","hash":"b25d6c574a33e512dfa5019a9ef46e9c5f9bd580","datavalue":{"value":"https://mathoverflow.net/tags/proof-assistants","type":"string"},"datatype":"url"},"type":"statement","id":"Q6481103$93946600-93AE-48B9-A5ED-4FD100B1CF35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P357","hash":"4db6cb63f2a007002aa00aafaf51fb5c8a574d10","datavalue":{"value":"https://cs.stackexchange.com/tags/proof-assistants","type":"string"},"datatype":"url"},"type":"statement","id":"Q6481103$0589011E-5614-4F25-9711-00C87DD16F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P357","hash":"97912e6b943aaf8f515107bda5c1595d6fb75c2f","datavalue":{"value":"https://cstheory.stackexchange.com/tags/proof-assistants","type":"string"},"datatype":"url"},"type":"statement","id":"Q6481103$5169B3CE-5380-4FDB-9CD0-2D519268A5DD","rank":"normal"}],"P1526":[{"mainsnak":{"snaktype":"value","property":"P1526","hash":"e42dd2cfb5923be0faabc569e5295b2b2a1503dd","datavalue":{"value":"https://proofassistants.stackexchange.com","type":"string"},"datatype":"url"},"type":"statement","id":"Q6481103$68A38F1A-ED47-450C-B591-7D3C454C1B70","rank":"normal"}],"P356":[{"mainsnak":{"snaktype":"value","property":"P356","hash":"1d9b56ff51d3cffd380ac7a1aec8cf3e798490ad","datavalue":{"value":"CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png","type":"string"},"datatype":"commonsMedia"},"type":"statement","id":"Q6481103$67832984-CBB5-4C82-84D3-A29D52213636","rank":"normal"}],"P380":[{"mainsnak":{"snaktype":"value","property":"P380","hash":"7ed359834bebfe518a651a8710605dee00c5b82c","datavalue":{"value":"\uc99d\uba85\ubcf4\uc870\uae30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$A5004079-A696-4DA3-B766-C3C931A7ACDD","rank":"normal"}],"P265":[{"mainsnak":{"snaktype":"value","property":"P265","hash":"2d8761b82812dc86fb1bcebd5537498ff3f9e551","datavalue":{"value":{"entity-type":"item","numeric-id":7280101,"id":"Q7280101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$879E8C8B-C7F2-4DFD-A8CD-FDD701F70245","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P265","hash":"7380046b1ac2f77e29336aff9af80b5290dd152c","datavalue":{"value":{"entity-type":"item","numeric-id":7280102,"id":"Q7280102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$DB6FBD57-856C-4BF6-93C9-14A6F7CFB6B2","rank":"normal"}],"P250":[{"mainsnak":{"snaktype":"value","property":"P250","hash":"5f210b54f61b7ec3379cf9412e67acf122471bf4","datavalue":{"value":{"entity-type":"item","numeric-id":7280101,"id":"Q7280101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$44A94888-1D14-4148-9CDE-94962A678399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P250","hash":"df412cbe99618733d7073262c32300d438f5dce9","datavalue":{"value":{"entity-type":"item","numeric-id":7280103,"id":"Q7280103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$A960E2A3-75A3-4BF1-B993-D91C488CEE40","rank":"normal"}],"P95":[{"mainsnak":{"snaktype":"value","property":"P95","hash":"47e113c54259379d1f773d9f474a184cfc0f6b28","datavalue":{"value":{"entity-type":"item","numeric-id":7280104,"id":"Q7280104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6481103$05A7D427-78F4-46D0-BA59-B0042E4AFBCD","rank":"normal"}],"P1994":[{"mainsnak":{"snaktype":"value","property":"P1994","hash":"140493db42b001c53738c132b7576e23bc652a8d","datavalue":{"value":"automated theorem prover","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6481103$13C2161D-EFF6-4384-9179-3CF360DD6F97","rank":"normal"}]},"sitelinks":{}}}}