Part IX · Horizons Chapter 60 of 60
The frontier
The course ends where the answers end. A map of the unknown: the Millennium Problems, the Collatz conjecture, P versus NP; how mathematics is done today, together, with computers, Lean and AI; and a return to the seven questions we started with.
Builds on: 59 · Chaos and fractals
You will learn
- which problems mathematics hasn’t solved yet, and why they are so hard to solve
- what the classes P and NP are, and why “easy to check” doesn’t mean “easy to find”
- how proofs are checked today: computer searches, systems like Lean, and artificial intelligence
The last chapter ended with a question nobody can answer: is the Mandelbrot set connected “in the small”? You can draw the picture to any precision you like, but there’s no proof. This whole chapter is made of places like that, the edge of the map beyond which the unknown begins.
The course began with a rope round the Earth and with Euler’s formula, which produced primes forty times in a row and then broke on the forty-first. From it we took the main rule of mathematics: however many examples confirm a pattern, that is still not a proof. Now, at the end, the rule shows its full force. Below are conjectures checked on billions of billions of examples and still unproved, conjectures that held out for decades and then collapsed, and proofs that are no longer checked by people alone.
The chapter is laid out as a map of the unknown: first the map itself, then three expeditions to its edge — to a problem a ten-year-old can understand, to the question of which is easier, finding or checking, and to seven problems worth a million each. Then comes how mathematicians work today. And at the end we’ll return to the seven questions from the first chapter and to the map of the whole course.
The edge of the map
An open problem is a statement that nobody has managed either to prove or to disprove. We met some along the way: Goldbach’s conjecture in the chapter on primes, the Riemann hypothesis in chapter 44, the continuum hypothesis in chapter 52 (which, as it turned out, is a special case). Mathematicians are good not only at solving problems but at posing them, and some lists of problems have become historic events.
On 8 August 1900, at the International Congress of Mathematicians in Paris, David Hilbert gave a talk on the problems the new century would inherit. In the talk itself he had time for ten; the printed text has 23. They met very different fates. The third, on cutting up polyhedra, was solved that same year by his student Max Dehn (chapter 20). The seventh, on the transcendence of numbers like $2^{\sqrt 2}$, fell to Alexander Gelfond and Theodor Schneider in 1934–1935. The tenth fell to Yuri Matiyasevich in 1970, and the answer turned out to be negative (chapter 56). The first, the continuum hypothesis, can be neither proved nor disproved from the usual axioms. And the eighth, which includes the Riemann hypothesis, is open to this day.
A hundred years later, on 24 May 2000, the Clay Mathematics Institute announced the seven Millennium Prize Problems in Paris and put a million dollars on each. The rules are strict: a solution must appear in a peer-reviewed journal, at least two years must pass, and it must be accepted by specialists; only then does the institute begin to consider it.
Compare the slider at 1900 and at 2026. Most of the islands appeared in the second half of the twentieth century, and their stories repeat the same three plots again and again. A problem is solved by a new theory built for something else entirely, as modular forms were for Fermat’s Last Theorem. A problem is solved by a computer that works through a huge number of cases, as with the four colour problem. Or the problem turns out not to be what it seemed: the conjecture is refuted by an example nobody thought to look for.
A problem for a ten-year-old
Take any positive integer. If it’s even, halve it; if it’s odd, multiply it by 3 and add 1. Do the same with the result, and so on. Six gives $6 \to 3 \to 10 \to 5 \to 16 \to 8 \to 4 \to 2 \to 1$, and after that comes the cycle $1 \to 4 \to 2 \to 1$. The German mathematician Lothar Collatz came up with this game in 1937 and asked: does it always reach 1?
The number 27 takes 111 steps and climbs as high as 9232 on the way, while 97, though bigger, takes 118 and rises to the same peak. Among the numbers below a million, the longest journey belongs to 837,799: 524 steps, with a peak of almost three billion. The second tab shows that the number of steps jumps about erratically from one number to the next, and yet the cloud of points is layered into bands. Nobody can fully explain those bands.
How many steps does 7 need to reach 1?
$7 \to 22 \to 11 \to 34 \to 17 \to 52 \to 26 \to 13 \to 40 \to 20 \to 10 \to 5 \to 16 \to 8 \to 4 \to 2 \to 1$: 16 steps. On the way the number rises to 52.
Computers have checked the conjecture for every number up to $2^{71} \approx 2.36 \cdot 10^{21}$: the Czech researcher David Barina set this record in January 2025. Following every number honestly all the way down to 1 would take too long. The checkers rely on a simple observation, and it’s worth proving: it shows how mathematics turns an infinite check into a finite one.
(a) If for every $n$ from 2 to $N$ the trajectory of $n$ at some point drops below $n$, then all the numbers from 1 to $N$ reach 1. (b) An even $n$ drops below itself in one step, and $n = 4k + 1$ with $k \ge 1$ does so in three. So only numbers of the form $4k + 3$ need checking.
The idea: instead of following each number down to 1, follow it only to the first smaller number. From there its fate is already known.
So why is there no proof? An odd step multiplies by about 3, and the even step that always follows it halves the result, so together they multiply by about $\frac32$; any other even step simply halves. If after each such move the number came out odd or even like heads and tails, then on average a pair of moves would multiply it by $\frac32 \cdot \frac12 = \frac34$, and it would fall fast. This “probabilistic” picture explains why the conjecture looks true, but it proves nothing: the trajectory of a single number is not a coin. Terence Tao has come closest. In 2019 he proved that almost all trajectories, in the precise sense of logarithmic density, drop below any bound that grows, however slowly — below $\log\log\log\log n$, for example. Almost all doesn’t mean all. There’s a worrying sign too: in 1972 John Conway showed that for some similar rules, where “halve it” and “$3n + 1$” are replaced by other linear functions chosen by the remainder, the question “will this number reach 1?” is algorithmically undecidable, in the spirit of the halting problem. Paul Erdős is said to have remarked of the Collatz problem that mathematics may not be ready for such problems.
Easy to check, hard to find
Here’s a game for a couple of minutes. You’re given some numbers and a target. Pick some of them so that their sum is exactly the target.
If someone hands you a solution, checking it is easy: add up a few numbers. But finding one yourself is hard. $n$ numbers have $2^n$ subsets (chapter 45), and every new number doubles that. Even a computer checking a billion subsets a second soon gives up.
| Numbers $n$ | Subsets $2^n$ | Brute force at $10^9$ per second |
|---|---|---|
| 20 | $\approx 10^6$ | a thousandth of a second |
| 40 | $\approx 1.1 \cdot 10^{12}$ | 18 minutes |
| 50 | $\approx 1.1 \cdot 10^{15}$ | 13 days |
| 60 | $\approx 1.2 \cdot 10^{18}$ | 36 years |
| 100 | $\approx 1.3 \cdot 10^{30}$ | $4 \cdot 10^{13}$ years, three thousand times the age of the Universe |
Brute force isn’t the only way. There’s a trick that takes half off the exponent.
The subset sum problem for $n$ numbers can be solved in about $n \cdot 2^{n/2}$ operations.
Split the numbers into two halves of $\frac n2$ each. Write out all the subset sums of the first half — there are $2^{n/2}$ of them — and do the same for the second. Sort the second list; this takes on the order of $2^{n/2} \cdot \frac n2$ comparisons. Now, for each sum $s$ in the first list, look in the sorted second list for the number $T - s$, where $T$ is the target. Binary search, which halves the interval each time, finds it or confirms that it isn’t there in $\log_2 2^{n/2} = \frac n2$ comparisons. Altogether that’s on the order of $n \cdot 2^{n/2}$ operations. Why it’s correct: any subset of all the numbers splits in exactly one way into a part from the first half and a part from the second, and its sum equals $T$ exactly when the first part sums to some $s$ and the second to $T - s$. So if a solution exists, the search will find it, and if the search finds nothing, there is no solution.
For a hundred numbers that’s $100 \cdot 2^{50} \approx 10^{17}$ operations instead of $10^{30}$: ten trillion times less work, but at a billion operations a second it still takes several years. Nobody knows a method that would handle the problem in a time growing with $n$ like a polynomial rather than an exponential. And nobody has proved that no such method exists. That is the famous question.
A problem is said to be solvable in polynomial time if there is an algorithm whose number of steps on an input of length $n$ is at most $Cn^k$ for some constants $C$ and $k$. The class P consists of yes-or-no problems that can be solved in polynomial time. The class NP consists of problems in which a “yes” can be backed up by a hint (computer scientists call it a certificate), and the hint can be checked in polynomial time. For subset sum, the hint is the set of numbers itself.
Every problem in P lies in NP: no hint is needed, you can just solve it. The question is the converse: are the classes equal, is $\mathrm P = \mathrm{NP}$? Stephen Cook posed it in 1971, and Leonid Levin in the USSR arrived at the same thing independently. But the first to think about it seems to have been Kurt Gödel: in a letter to John von Neumann dated 20 March 1956 he asked whether proofs of theorems could be found in a time growing like $n$ or $n^2$ in their length, and remarked that the creative work of a mathematician could then be entirely replaced by a machine.
Cook and Levin’s main discovery is that NP contains hardest problems: solve one of them quickly, and they can all be solved quickly.
A problem in NP is called NP-complete if every problem in NP can be reduced to it in polynomial time: any input of that problem can be rewritten as an input of this one so that the answers agree.
The satisfiability problem for a logical formula — can the variables be assigned the values “true” and “false” so that the formula comes out true? — is NP-complete.
The proof needs a precise definition of an algorithm via Turing machines (chapter 56) and takes several pages, so here we’ll accept the theorem without proof. The idea is this. A problem in NP is a checking machine that reads the input and the hint in a polynomial number of steps. The machine’s entire run, cell by cell of the tape and step by step, can be written down as a formula of polynomial size: the variables say which symbol sits in which cell at which moment, and the formula demands that every step obey the program and that at the end the machine says “yes”. A hint the machine will accept exists exactly when the formula is satisfiable. A full proof can be found, for example, in Michael Sipser’s textbook “Introduction to the Theory of Computation”.
In 1972 Richard Karp showed that 21 famous problems are NP-complete, among them the knapsack problem, of which our subset sum is a special case, colouring a graph with a given number of colours (chapter 46), and finding a Hamiltonian cycle. Thousands of others have joined them since, from timetabling to sudoku of arbitrary size. They are all one problem in different costumes: find a fast algorithm for any of them, and $\mathrm P = \mathrm{NP}$.
Suppose that tomorrow someone proves $\mathrm P \ne \mathrm{NP}$. Would that make the RSA cipher provably secure?
Factoring lies in NP, but experts don’t believe it’s NP-complete: it has a special structure. So it could turn out to be easy even if $\mathrm P \ne \mathrm{NP}$. That’s why the security of the ciphers in chapter 41 rests not on theorems but on the fact that nobody has found a fast method. In the other direction there is a link: if $\mathrm P = \mathrm{NP}$ and the fast algorithm were practical, all of public-key cryptography would fall.
Seven million-dollar problems
P versus NP is one of the seven Millennium Problems. Here are all seven, with their status as of September 2026.
| Problem | Origin | Status |
|---|---|---|
| P versus NP | Cook, 1971 | open |
| The Riemann hypothesis | Riemann, 1859 | open |
| The Navier–Stokes equations | Leray, 1934 | a solution of one version claimed, being checked |
| Yang–Mills and the mass gap | physics from 1954 | open |
| The Hodge conjecture | Hodge, 1950 | open |
| The Birch and Swinnerton-Dyer conjecture | 1960s | open |
| The Poincaré conjecture | Poincaré, 1904 | proved by Perelman |
The Riemann hypothesis. In chapter 44 we saw that the primes are distributed almost as if at random, and that how accurate the law of their distribution is depends on the zeros of the zeta function. The hypothesis says that all the non-trivial zeros lie on the line $\operatorname{Re} s = \frac12$, which means the error in the law is no bigger than for honest randomness. In 2021 David Platt and Timothy Trudgian rigorously verified it for all zeros up to height $3 \cdot 10^{12}$, more than twelve trillion zeros. Hundreds of theorems proved in the form “if the hypothesis is true, then…” rest on the Riemann hypothesis.
The Navier–Stokes equations (Navier, 1822; Stokes, 1845) describe the motion of a viscous fluid: water in a pipe, air around a wing. Physicists and engineers solve them on computers every day, but mathematics doesn’t know whether the three-dimensional equations always have a smooth solution, or whether a fluid can reach a state of infinite speed in finite time, can “blow up”. The Clay formulation, written by Charles Fefferman, accepts either outcome: a proof of smoothness or an example of blow-up, including one with a smooth external force. On 8 September 2026 OpenAI announced that its system of many AI models working together had found a proof of exactly such a blow-up, with a specially constructed external force, and had checked it in Lean. The work builds on an approach developed earlier by Diego Córdoba and Luis Martínez-Zoroa; a day before OpenAI, Tristan Buckmaster and Levent Alpöge announced similar results for related equations. The Clay Institute called the problem apparently solved, but will consider it without haste, as its rules require. The question physicists care about most, whether a fluid can blow up with no external force at all, remains open. By the time you read this, the picture may have become clearer.
Yang–Mills and the mass gap. Yang–Mills quantum field theory (1954) underlies the Standard Model of particle physics and is superbly confirmed by experiment. But there is no rigorous mathematical theory of such fields in four-dimensional spacetime. The problem was formulated by Arthur Jaffe and Edward Witten: build such a theory and prove that its particles have a smallest positive mass.
The Hodge conjecture is about higher-dimensional spaces defined by polynomials. It says that certain topological “shapes” in them, the Hodge classes, can always be assembled from pieces that are also defined by polynomials. It’s a question of how much of topology algebra can see.
The Birch and Swinnerton-Dyer conjecture is about the elliptic curves of chapter 44. According to the conjecture, whether a curve has infinitely many rational points, and “how many”, can be read off from its zeta function at the point $s = 1$. Bryan Birch and Peter Swinnerton-Dyer arrived at it in the early 1960s by counting points on one of the first computers, EDSAC 2 in Cambridge. In the simplest cases, when the curve’s zeta function vanishes at $s = 1$ to order at most one, the conjecture is proved (Gross and Zagier, 1986; Kolyvagin, 1989).
The Poincaré conjecture is the only one solved. Every closed three-dimensional manifold in which any loop can be shrunk to a point is the three-sphere (chapter 57). Grigori Perelman posted his proof in 2002–2003, then declined the Fields Medal in 2006 and the Clay prize in 2010.
How mathematicians work today
The image of the lone genius at a desk is only half true. Perelman really did work alone, and Andrew Wiles spent seven years proving Fermat’s theorem in secret. But more and more problems are solved together, and not only with other people.
Together
In January 2009 Timothy Gowers asked on his blog whether “massively collaborative” mathematics was possible, and proposed a problem. Dozens of people discussed it in the comments, and within six weeks they had found a new proof of the density Hales–Jewett theorem; the paper was signed with the collective pseudonym D. H. J. Polymath. In 2013 Yitang Zhang proved that there are infinitely many pairs of primes at most 70 million apart. The Polymath project, together with ideas of James Maynard, brought 70 million down to 246 (chapter 3). Nobody has yet got all the way down to 2, which would be the twin prime conjecture.
With a computer
In 1976 Kenneth Appel and Wolfgang Haken proved the four colour theorem (chapter 46) by reducing it to a check of almost two thousand configurations, which a computer carried out in more than a thousand hours. Many mathematicians were unhappy: a proof that couldn’t be read didn’t seem quite like a proof. In 1998 Thomas Hales proved the Kepler conjecture on the densest packing of spheres, again with a huge search; after several years of work the journal’s referees wrote that they were $99\,\%$ certain it was correct. We’ve seen such proofs in this course too: the Feigenbaum constant and the Lorenz attractor in chapter 59, the fifth busy beaver in chapter 56.
With a program that checks
The answer to these doubts was programs that check proofs completely, all the way from the axioms. The proof is written in a special language so that every step is an application of a rule of logic or of an already-checked theorem, and the program accepts it only if every step is legitimate.
A proof assistant is a program that accepts a proof written in a formal language only if every step follows legitimately from the axioms and from statements already checked. The best known are Coq (now Rocq), Isabelle and Lean.
Here’s what it looks like in miniature. Numbers are built from zero and the “next number” operation $\mathrm S$, as in the Peano axioms (chapter 56): $1 = \mathrm S(0)$, $2 = \mathrm S(\mathrm S(0))$. Addition is defined by two rules. Let’s prove that $2 + 2 = 4$.
Four steps for $2 + 2 = 4$ look comical, but that’s how every formal check works: big theorems are made of thousands of lemmas, lemmas are made of steps like these, and the machine checks every one. It won’t accept a false statement, however hard you try. The only mistake left is in how the statement is written down: the machine proves exactly what is written, so it’s up to people to check that what is written is what they meant.
Leonardo de Moura started Lean at Microsoft Research in 2013. The mathematical community has built a library for it, mathlib, which already holds hundreds of thousands of formally verified definitions and theorems. In December 2020 Peter Scholze, a Fields medallist, proposed checking in Lean the main theorem of the new theory he had built with Dustin Clausen, a theorem he wasn’t fully sure of himself. The “Liquid Tensor Experiment” was completed in July 2022: the theorem is true. In 2024 Kevin Buzzard started a five-year project to formalise the proof of Fermat’s Last Theorem. And in September 2026 Anthropic reported that its model Claude had built, in 11 days and almost on its own, the first complete computer-verified proof of Fermat’s theorem: about 13 million lines of Lean and nearly thirty thousand intermediate theorems. It follows the historical route of Wiles and Taylor rather than the updated path Buzzard’s project is laying, but it couldn’t have been done without that project’s groundwork or without mathlib. Buzzard compiled the code himself and checked it: Fermat’s theorem is derived from the standard axioms alone.
With artificial intelligence
Back in 2024 Google DeepMind’s systems AlphaProof and AlphaGeometry 2 scored 28 points out of 42 on the problems of the International Mathematical Olympiad, silver-medal level. People translated the problems into Lean for them, and some problems took the systems days. In July 2025 the Gemini Deep Think model solved five of that year’s six olympiad problems in ordinary language, within the official four and a half hours, and the olympiad’s coordinators officially graded the solutions at 35 points, gold-medal level. An experimental OpenAI model achieved the same score, as graded by former medallists.
Olympiad problems come with known solutions; research problems don’t. In 2025–2026 AI systems helped settle a number of problems from Paul Erdős’s collection: sometimes by finding a forgotten solution in the literature, sometimes with a new proof, which people and programs like Lean then checked. In May 2026 an OpenAI model disproved Erdős’s 1946 conjecture on unit distances: Erdős believed that among $n$ points in the plane only slightly more than $n$ pairs can be exactly 1 apart, and the model found arrangements with about $n^{1 + c}$ such pairs for a constant $c > 0$. Then came September 2026 and the claim on the Navier–Stokes Millennium problem.
Mathematicians themselves are arguing over what this means for mathematics. Terence Tao at first called the new blow-up results a remarkable achievement, but soon added that OpenAI’s method doesn’t carry over to analytic, that is “natural”, external forces, and that AI may change mathematics not only for the better. Many are worried about something else as well: answers may start arriving before people have had time to draw out of the problems the methods and understanding that are usually born on the way to the answer. A proof is not only a certificate of truth but also an explanation of why something is true. Asking which questions are interesting, and understanding the answers, is still up to people.
Discovered yesterday
Besides the loud debates, the frontier has quiet victories that have already been verified. Here are a few from recent years.
In 2016 Maryna Viazovska proved that in eight-dimensional space balls are packed most densely by the $E_8$ lattice, and a few days later, together with Henry Cohn, Abhinav Kumar, Stephen Miller and Danylo Radchenko, that in 24 dimensions the best packing comes from the Leech lattice. In three-dimensional space the same problem, the Kepler conjecture, needed a computer and hundreds of pages; in dimensions 8 and 24 Viazovska found a short and beautiful proof using modular forms. In 2022 she became the second woman to win the Fields Medal.
In 2024 a group led by Dennis Gaitsgory and Sam Raskin posted a proof of the geometric Langlands conjecture: five papers running to almost a thousand pages. It is one of the cornerstones of the Langlands programme, a vast web of conjectures connecting number theory, symmetry and analysis.
In February 2025 Hong Wang and Joshua Zahl proved the Kakeya conjecture in three-dimensional space. A set containing a segment of length 1 in every direction can have zero volume — Abram Besicovitch showed this back in the 1920s — but we now know that its dimension is still three: such a set can’t be “thinner” than a solid. In 2026 Hong Wang was awarded the Fields Medal, together with Yu Deng, John Pardon and Jacob Tsimerman.
And in October 2024 Nikita Gladkov, Igor Pak and Aleksandr Zimin disproved the bunkbed conjecture (Pieter Kasteleyn, 1985). It was about random paths in a graph and seemed so obvious that people tried to prove it for almost forty years. The counterexample is a graph with 7222 vertices, and the violation is about $10^{-6500}$: no experiment would ever have noticed it. It’s the same moral as Euler’s formula from the first chapter, only with six and a half thousand zeros after the decimal point.
Seven answers
In the first chapter we asked seven questions. They sounded almost childish, but answering them took the whole course. Here they are together.
The rule of signs is not a convention. If negative numbers obey the distributive law, there is no other way: from $0 = (-1)\bigl(1 + (-1)\bigr) = -1 + (-1)(-1)$ it follows that $(-1)(-1) = 1$ (chapter 2). In the plane, multiplying by $-1$ is a turn through $180^\circ$, and two such turns make a full revolution (chapter 15).
With scissors, no, not even cutting along curves (chapter 20). Nor can you construct a square equal to the disc with compass and straightedge: $\pi$ is transcendental (chapter 6, chapter 43). But you can cut the disc into finitely many pieces that no scissors could cut out and assemble a square from them by translations alone: Laczkovich, 1990, about $10^{50}$ pieces (chapter 54).
There is no formula in radicals for the equation of degree five: Abel proved it in 1824, and Galois explained why. The permutations of the five roots are “tangled” in a way that no finite number of storeys of radicals can untangle (chapter 14, chapter 43).
A segment has more points: the natural numbers form a countable set, the points of a segment form the continuum, and Cantor’s diagonal always finds a point left without a number (chapter 52). Whether there’s anything in between is a question the usual axioms don’t settle.
A cipher rests on operations that are easy to perform and, as far as anyone knows, hard to reverse: modular exponentiation versus factoring and the discrete logarithm (chapter 41), multiplying a point on an elliptic curve versus the logarithm on the curve (chapter 44). “As far as anyone knows” isn’t a figure of speech: nobody has proved that reversing them is hard, and the question runs into problems of the same kind as P versus NP.
The equations of the atmosphere are deterministic but chaotic: small measurement errors grow exponentially, and each new correct digit extends the forecast only by a fixed amount of time. And because of motions on every scale, the limit of about two weeks can’t be pushed back by any amount of accuracy (chapter 31, chapter 59).
Yes. In any consistent system of axioms that can be written out mechanically and contains arithmetic, there are statements about numbers that are true but can’t be proved in it (Gödel, 1931; chapter 56). Unprovability is relative to the system of axioms: a new axiom closes the old gap and opens a new one.
End of the line
On the main page the course is drawn as a metro map: ten lines, 61 stations, and interchanges wherever an idea from one part works in another. Here is the same map one last time, with everything you’ve read. The Frontier station is the end of the course but not of the lines: the tracks go on into areas a textbook can no longer hold.
Mathematics is not a collection of ready-made answers but a way of getting answers you can be sure of. Everything in this course rests on proofs, and at the edge of the map you can see how they are found: through examples that give hints, counterexamples that sober you up, and arguments that make the answer final.
Further reading
If you’ve enjoyed the course, here’s where to go next. The books are for different levels, and all of them are available in English.
- Richard Courant and Herbert Robbins, “What Is Mathematics?”, the classic this course took as its model.
- Martin Gardner, “Mathematical Puzzles and Diversions”, and Yakov Perelman, “Mathematics Can Be Fun”, to keep things light.
- Vladimir Arnold, “Problems for Children from 5 to 15” (in English it’s part of “Lectures and Problems: A Gift to Young Mathematicians”): short problems that grown-ups think hard about too.
- Ian Stewart, “The Great Mathematical Problems” (in the US, “Visions of Infinity”): open and recently solved problems, told accessibly and accurately.
- Simon Singh, “Fermat’s Last Theorem”, and John Derbyshire, “Prime Obsession”: the stories of Fermat’s theorem and the Riemann hypothesis.
- James Gleick, “Chaos: Making a New Science”, and Benoit Mandelbrot, “The Fractal Geometry of Nature”, for chapter 59.
- Douglas Hofstadter, “Gödel, Escher, Bach: An Eternal Golden Braid”, for chapter 56.
- Steven Strogatz, “Nonlinear Dynamics and Chaos”, and “The Princeton Companion to Mathematics”, edited by Timothy Gowers: the first is a university textbook, the second an encyclopedia of all of modern mathematics written by mathematicians themselves.
- The Natural Number Game (Kevin Buzzard and co-authors) and Mathematics in Lean (Jeremy Avigad and Patrick Massot): free online courses in which addition is proved from the Peano axioms in Lean, just as in the widget above.
- The 3Blue1Brown videos for the eyes, and Quanta Magazine for news from the frontier.
Where next
There’s no next chapter: this is the last one. But the course doesn’t end here. In the topic catalogue you can pick chapters by topic and level and go through the course again by a different route, for instance only through proofs or only through applications. The solvers will take your own problem apart step by step, from a quadratic equation and a derivative to the eigenvalues of a matrix. The trainers, like the subset sum one in this chapter, invent problems endlessly and accept an answer in any correct form. And if you’d like to start again, the first chapter is waiting with the same question: how far does a rope round the Earth rise if you make it a metre longer? Now you know not only the answer but also that behind it stands the whole of mathematics: notice, doubt and prove.