Digital thinking tools for better decision making
Digital thinking tools for better decision making

Start this free course now. Just create an account and sign in. Enrol and complete the course for a free statement of participation or digital badge if available.

Free course

Digital thinking tools for better decision making

2.2 Computers as tools for mathematicians

Working mathematicians continued their labours and were relatively unfazed by Gödel’s and Turing’s findings. If anything, they were reassured that computers wouldn’t put them out of a job anytime soon.

With the rise of computing technology, some forays were made into turning computers into the mathematician’s assistant or tool. Whereas there is no general computer program for telling whether mathematical statements are true, there are relatively simple programs that can check whether a proof of a statement is correct. In other words, although computers can’t come up with a proof for any arbitrary statement, they can tell us whether a proof, once found, has no missing or incorrect steps.

An early example is the Automath project by Dick de Bruijn (1918–2012) and his research group at Eindhoven University of Technology in the Netherlands. In the 1960s, the Automath team checked the proofs in a classic textbook on the foundations of analysis (Landau’s Grundlagen der Analysis) – see Figure 9. Several years of labour went into translating the textbook content into precise statements that could be processed by a computer. Along the way several mistakes and gaps in the original ‘proofs’ were discovered and corrected.

The Automath team using a computer to check the final proof of Landau’s mathematics textbook.
Figure 9 The Automath team using a computer to check the final proof of Landau’s mathematics textbook, followed by celebrations with two team members holding a print-out of the final proof.

Automath pioneered the idea that computers can play a useful role in assisting, rather than replacing, mathematicians. The need for such tools has become increasingly pressing as some of the most influential mathematical proofs can take over a hundred pages of dense mathematical reasoning.

A dramatic example is the famous proof by Andrew Wiles (born 1953) of Fermat’s last theorem. The initial proof of well over a hundred pages contained a mistake that was discovered only after Wiles had announced his proof in public. Wiles succeeded in correcting the proof and no further issues have been reported since.

Some mathematicians have warmed to using proof checkers to verify mathematical results, despite the enormous amount of work that is involved in translating a human-authored proof to computer input. For instance, after six years, in 2012, a team from Inria (the French national research institute for the digital sciences) and Microsoft Research completed checking a significant mathematical theorem, the Feit–Thompson theorem (Breton, 2012).


Take your learning further

Making the decision to study can be a big step, which is why you'll want a trusted University. The Open University has 50 years’ experience delivering flexible learning and 170,000 students are studying with us right now. Take a look at all Open University courses.

If you are new to University-level study, we offer two introductory routes to our qualifications. You could either choose to start with an Access module, or a module which allows you to count your previous learning towards an Open University qualification. Read our guide on Where to take your learning next for more information.

Not ready for formal University study? Then browse over 1000 free courses on OpenLearn and sign up to our newsletter to hear about new free courses as they are released.

Every year, thousands of students decide to study with The Open University. With over 120 qualifications, we’ve got the right course for you.

Request an Open University prospectus371