TOK knowledge questions about mathematics

Technology, algorithms and AI: TOK knowledge questions

Computers now check proofs, find patterns in data and even suggest new results. These questions ask when we should trust a machine's mathematics, and what knowledge is lost or gained when we do.

Questions on this page

Each question has claims, counterclaims, real-life situations from mathematics and pointers for your essay and exhibition. Check dates and figures in a reliable source before you use them, and cite that source. Link a question to the prescribed title or exhibition prompt you are working on, in your own words: see using maths examples in your essay and choosing exhibition objects. The study headings (scope, perspectives, methods and tools, ethics) are our own.

Does a proof checked by software give us more certainty than a proof checked by people?

Knowledge and technology Methods and tools

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.

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.

The mathematics behind it

Can an algorithm be biased if it only follows mathematics?

Knowledge and technology Knowledge and politics Ethics

Algorithms decide what we see online, who gets loans and, in some places, who is released on bail. They are built from mathematics that looks neutral. This question asks where bias can enter, and who is responsible for it.

Claims

  • Algorithms apply the same rule to everyone and can be audited, so they can be fairer than human judgement, which is inconsistent and often biased.
  • Bias comes from data and design choices, not from the mathematics, so better data and checks can fix it.

Counterclaims

  • If an algorithm learns from past decisions that were unfair, it repeats that unfairness while appearing objective.
  • Different mathematical definitions of fairness can be impossible to satisfy at the same time, so someone must choose, and that choice is ethical, not mathematical.

Real-life situations from mathematics

COMPAS risk scores. In 2016 the news organisation ProPublica analysed a risk-scoring tool used in US courts and reported that it wrongly flagged Black defendants as high risk more often than white defendants. The tool's makers disputed the analysis, and the debate showed that different measures of fairness can conflict.

Exam grades in 2020. With exams cancelled in 2020, England's exams regulator used a statistical model to adjust teachers' predicted A level grades, and about four in ten were lowered. After protests the government reverted to teachers' grades. The IB also used a model for its May 2020 results and faced complaints from students and schools.

Use this in your TOK work

Essay. Very strong for titles about technology, ethics and objectivity. The 2020 exam grades are a personal and relevant example for IB students.

Exhibition. A screenshot of a recommendation feed or a results slip from 2020 is an object close to students' lives.

The mathematics behind it

If an AI system produces a correct proof, does anyone know the result?

Knowledge and technology Knowledge and the knower Methods and tools

AI systems have begun to solve competition problems and to suggest new constructions in research mathematics. This question asks where the knowledge sits when a machine finds a proof: in the machine, in the people who check it, or nowhere until someone understands it.

Claims

  • If the proof is checked, for example by a proof assistant, the result is known, whoever or whatever found it; discovery and justification are different things.
  • AI can widen what mathematicians can explore, just as computers did for calculation.

Counterclaims

  • Knowledge may require understanding; a verified result no human understands is closer to a reliable rumour than to mathematical knowledge.
  • AI systems can produce convincing but wrong arguments, so trusting them without independent checks is risky.

Real-life situations from mathematics

AI at the International Mathematical Olympiad. In July 2024 Google DeepMind reported that its AlphaProof and AlphaGeometry 2 systems together solved four of the six problems from that year's olympiad, a score at silver-medal level. AlphaProof's solutions were checked in the Lean proof assistant.

FunSearch and the cap set problem. In December 2023 researchers reported that FunSearch, a method combining a language model with an automatic evaluator, found larger examples of 'cap sets' in some dimensions than mathematicians had found before. The constructions could be checked directly.

Use this in your TOK work

Essay. Fits titles about technology, the knower, or what counts as understanding. Keep your facts dated: this area changes quickly.

Exhibition. A printout of an AI chatbot's (flawed or correct) attempt at a proof is a timely object; label it as AI output and comment on it.

The mathematics behind it

How far should we trust tools whose workings we cannot check?

Knowledge and technology Methods and tools

Students use calculators and software that give answers in an instant. Few users could explain how the device computes a sine or a square root. This question asks what kind of knowledge we have when we rely on such tools.

Claims

  • Calculators are tested and reliable, and relying on them is like relying on any expert source; it frees us to think about the problem.
  • We can check tools indirectly, by estimation or by comparing methods, so trust need not be blind.

Counterclaims

  • Hardware and software can contain errors, and people who cannot estimate cannot notice when a tool is wrong.
  • Relying on tools may change what we understand: knowing how to get an answer is not the same as knowing why it is right.

Real-life situations from mathematics

The Pentium division bug. In 1994 the mathematician Thomas Nicely noticed that some Intel Pentium processors gave slightly wrong answers to certain divisions. Intel eventually offered to replace the chips, at great cost.

Spreadsheet errors. Errors in spreadsheet formulas have affected business and research decisions. In 2020 a file format limit in a spreadsheet caused thousands of positive COVID-19 test results in England to be left out of daily figures for several days.

Use this in your TOK work

Essay. Fits titles about technology and knowledge, or about trust in sources.

Exhibition. Your own graphic display calculator is a natural, personal object for a technology prompt.

The mathematics behind it

Does big data make mathematical theory less necessary?

Knowledge and technology Methods and tools

With enough data, some argue, patterns speak for themselves and we no longer need models that explain them. This question asks whether prediction from data alone is knowledge, and what happens when the patterns change.

Claims

  • Large data sets reveal patterns no theory anticipated, and many useful systems, such as translation software, work well without a theory of why.
  • Prediction is what matters for many practical decisions, so if data predicts well, theory is optional.

Counterclaims

  • Patterns found without theory can fail suddenly when circumstances change, because nothing explains why they held.
  • Choosing what data to collect, and how to analyse it, already involves theory and assumptions.

Real-life situations from mathematics

'The end of theory'. In 2008 Chris Anderson, then editor of Wired magazine, argued that with enough data the scientific method of hypothesis and model would become obsolete. Many scientists and statisticians disagreed.

Google Flu Trends. Google Flu Trends estimated flu levels from search queries. It worked well at first, but in the 2012–13 season it greatly overestimated flu levels in the US, and the service was later closed.

Use this in your TOK work

Essay. Fits titles about explanation versus prediction, or about technology changing methods.

Exhibition. A fitness tracker's data summary is an everyday object for a prompt about how technology shapes knowledge.

The mathematics behind it

Other areas: Proof · Nature of maths · Infinity · Models · Statistics · The knower · Culture · Ethics · all 49 knowledge questions