Technology, algorithms and AI · Methods and tools
Does a proof checked by software give us more certainty than a proof checked by people?
Proof assistants such as Lean, Coq and Isabelle check each logical step of a proof written in a precise formal language. Some mathematicians now formalise major results this way. This question asks whether moving checking from people to software changes what it means to know a theorem.
Claims
- A proof assistant checks every step against explicit rules, so a formalised proof cannot contain the hidden gaps that human readers often miss.
- Formal checking lets a large community build on each other's results safely, because each piece is verified the same way.
Counterclaims
- The software checks that the formal statement is proved, but a human still has to judge that the formal statement means what the theorem means, so human judgement has not gone away.
- Formalisation can be slow and expensive, and proofs that are easy to check by machine may be hard for people to learn from.
Real-life situations from mathematics
The Liquid Tensor Experiment
In December 2020 Peter Scholze challenged the community to check a difficult result of his own in the Lean proof assistant, because he was not fully sure of it himself. A team led by Johan Commelin completed the formal check in July 2022.
Flyspeck
The project to formally verify Thomas Hales's proof of the Kepler conjecture finished in 2014, more than fifteen years after the original proof, turning a proof the referees could not fully check into one checked by machine.
Check dates and figures in a reliable source before you use them, and cite that source.
Use this in your TOK work
Essay. Fits titles about technology and knowledge, or about the role of the knower. Ask what the human still contributes.
Exhibition. A screenshot of a few lines of a formal proof next to the same argument in ordinary words could support a prompt about language or technology.
Link it to the prescribed title or the exhibition prompt you are working on, in your own words. See using maths examples in your essay and choosing exhibition objects.
Themes and study heading
Knowledge and technology Methods and tools
How mathematical knowledge is produced and justified.