{"entities":{"Q4373335":{"pageid":6402934,"ns":120,"title":"Item:Q4373335","lastrevid":108315254,"modified":"2026-11-05T21:28:53Z","type":"item","id":"Q4373335","labels":{"en":{"language":"en","value":"The Logical Structure of Computer-Aided Mathematical Reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1107419"}},"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":"Q4373335$CDEB899D-7F5D-42E0-8F66-A40AA96DAC7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f3b614da8a06610412270f4fe7cd900c28b2655e","datavalue":{"value":{"text":"The Logical Structure of Computer-Aided Mathematical Reasoning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4373335$E2141D9A-A907-44F7-B969-28F37BE58DAB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c045e3c8f946c3060034dfa454b6a98c637b4755","datavalue":{"value":"0891.00001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$07387EBF-A368-40B3-B461-F535F200CCAC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"71e669d6ef68b28e74b787a7938ae63d520ccf5b","datavalue":{"value":"10.2307/2975057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$F22DCA1B-23E3-40CF-BACC-F6EEAFB2D05C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"cb96b4ac991d1c9fabb6ef3d281db52e4eb2e155","datavalue":{"value":{"entity-type":"item","numeric-id":93751,"id":"Q93751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4373335$FDC9D360-2626-445E-9462-D2AAAAB3FF87","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"322ecd43c31b54848c738d5755b8976de554681a","datavalue":{"value":{"time":"+1998-07-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4373335$60493569-9CD3-4CD4-BFB8-779C0B60C3FB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a4bd060761544b1cc1e1a5443f31290ce4c99e00","datavalue":{"value":"00A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$49D2462A-F9A7-4C07-BD56-26C58CB54211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8185bbfdd4506f4c14d2d3b46dfb55f8bdc3864","datavalue":{"value":"00A30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$5DD47BDC-E822-48A2-8A0D-113690BCBC42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9a40bc6020a753d5c0fbe6e70014c173b25058d7","datavalue":{"value":"00A06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$64F5701E-72C9-4DC7-8DB3-7F42D1B979A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"583f5b413168fbae938ab6e84f275da91256e071","datavalue":{"value":"00A69","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$511FE6C8-FEF6-497D-A165-97BFDDBEEB05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"654b667013631be85bc45fdfe776d3b9ed2e5330","datavalue":{"value":"00A35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$8AB9CF59-5BB4-40ED-AFD7-4AEC4ACD72DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"48a2830216eefdc24b89ba9895c8f20366f6740d","datavalue":{"value":"03A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$C89B1222-DB46-4E8F-8138-7F1E3AF3ED85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$986667D9-3451-440E-BC51-F394F910F961","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"099ff5bfcd7ff559991236ba47b1a3e9dc5f52bd","datavalue":{"value":"1107419","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$7DE17A8E-0AD0-4EA7-A1DA-DE20ABB3AE42","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83a4003069926cc612c694964e3cbdf707c8f2c7","datavalue":{"value":"computer-aided proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$DEC9E36E-E042-4D52-A226-568D868E8DC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae57d2d9059c2d51a5d49ad79ae53bd6a04f800e","datavalue":{"value":"logic of mathematical discovery","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$CE51CF5D-A4DE-497D-BB26-2D4B40ADBDA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e977db44bd54fd53e55c7cddc5eaab507bef6107","datavalue":{"value":"philosophy of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$03C3F1CF-FA84-4357-A71D-E6887D1A136F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a737d57830bd39c6e0b4446cb3961afe6c6e5a13","datavalue":{"value":"heuristic methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$813B12D8-E478-47A1-8924-85B0014C4EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"755a933adb167e01eae33695d067a9b3b5cd353c","datavalue":{"value":"situation calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$C08A3E28-03BA-4262-9C9C-8C7AFCA6C0DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c823b56192bce445b4b9ec3d99d959d2bc7a655","datavalue":{"value":"artificial intelligence","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$346C2156-2015-4BBE-8DE2-FF79A652234C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc36520fd57f0cee4d3a97f8e0546644cada3e1c","datavalue":{"value":"common sense reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$874DFDBD-0DA3-4C50-9612-90570B1B02C6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3702e20aa2b5746c3c7ac14d24195909e42e553a","datavalue":{"value":{"entity-type":"item","numeric-id":1138544,"id":"Q1138544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4373335$D0472294-55C5-417D-AFD1-3A3C8202C287","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4373335$F1929E37-69F1-44C2-AEE8-C08F1B8AD16D","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":"Q4373335$5555A6BD-D491-44EE-8BFC-830F4D69CB7C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"035bc24da31d7ec90e89f20b0f88939a597d12dc","datavalue":{"value":"https://doi.org/10.2307/2975057","type":"string"},"datatype":"url"},"type":"statement","id":"Q4373335$CB11E4DC-63C0-4DFB-864E-4DF5FB74C15F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"212a5289cedad48c39c78ef8e0ccb22c8e212d55","datavalue":{"value":"W4234615591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4373335$730DF34C-519E-464D-B714-2E306E971608","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ce05bb1fd459e915222ffd11d222df4c8e95d3f","datavalue":{"value":{"entity-type":"item","numeric-id":3327746,"id":"Q3327746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac7be54d2f65b8fbdc8c654c47debae002f80f41","datavalue":{"value":{"amount":"+0.919925","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$9CB5D9FB-7272-4039-8325-37AD604D5AF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"708792ce3dbf2f0f13c0d570467d3249161df16e","datavalue":{"value":{"entity-type":"item","numeric-id":4694210,"id":"Q4694210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39c06a10bde2128a08d8900dfc77cb4d58a63235","datavalue":{"value":{"amount":"+0.913415","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$E8D0FC6B-F13F-4EE6-9B6E-FA7425B151C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"027b559043e6257dda9a0b8a108abb3237e68b70","datavalue":{"value":{"entity-type":"item","numeric-id":4205404,"id":"Q4205404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5b990b0780902675c6fbf99aba6cf0e6ef34d71","datavalue":{"value":{"amount":"+0.898479","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$83753A83-3AB7-4870-B194-CB022E2967B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4334d8ba5afaa3755ced118c965b8436fa1bd1f6","datavalue":{"value":{"entity-type":"item","numeric-id":4272504,"id":"Q4272504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"79622f4d28a945325a09cdf654f7eb306806a396","datavalue":{"value":{"amount":"+0.89358103","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$F03CCB77-9435-4BDC-8ADC-B347DDC80405","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"099a133aa6561b9f20fea89e2eb7c53902a6fe52","datavalue":{"value":{"entity-type":"item","numeric-id":3685233,"id":"Q3685233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc85e628033c8b3edbe4bca62b5a55aad856b7a1","datavalue":{"value":{"amount":"+0.8794301","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$8EEE4502-B31D-472E-91EB-EB4783464B44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"703d0f40850fe4355ed51fd844ce2e4638f0c6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4730771,"id":"Q4730771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18736cca25d3564823e57241860714839eb9f80a","datavalue":{"value":{"amount":"+0.87848747","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$3BD412F1-816A-488C-90B4-C053B64189EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"224b22dc987944eaa77abf8f45eceaea25cde105","datavalue":{"value":{"entity-type":"item","numeric-id":2950044,"id":"Q2950044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc8adf67ab0732b066ffe858f5eb3d453a3ef1fd","datavalue":{"value":{"amount":"+0.87822545","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$284C75CB-AA7B-47ED-BF4B-3F594DB081C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa9ee196048636048be4a709ecfab57184cbee98","datavalue":{"value":{"entity-type":"item","numeric-id":1354049,"id":"Q1354049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f229886d47b65f2d3711e0c0eb7cc73f3aef66fe","datavalue":{"value":{"amount":"+0.8780743","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4373335$412DD246-5D56-4C3F-99E3-7F554DBF38A4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d30aee3716d499caeddf04c903f7cdf275887709","datavalue":{"value":"How did computers influence mathematicians? The answer depends on what we mean by mathematicians. The word ``mathematician'' has (at least) two radically different meanings. The meaning most familiar to the readers of Zentralblatt is a person who professionally proves theorems; his/her main output is a proof, i.e., something which is absolutely correct (unless there is a typo, or ZF is inconsistent, or, what sometimes happens, the author produced an \\textit{idea} of the proof without bothering to produce the actual proof). Such mathematicians use computers mainly for typing in the papers and very rarely -- for the actual computer-aided proofs. The all-time number of successful computer-aided proofs is still under 100; these proofs do not (do not yet?) constitute a major trend. There is, however, a different, more applied meaning of the word ``mathematician'': a person who tries to find solutions to applied problems formulated in purely mathematical terms; if possible, this person tries to find a solution with a proof, but since this is often impossible, a heuristic solution, without a proof, is better than nothing. For example, if a physics-motivated partial differential equation turns out to be too complicated to be solved by using some known and proven technique, a natural idea is to try some (heuristic) numerical or asymptotic methods, even when there is no proof that these methods converge (and even if there are examples that sometimes, these methods diverge). In this activity, computers have really brought in a revolution. It used to be that since manually we can only check few examples, so heuristic methods were not very reliable, and proven methods were definitely more welcome by the user. With the computers, the situation has drastically changed. To check a heuristic method, we can now test thousands of examples and thus, get a feeling of how frequently the method works well. To get more confident that a (sometimes diverging) heuristic method really converges in the given example, we can use the computer to run many iterations and observe that the errors really go down, etc. Because of the possibility to run an enormous number of numerical examples and to test a huge amount of different techniques, heuristic methods have become much more reliable, to the extent that many users (engineers, scientists, etc.) no longer feel the need for proof-based mathematics. The number of proofs taught to engineering majors is (often) going down (if any proofs are left at all), the financial support for mathematical research is diminishing and computer-based heuristic methods are supported instead. Moreover, many people from outside the mathematical community no longer see the difference between the traditional (proof-based) mathematics and application-oriented heuristic mathematics. The paper under review seems to be one of such papers. The first part of the paper, in which the author claims that computers have revolutionized professional mathematicians, seems to hint at this type of confusion. The author is right in saying that, say, Mathematica is advertised as a system for ``doing math on a computer'', but this rather means doing routine math steps important in \\textit{applications} rather than doing mathematical \\textit{research} (i.e., proving theorems). The author, however, seems to imply that this revolution is applicable to proving theorems as well. He claims, on p. 634, that a proof is never correct, it just has not yet been refuted just like a physical theory like relativity theory can never be proven correct, it can only be not refuted yet. Well, every student with a degree in pure math has to learn quite a few proofs which he/she has to trace down to the basics. I would be very surprised if it turns out that, say, the so-called main theorem of algebra (that every polynomial has a complex zero) or a mean value theorem or any other textbook proof turns out to be incorrect, but this is exactly what the author seems to imply. (Of course, some papers contain raw ideas and not proofs, and as we all know, sometimes there is a gap and a result turns out to be wrong; in this, I have no disagreement with the author.) The above-mentioned ``negative'' parts clearly caused by confusion may attract the most of the mathematical reader's attention, but a reader should not overlook a very interesting ``positive'' part: namely, the author suggests that situation calculus, one of the formalisms invented in Artificial Intelligence to describe common sense reasoning in formal (and thus computer-understandable) terms, can be usefully applied to describe the way mathematicians come to their proofs, and the way they teach these proofs. Hopefully, if this idea really becomes successful, computers equipped with AI techniques will be truly helpful in understanding how we do math and maybe even in helping us to do it.","type":"string"},"datatype":"string"},"type":"statement","id":"Q4373335$74BFAC95-ECB0-43FC-8E86-30BC75F83747","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Logical Structure of Computer-Aided Mathematical Reasoning","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Logical_Structure_of_Computer-Aided_Mathematical_Reasoning"}}}}}