Present day mathematics is a human construct, where computers are used more and more but do not play a creative role.

It always seemed very strange to me how, despite the obvious similarities and overlaps between mathematics and computer science, the use of computers for mathematics has largely been a fringe movement and mathematicians mostly still do mathematics the way it was done in the 19th century. This even though precision and accuracy is highly valued in mathematics and decades of experience in computer science has shown us just how prone humans are to making mistakes in programs, proofs, etc. and just how stubbornly these mistakes can evade the eyes of proof-checkers.

Showing 3 of 5 replies (Click to show all)

People are working on changing that (at CMU for example).

4Sarunas5yCorrectness is essential, but another highly desirable property of a mathematical proof is its insightfulness, that is, whether they contain interesting and novel ideas that can later be reused in others' work (often they are regarded as more important than a theorem itself). These others are humans and they desire, let's call it, "human-style" insights. Perhaps if we had AIs that "desired" "computer-style" insights, some people (and AIs) would write their papers to provide them and investigate problems that are most likely to lead to them. Proofs that involve computers are often criticized for being uninsightful. Proofs that involve steps that require use of computers (as opposed to formal proofs that employ proof assistants) are sometimes also criticized for not being human verifiable, because while both humans make mistakes and computer software can contain bugs, mathematicians sometimes can use their intuition and sanity checks to find the former, but not necessarily the latter. Mathematical intuition is developed by working in an area for a long time and being exposed to various insights, heuristics, ideas (mentioned in a first paragraph). Thus not only computer based proofs are harder to verify, but also if an area relies on a lot of non human verifiable proofs that means it might be significantly harder to develop an intuition in that area which might then make it harder for humans to create new mathematical ideas. It is probably easier understand the landscape of ideas that were created to be human understandable. That is neither to say that computers have little place in mathematics (they do, they can be used for formal proofs, generating conjectures or gathering evidence for what approach to use to solve a problem), nor it is to say that computers will never make human mathematicians obsolete (perhaps they will become so good that humans will no longer be able to compete). However, it should be noted that some people [
2RichardKennaway5ySubstantial work has been done on this. The two major systems I know of are Automath [] (defunct but historically important) and Mizar [] (still alive). Looking at those articles just now also turns up Metamath []. Also of historical interest is QED [], which never really got started, but is apparently still inspiring enough that a 20-year anniversary workshop was held last year. Creating a medium for formally verified proofs is a frequently occurring idea, but no-one has yet brought such a project to completion. These systems are still used only to demonstrate that it can be done, but they are not used to write up new theorems.

Open thread, Nov. 23 - Nov. 29, 2015

by MrMind 1 min read23rd Nov 2015258 comments


If it's worth saying, but not worth its own post (even in Discussion), then it goes here.

Notes for future OT posters:

1. Please add the 'open_thread' tag.

2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)

3. Open Threads should be posted in Discussion, and not Main.

4. Open Threads should start on Monday, and end on Sunday.