KnowledgeInSight
What Mathematicians Do
0% of Course 5 complete

Module 3 · Lesson 2

Computation: Efficient algorithms, P versus NP, and computers that help prove theorems

You'll see why some problems are easy to check but appear hard to solve, and why a million-dollar prize hangs on whether that appearance is real. You'll then look at how computers have taken part in proof, from checking cases in 1976 to machine-verified proofs and AI systems in 2026.

What you will be able to do

  • Explain the P versus NP problem and describe how computers and AI systems now take part in mathematical proof.

0% of this lesson · 10 items · 1h 33m total · 1h 18m without the optional journal

Contents of this lesson10 items
  1. ReadingEasy to Check, Hard to Find3 min
  2. ReadingEfficient and Inefficient Algorithms: Why Growth Rates Matter4 min
  3. ReadingP Versus NP: The Million-Dollar Question About Hard Problems4 min
  4. ReadingComputer-Assisted Proof and Proof Assistants4 min
  5. ReadingAI Systems as Mathematical Collaborators: The 2026 Frontier4 min
  6. Guided ReadingGuided Walkthrough: Checking a Route Versus Finding the Best One7 min
  7. Guided ConversationWhat Would It Take for You to Believe a Proof?12 min
  8. Journal · optionalShould a Proof No Human Can Read Count?15 min
  9. Knowledge CheckEfficient algorithms, P versus NP, and computers that help prove theorems10 min
  10. Graded QuizComputation30 min

Report an issue on this page

Reading 3 min Done

Easy to Check, Hard to Find

The Clay Mathematics Institute introduces one of its prize problems with a housing puzzle. A university has 400 students who want dormitory places, and only 100 places. The dean has a list of pairs of students who mustn't both be chosen. Your job is to pick 100 students so that no flagged pair is among them (Clay Mathematics Institute n.d.-a).

Suppose a coworker hands you a proposed list of 100 names. Checking it is routine. Go through the dean's pairs one at a time and confirm that no pair has both students on the list. The institute calls this check easy (Clay Mathematics Institute n.d.-a). It takes one pass through the dean's list.

Now try to build a list yourself, from scratch. The direct approach is to try every possible group of 100 students and check each one. But the number of ways to choose 100 students from 400 is greater than the number of atoms in the known universe (Clay Mathematics Institute n.d.-a). No computer could get through them. Clever methods can help on particular lists, but the institute describes generating a list from scratch as seeming "so hard as to be completely impractical" (Clay Mathematics Institute n.d.-a).

The same gap shows up in familiar places:

  • A finished jigsaw puzzle is quick to check, and slow to assemble.
  • A completed sudoku grid can be checked in a minute, and can take far longer to fill in.
  • A proposed delivery route is easy to add up, and hard to prove the shortest.

Is the gap real? Or is there, for every problem like these, some clever method for finding answers that's nearly as fast as checking them, one that nobody has discovered yet? That's the question known as P versus NP. In the institute's shorthand, P stands for problems where answers are easy to find, and NP for problems where answers are easy to check (Clay Mathematics Institute n.d.-a). Every problem in P is also in NP, since you can check an answer by finding one yourself. The open question is whether the reverse holds.

The question is one of seven Millennium Prize Problems, with $1 million set aside for the solution of each (Clay Mathematics Institute n.d.-b). As of October 2026, it's unsolved.

What this area of mathematics offers is a precise way to say "hard." Saying a problem feels difficult isn't enough. Mathematicians measure how the number of steps needed to solve it grows as the problem gets bigger. That turns a hunch about difficulty into a question that can, in principle, be settled by proof.

This content reflects the field as of October 2026.

References

Reading 4 min Done

Efficient and Inefficient Algorithms: Why Growth Rates Matter

Introduction

A method that works in a second for 10 items can take longer than the age of the universe for 100. What decides which methods stay practical is how fast their work grows as the input grows. This reading compares growth rates, explains why computer scientists call some algorithms efficient and others impractical, and shows why faster hardware doesn't rescue the slow ones.

Comparing Growth

An algorithm's step count is the number of basic operations an algorithm carries out on a given input, used to measure its speed. Write n for the size of the input, such as the number of items to sort or cities to visit. The table compares three ways a step count can grow: like n itself, like n^2 (read "n squared," meaning n \times n), and like 2^n ("2 to the n," meaning 2 multiplied by itself n times).

Input size nnn^22^n
10101001,024
20204001,048,576
50502,500about 1.1 \times 10^{15}

At n = 10, the three columns are close enough not to matter. At n = 50, the last one has passed a thousand trillion. A computer doing a billion steps per second would finish n^2 steps for n = 50 in a few millionths of a second. It would need about 13 days for 2^{50} steps, and about 40 trillion years for 2^{100}.

Efficient and Impractical

An algorithm runs in polynomial time if its step count grows no faster than some fixed power of the input size, such as n^2 or n^3. It runs in exponential time if its step count grows like 2^n or faster, so that each additional item multiplies the work. Computer scientists treat polynomial time as the working definition of "efficient." Stephen Cook, writing for the Clay Mathematics Institute, notes that identifying polynomial time with feasible computation has become standard, while admitting it's an idealization: a method needing n^{100} steps would be useless in practice (Cook n.d.). Exponential-time methods, by contrast, become impractical once inputs grow even moderately large.

Brute Force and the Traveling Salesperson

A brute force method solves a problem by checking every possible answer. It always works in principle. The question is how many answers there are.

Take the traveling salesperson problem: given some cities and the distances between them, find the shortest round trip that visits each city once and returns home. Fix a starting city. With n cities, the remaining n - 1 can be visited in (n-1)! orders, where the exclamation mark, read "factorial," means multiplying all the whole numbers from 1 up to that number. Each round trip can be driven in either direction, so the number of distinct tours is (n-1)!/2.

For 10 cities, that's 181,440 tours, which a laptop can check almost instantly. For 20 cities, it's about 6 \times 10^{16}. At a billion tours per second, checking them all would take about two years. Each added city multiplies the count again: 21 cities would take about 39 years at the same rate.

Routing problems like this one have real industrial importance (Cook n.d.). Ask a yes-or-no version, "Is there a tour shorter than 1,000 kilometers?", and a proposed tour is easy to check: add up its distances. That puts the question in the family of easy-to-check problems at the center of the P versus NP question (Clay Mathematics Institute n.d.-a). Whether some method can find such tours efficiently, for every map, is part of what that question asks.

Why Faster Hardware Barely Helps

Suppose computers become 1,000 times faster. For a polynomial-time method that takes n^2 steps, the same hour now handles inputs about 30 times larger, since 30^2 is about 1,000. For a method that takes 2^n steps, the same hour handles inputs only about 10 items larger, since 2^{10} = 1,024. A thousandfold gain in speed buys ten more items.

That's why growth rates matter more than hardware. Improvements in machines shift the limits of an exponential method a little. A better algorithm, one with a slower-growing step count, can move them enormously.

Conclusion

Polynomial-time algorithms stay usable as inputs grow, and exponential-time ones don't. For a large family of important problems, no polynomial-time method is known. Whether one exists is one of the central open questions in mathematics.

This content reflects the field as of October 2026.

Key Terms

  • Step count: The number of basic operations an algorithm carries out on a given input, used to measure its speed.
  • Polynomial time: A step count that grows no faster than some fixed power of the input size, such as n^2; the usual working definition of "efficient."
  • Exponential time: A step count that grows like 2^n or faster, so that each additional item multiplies the work.
  • Brute force: Solving a problem by checking every possible answer.

References

  • Clay Mathematics Institute. n.d.-a. "P vs NP." Millennium Prize Problems. Accessed October 13, 2026.
  • Cook, Stephen. n.d. "The P Versus NP Problem." Official problem description, Millennium Prize Problems. Clay Mathematics Institute. Accessed October 13, 2026.

Reading 4 min Done

P Versus NP: The Million-Dollar Question About Hard Problems

Introduction

Many problems share an odd feature: if someone hands you an answer, you can check it quickly, but finding an answer yourself seems to take an enormous search. Nobody knows whether that difference is real or only reflects methods not yet discovered. This reading defines the classes P and NP in plain words, explains NP-complete problems, and describes why the question matters for encryption and why it remains open.

Two Classes of Problems

Complexity theory, the part of computer science that classifies problems by how much computation they need, sorts problems into classes. It usually works with yes-or-no questions, such as "Is there a choice of 100 students with no flagged pair?" or "Is there a round trip through these cities shorter than 1,000 kilometers?"

P is the class of yes-or-no problems that some algorithm can solve in polynomial time, meaning its step count grows no faster than a fixed power of the input size (Cook n.d.). These are the problems treated as efficiently solvable.

NP is the class of yes-or-no problems for which a proposed "yes" answer can be checked in polynomial time. The name stands for "nondeterministic polynomial time" (Cook n.d.). The housing and route questions are in NP. Hand someone a list of students, or a route, and they can confirm it quickly.

The Clay Mathematics Institute's shorthand is that P means "easy to find" and NP means "easy to check" (Clay Mathematics Institute n.d.-a). Every problem in P is also in NP. The question is whether every problem in NP is also in P. In symbols, does \text{P} = \text{NP}?

NP-Complete Problems

In 1971, Stephen Cook introduced the idea of NP-completeness, and Leonid Levin independently defined a closely related idea (Cook n.d.; Clay Mathematics Institute n.d.-a). A problem is NP-complete if it's in NP and every problem in NP can be translated into it efficiently. So NP-complete problems are, in a precise sense, the hardest problems in NP.

That gives them a remarkable property. If any single NP-complete problem had a polynomial-time algorithm, then every problem in NP would, and P would equal NP (Cook n.d.). Cook's description reports many hundreds of known NP-complete problems, including ones about coloring the points of a network and finding a route that visits every point of a network exactly once. Such problems give rise to many scheduling and routing problems of real industrial importance (Cook n.d.). A fast method for one would be a fast method for all of them.

Why It Matters for Encryption

Much of modern encryption relies on problems that are believed to be hard. Cook gives the example of factoring large whole numbers into primes: an efficient factoring algorithm would break the RSA public-key encryption scheme (Cook n.d.). Public-key encryption lets two parties communicate securely without first sharing a secret key. Assumptions of this kind would all be false if P equaled NP (Cook n.d.).

So a proof that P equals NP would threaten much of today's encryption, at least in principle. How much it would threaten in practice would depend on how fast the resulting algorithms turned out to be. A proof that P doesn't equal NP wouldn't by itself make any particular code safe, but it would confirm that some problems really are beyond efficient solution.

An Open Prize Problem

Most complexity theorists believe that P doesn't equal NP (Cook n.d.). Part of the reason is that decades of effort have produced no fast algorithm for any NP-complete problem. But a belief isn't a proof. P versus NP is one of the seven Millennium Prize Problems, a set of major open problems for which the Clay Mathematics Institute set aside $1 million each when it announced them in 2000. One of the seven, the Poincaré conjecture, has been solved. P versus NP is listed as unsolved (Clay Mathematics Institute n.d.-b).

Conclusion

P is the class of problems that can be solved efficiently, and NP the class whose answers can be checked efficiently. Whether the two are the same is unknown. Most experts expect a proof that they differ, but as of October 2026 no proof in either direction exists.

This content reflects the field as of October 2026.

Key Terms

  • P: The class of yes-or-no problems that some algorithm can solve in polynomial time.
  • NP: The class of yes-or-no problems for which a proposed "yes" answer can be checked in polynomial time.
  • NP-complete: Describes a problem in NP into which every problem in NP can be translated efficiently, so that a fast algorithm for it would give fast algorithms for all of NP.
  • Millennium Prize Problems: Seven major open problems for which the Clay Mathematics Institute set aside $1 million each in 2000.

References

Reading 4 min Done

Computer-Assisted Proof and Proof Assistants

Introduction

For most of history, a proof was something a person wrote and other people checked by reading. Since 1976, computers have taken over more and more of that work, first by checking cases inside human arguments, then by checking entire proofs line by line. This reading follows that shift through two famous theorems, explains what proof assistants are, and sets out what a machine-checked proof does and doesn't guarantee.

Checking Cases: The Four Color Theorem

In 1852, Francis Guthrie posed a coloring puzzle: can every map be colored with four colors so that regions sharing a border always get different colors (Gonthier 2008, 1382)? The answer, yes, was proved by Appel and Haken in 1976. Their proof combined a human argument with a computer check of a very large number of cases. As Gonthier puts it, they "had a computer do the proof for them," and that part couldn't be checked by reading (Gonthier 2008, 1382). A 1995 revision of the proof still relied on a computer to check 633 configurations, small map patterns that the argument has to rule out one by one (Gonthier 2008, 1382–1383).

The result is a standard example of a computer-assisted proof: a proof in which a computer carries out part of the argument, typically checking more cases than people could check by hand. Gonthier describes the 1976 result as a triumph with "a hint of defeat" (Gonthier 2008, 1382). People could check the logic of the human part, but trusting the computer part meant trusting the program that did it.

Checking a Whole Proof: The Kepler Conjecture

The Kepler conjecture says that no way of packing equal balls in space is denser than an arrangement called the face-centered cubic packing, which fills about 74 percent of space (Hales et al. 2017, secs. 1 and 3). Ferguson and Hales established it in 1998, but their proof relied on extensive computer calculations, and it wasn't published in full until 2006. Even then, it appeared without complete certification from the referees (Hales et al. 2017, sec. 1).

A project called Flyspeck then set out to check the entire proof by computer, down to the last logical step. The finished formal proof, written in two proof assistants called HOL Light and Isabelle, was published in 2017 (Hales et al. 2017).

Proof Assistants

A proof assistant is software that checks every logical step of a proof written in a formal language, a language precise enough that a computer can read it. Using one is called formal verification: checking by computer that every step of a proof follows, by the rules of logic, from stated axioms and results already proved. Axioms are the basic assumptions a branch of mathematics starts from.

Gonthier and his colleagues completed a formal proof of the four color theorem in 2005 in a proof assistant called Coq (Gonthier 2008, 1382, 1384). Another proof assistant is Lean, which its developers describe as an open-source programming language and proof assistant (Lean FRO n.d.). Writing formal proofs is still hard work. Gonthier calls them "very difficult to produce" (Gonthier 2008, 1382).

What Verification Guarantees and What It Doesn't

A formally verified proof is far more trustworthy than a long proof checked only by eye. But it isn't beyond all doubt, and the limits are specific.

A verified proof guaranteesA verified proof doesn't guarantee
Every step follows from the stated axioms by the rules of logicThat the formal statement says what the mathematician meant
No case was skipped and no step was waved throughThat the axioms and definitions match the intended ones
The check can be repeated by anyone, or by a different programThat the checking software itself has no bugs, though checkers are tested on many inputs

The first gap matters most. Gonthier's four color statement rests on about 40 lines of definitions from topology and about 100 lines describing the real numbers. A reader still has to check those definitions to confirm that the theorem "lives up to its name" (Gonthier 2008, 1388). If the formal statement were subtly wrong, the software would correctly verify a proof of the wrong theorem.

Conclusion

Computers have moved from checking cases inside human proofs to checking whole proofs, step by step. The four color theorem and the Kepler conjecture now both have machine-checked proofs, and proof assistants such as Lean are in active use. A verified proof shows that the result follows from the axioms, provided the statement was formalized correctly, and checking that still falls to people.

This content reflects the field as of October 2026.

Key Terms

  • Computer-assisted proof: A proof in which a computer carries out part of the argument, typically checking more cases than people could check by hand.
  • Proof assistant: Software that checks every logical step of a proof written in a precise formal language.
  • Formal verification: Checking by computer that every step of a proof follows, by the rules of logic, from stated axioms and results already proved.
  • Lean: An open-source programming language and proof assistant.

References

  • Gonthier, Georges. 2008. "Formal Proof—The Four-Color Theorem." Notices of the American Mathematical Society 55 (11): 1382–1393.
  • Hales, Thomas, Mark Adams, Gertrud Bauer, Dat Tat Dang, and 18 others. 2017. "A Formal Proof of the Kepler Conjecture." Forum of Mathematics, Pi 5: e2. Preprint arXiv:1501.02155.
  • Lean FRO. n.d. "Lean." Accessed October 13, 2026.

Reading 4 min Done

AI Systems as Mathematical Collaborators: The 2026 Frontier

Introduction

Until recently, computers in mathematics checked cases or checked proofs that people had found. In 2026, AI systems were reported to have produced research-level results themselves, and mathematicians are arguing about what that means. This reading reports three recent cases, with their dates, and the debate they've prompted. Some of these claims are still under review, so they're reported here as claims.

A New Bound for Multiplying Matrices

A matrix is a rectangular table of numbers, and multiplying matrices is a basic step in many calculations. The matrix multiplication exponent, written \omega (the Greek letter omega), measures how fast the best possible method for multiplying two large square matrices can be. A smaller upper bound on \omega means faster methods are known to exist in principle.

On August 17, 2026, ten researchers posted a preprint, a paper shared publicly before peer review, reporting that \omega < 2.371177, improving the previous best bound of 2.371339 (Dupont et al. 2026). They reformulated the optimization problem at the core of the current method, built a new optimization algorithm, and made a final refinement with an AI system called AlphaEvolve. Several of the authors list Google DeepMind as their affiliation (Dupont et al. 2026). Two days later, a revised version of a 2024 paper by six researchers, three of them also authors of the August preprint, stated the same bound, combining its own analysis with recent numerical optimization results (Alman et al. 2024). Both are preprints, so the bound is provisional until it has been checked by referees.

A Claim About Navier–Stokes

The Navier–Stokes equations describe how fluids such as water and air flow. One of the Clay Mathematics Institute's Millennium Prize Problems asks whether their solutions always stay smooth, or whether they can break down, a failure called blowup, in finite time.

On September 8, 2026, OpenAI announced that an internal AI system had produced a proof that an initially smooth fluid at rest, pushed by a smooth external force, can develop a singularity in finite time. The company said the proof establishes one of the outcomes that the official problem statement accepts as a solution, and that a formalization in Lean, a proof assistant, was completed in about 17 more hours. It said it doesn't intend to claim the prize (OpenAI 2026). On September 11, the institute acknowledged the announcement that the problem "has apparently been settled." It said that its rules cover both evaluating the result and assigning credit, and that the process is "deliberately unhurried" (Clay Mathematics Institute 2026). As of October 13, 2026, the institute lists the problem as "Active," not solved (Clay Mathematics Institute n.d.-b).

AI as an Assistant

AI systems also work alongside mathematicians. On September 7, 2026, Terence Tao described new results by Levent Alpöge and Tristan Buckmaster on blowup, with a smooth applied force, for three related fluid equations. Tao called the arguments "heavily AI-assisted" and noted that the work had been formalized in Lean (Tao 2026). This is an AI-assisted proof: one in which AI systems contribute substantially to finding or writing the argument, while people direct the work and check it.

Two further steps keep such work trustworthy. Formalization is translating a proof into a formal language that a proof assistant can check. Verification is checking that a proof is correct, by expert readers, by a proof assistant, or both. Formalization makes machine verification possible, but experts still have to confirm that the formal statement matches the intended problem.

The Debate About Understanding

In a guest post on Tao's blog on September 12, 2026, Steven Strogatz described mathematics as a human conversation about why things are true. He welcomed AI for opening the field to "millions of people without years of specialized training," a prospect he called "thrilling." He also feared that "something precious may disappear along the way" (Strogatz 2026). In a reply to a reader, he said the loss would be greatest if producing and verifying proofs came to replace understanding them (Strogatz 2026). Understanding, in this sense, means grasping why a result is true, not only knowing that it has been proved.

Conclusion

As of October 2026, the reported record bound for matrix multiplication comes from preprints, one of which used an AI system in its final step. A claimed AI-produced Navier–Stokes proof is under the Clay Institute's evaluation, and AI tools are part of some mathematicians' research. What these results mean for proof and understanding is openly contested.

This content reflects the field as of October 2026.

Key Terms

  • AI-assisted proof: A proof in which AI systems contribute substantially to finding or writing the argument, while people direct the work and check it.
  • Formalization: Translating a proof into a formal language that a proof assistant can check.
  • Verification: Checking that a proof is correct, by expert readers, by a proof assistant, or both.
  • Understanding: Grasping why a result is true, not only knowing that it has been proved.

References

  • Alman, Josh, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou. 2024. "More Asymmetry Yields Faster Matrix Multiplication." arXiv:2404.16349. Preprint, version 3, August 19, 2026.
  • Clay Mathematics Institute. 2026. "Navier–Stokes Announcement." September 11, 2026.
  • Clay Mathematics Institute. n.d.-b. "Millennium Prize Problems." Accessed October 13, 2026.
  • Dupont, Emilien, Marvin Eisenberger, Borislav Kozlovskii, Abbas Mehrabian, Francisco J. R. Ruiz, Abigail See, Renfei Zhou, Josh Alman, Virginia Vassilevska Williams, and Matej Balog. 2026. "Improving the Matrix Multiplication Exponent with Modern Optimization and AlphaEvolve." arXiv:2608.16884. Preprint.
  • OpenAI. 2026. "On the Navier–Stokes Millennium Prize Problem." September 8, 2026; updated September 10, 2026.
  • Strogatz, Steven. 2026. "Wimbledon, the U.S. Open, and the Future of Mathematics." Guest post on Terence Tao's blog, What's New, September 12, 2026.
  • Tao, Terence. 2026. "Finite Time Blowup with Smooth Forcing Term for the Incompressible Porous Medium, Boussinesq, and Incompressible Euler Equations." What's New, September 7, 2026.

Guided Reading 7 min Done

Guided Walkthrough: Checking a Route Versus Finding the Best One

Introduction

Some problems are easy to check and hard to solve. A route problem shows the difference in numbers you can work out by hand. This walkthrough takes four towns and a claim about a short round trip, checks the claim, then finds the best trip by trying every possibility. It then counts how both jobs grow as the number of towns grows.

The gap you'll see is the one at the center of the P versus NP question, which asks whether every problem whose answers are easy to check also has answers that are easy to find (Clay Mathematics Institute n.d.-a).

The Starting Point

Four towns, labeled A, B, C, and D, are connected by roads. The distances in kilometers are:

RoadDistance (km)
A to B50
A to C80
A to D60
B to C40
B to D70
C to D30

A delivery driver has to start at A, visit each of the other towns once, and return to A. A round trip like this is called a tour. A colleague claims that the tour A, B, C, D, then back to A is shorter than 200 kilometers.

You have two jobs. First, check the colleague's claim. Second, find the shortest tour of all, and be sure that no tour is shorter.

Walking Through the Comparison

Step 1: Check the claim

To check the claim, add the four distances on the proposed tour and compare the total with 200.

The tour goes A to B (50 km), B to C (40 km), C to D (30 km), and D back to A (60 km). The total is 50 + 40 + 30 + 60 = 180 kilometers. Since 180 is less than 200, the claim is true.

Count the work. You did three additions to combine four distances, then one comparison with 200. That's four steps. For a tour through any number of towns, checking takes as many steps as there are towns: one addition for each road after the first, plus one comparison at the end. You don't need to know anything about other possible tours to do it.

Step 2: Find the best tour by brute force

Finding the shortest tour is a different job. The direct method is brute force: list every possible tour, work out the length of each, and pick the smallest.

Start at A. The other three towns can be visited in 3 \times 2 \times 1 = 6 orders. But each tour can be driven in either direction, and both directions have the same length. A, B, C, D, A is the same round trip as A, D, C, B, A, driven the other way. So the 6 orders give only 3 distinct tours:

TourCalculationLength (km)
A, B, C, D, A50 + 40 + 30 + 60180
A, B, D, C, A50 + 70 + 30 + 80230
A, C, B, D, A80 + 40 + 70 + 60250

The shortest tour is A, B, C, D, A, at 180 kilometers. Because every tour is in the list, you know for certain that no shorter one exists. That certainty is what brute force buys, and what it costs is the work of listing everything.

Step 3: Count the tours for larger maps

With n towns, where n stands for the number of towns, the same reasoning gives (n-1)!/2 distinct tours. Here (n-1)!, read "n minus 1 factorial," means multiplying all the whole numbers from 1 up to n - 1. You fix the starting town, count the orders of the rest, and divide by 2 for the two directions.

For 4 towns, that's 3!/2 = 6/2 = 3, matching the list in Step 2. For 10 towns, it's 9!/2 = 362,880/2 = 181,440 tours. For 20 towns, it's 19!/2, which is about 6 \times 10^{16}, or 60 thousand trillion tours.

Step 4: Compare checking with searching

Put the two jobs side by side. Checking a single proposed tour through 20 towns takes about 20 steps. Searching all tours of 20 towns by brute force means checking about 6 \times 10^{16} of them. A computer that checked a billion tours per second would need about two years. With 21 towns, it would need about 39 years.

Checking grows slowly: add a town and you add one step. Searching grows explosively: add a town and you multiply the number of tours by the number of towns you already had. Going from 20 towns to 21 multiplies the count by 20. This kind of growth outpaces even exponential growth like 2^n, and it's why brute force, fine for 10 towns, is already impractical at around 20.

Step 5: Connect to P versus NP

Turn the route problem into a yes-or-no question: "Is there a tour shorter than 200 kilometers?" If someone hands you a tour, you can check it in a few steps, as in Step 1. So the question belongs to NP, the class of problems whose "yes" answers can be checked efficiently. P is the class of problems that can be solved efficiently, and the Clay Mathematics Institute describes the contrast as "easy to find" versus "easy to check" (Clay Mathematics Institute n.d.-a).

The open question is whether some clever method could find short tours for every map nearly as fast as you can check one, a shortcut through the search that nobody has discovered. If such shortcuts exist for every problem whose answers are easy to check, then P equals NP. Most complexity theorists believe they don't, but nobody has proved it either way (Cook n.d.). Routing and scheduling problems of this kind have real industrial importance (Cook n.d.), so the answer matters beyond mathematics.

Key Considerations

Good routes versus best routes. Real route planners don't use brute force. They use clever methods that find very good tours quickly, often without proving that no better tour exists. That's a different goal from the one in Step 2, where the aim was a tour you could prove is shortest. The P versus NP question is about finding guaranteed answers, for every possible map.

The common mistake: thinking faster computers will make brute force practical. It's tempting to think brute force is only waiting for better hardware. The numbers say otherwise. A computer 1,000 times faster would bring the 20-town search from about two years down to under a day. But each added town multiplies the work again, so the faster machine would be stuck again after only a few more towns. Speed buys a few extra towns, not a solution for large maps.

Checking isn't the same as finding. Step 1 confirmed that one tour is under 200 kilometers. It didn't show that 180 is the best possible. Only the full comparison in Step 2 did that. Mixing up the two jobs hides exactly the gap the P versus NP question is about.

Summary

Checking a proposed tour takes about one step per town, while finding the best tour by brute force means comparing a number of tours that explodes as towns are added.

TownsSteps to check one proposed tourNumber of distinct tours
443
1010181,440
2020about 6 \times 10^{16}

For the four-town map, the claim "under 200 km" is true (the tour totals 180 km), and A, B, C, D, A is the shortest tour, confirmed by comparing all three tours.

  1. The checking column counts one addition for each road after the first and one final comparison, which comes to one step per town.
  2. The tour column is (n-1)!/2, where n is the number of towns.
  3. Whether a shortcut can close the gap between the two columns, for every map, is part of what the P versus NP question asks.

References

  • Clay Mathematics Institute. n.d.-a. "P vs NP." Millennium Prize Problems. Accessed October 13, 2026.
  • Cook, Stephen. n.d. "The P Versus NP Problem." Official problem description, Millennium Prize Problems. Clay Mathematics Institute. Accessed October 13, 2026.

Guided Conversation 12 min Done

What Would It Take for You to Believe a Proof?

In this conversation, you'll start from something you believe because an expert or a machine checked it, then ask whether a proof that only a computer can check, or that an AI system found, counts as knowledge. You'll leave with your own criterion for accepting a proof.

You'll have this conversation with an AI assistant, using your own account. Choose a button to open a new chat with the prompt already filled in, then press send to start. If the chat opens empty, copy the prompt and paste it in.

Run this conversation in whichever assistant you already use:

Open in ClaudeOpen in ChatGPT
Claude desktop app

To use another LLM, simply copy and paste the prompt into its chat window.

Show the full prompt (it lists misreadings to watch for, so skip it if you would rather come to the conversation fresh) 
Guided Conversation: What Would It Take for You to Believe a Proof? (about 12 minutes)

Note to the learner: press send to start. Everything below is facilitator guidance for the AI. It lists misconceptions to watch for, so skip it if you'd rather come to the conversation fresh.

Please facilitate a reflective dialogue with me. I'm an adult who is comfortable with basic high-school algebra but may be rusty or uneasy with math, exploring what the mathematics of computation is and whether to study it further. I'm studying efficient algorithms, P versus NP, and computers that help prove theorems. Follow this guidance for the whole conversation.

GOAL
Help me explain P versus NP and describe how computers and AI systems take part in proof, through my own standards of evidence.

HOW TO RUN THE CONVERSATION
- Ask one question at a time, then wait for my reply. Keep each of your turns under about 120 words.
- Don't lecture. Explain a point only when I need it to continue, then return to my examples and reasons.
- Be curious, collegial, and patient. Define terms briefly on first use. Welcome disagreement when I give a reason.
- Plain conversation only: don't search the web or create files or documents.
- Aim for about 12 minutes, mostly on topics 2 and 3. If my replies are brief, offer one concrete prompt, such as "Do you trust a calculator's answer to a long division you'll never check?", and move on. If I seem uncertain, shorten the conversation to 5-7 minutes. Always reach the final topic.
- Start now. Open with one or two warm sentences: this is a conversation, not a quiz; my honest reasons matter more than the "right" view; I can ask you to clarify anything. Then ask me for something I believe because an expert or a machine checked it, not because I checked it myself.

TOPICS, IN ORDER
1. Trusting a check. Ask what I believe on someone else's check (a medical test, a bridge's safety rating) and why I trust it. Follow-up: in my example, is checking easier than finding? Connect briefly to P versus NP: many problems have answers that are easy to check but seem hard to find.
2. A proof no person can read. Describe the four color theorem briefly (see below). Ask whether it counts as knowledge for me, and what would make me trust or doubt it. Follow-up: what does a person still have to check?
3. A proof an AI system found. Ask what changes if an AI system finds the proof as well as checking it, using the Navier-Stokes claim as one example (see below). Follow-up: does it matter whether anyone understands why the result is true?
4. Closing. Ask me to state my own criterion for accepting a proof in one or two sentences, something I can take into writing a journal entry.

KEY POINTS TO KEEP ACCURATE
- P versus NP is unsolved. P: problems solvable efficiently (in polynomial time). NP: problems whose proposed answers can be checked efficiently. Most experts believe P is not equal to NP, but it's unproved. It's a Millennium Prize Problem.
- The four color theorem was computer-assisted (Appel and Haken, 1976) and fully machine-checked in the Coq proof assistant (Gonthier and colleagues, 2005). The Kepler conjecture's computer-assisted proof was fully formally verified in the Flyspeck project, published in 2017.
- On September 8, 2026, OpenAI announced that an internal AI system produced a proof of finite-time blowup for the Navier-Stokes equations with a smooth external force, with a Lean formalization. On September 11, the Clay Mathematics Institute said its review is deliberately unhurried. As of October 2026, the claim is under review and the institute lists the problem as active, not solved.
- Formal verification checks that a proof follows from the stated axioms and definitions. It doesn't check that the formal statement matches the intended one.
- Mathematicians disagree about what AI-produced proofs mean for understanding. Steven Strogatz welcomes the wider access AI offers but worries that producing and verifying proofs could replace understanding them.

MISCONCEPTIONS TO CORRECT GENTLY
When one appears, name the accurate version briefly, then return to my reasons.
- "A machine-checked proof can't be wrong": the formal statement can differ from the intended one, and people still have to check that it says what was meant.
- "AI has solved mathematics": AI results are specific, some are still under review, and many problems remain open.
- "P versus NP is about computer speed": it's about whether efficient methods exist at all, not about how fast machines run.

LIMITS
- Don't predict future AI capabilities.
- Don't take sides in credit disputes over any AI or human result.
- Don't state that the Navier-Stokes problem is solved.
- Don't settle the philosophical question for me; treat views on proof and understanding as positions.

TO FINISH
After I state my criterion, close in one short turn:
- Affirm one specific thing I worked out, in my own words where possible.
- Suggest one or two next steps that fit how the conversation went. Possible steps: test my criterion in writing on the four color theorem or the Navier-Stokes claim; look at what a proof assistant such as Lean checks; review the difference between checking and finding.
- Restate my criterion on its own line, labeled "My criterion for a proof", so I can copy it.

Journal 15 minOptional Done

Should a Proof No Human Can Read Count?

Overview

This optional journal entry asks you to take a position on a live question in mathematics: whether a proof that only a computer can check, or that an AI system produced, should count as mathematical knowledge. You'll state your view, argue for it, and give the other side its best case. The entry is for you; nothing is submitted.

Writing Prompt

In 300 to 400 words, argue whether a proof that only a computer can check, or that an AI system produced, should count as mathematical knowledge.

Steps

  1. State your position in one sentence. Say yes, no, or "it depends," and if it depends, say on what. A clear sentence here makes the rest of the entry easier to write.
  2. Give your strongest reason. Anchor it in a specific case: the four color theorem, proved in 1976 with a computer checking many cases; the Kepler conjecture, whose proof was fully machine-checked; the Navier–Stokes claim announced in September 2026 and still under review; or another case you know. Say what about that case supports your view.
  3. State the strongest objection, in its best form. Write it the way someone who holds it would. If your position is yes, the objection might be about understanding; if it's no, it might be about the reliability of human checking.
  4. Say what would change your mind. Name a specific fact, event, or argument. "Nothing would" isn't an answer for this step; push yourself to find something.

Self-Check

Before you finish, check that your entry:

  • States your position in one plain sentence
  • Supports your reason with a specific case, such as the four color theorem, the Kepler conjecture, or the Navier–Stokes claim
  • States the strongest objection fairly, in a form its supporters would accept
  • Names a specific thing that would change your mind
  • Falls between 300 and 400 words

Nothing is uploaded. Write in your own notebook or document and keep it.

Knowledge Check 10 min Done

Efficient algorithms, P versus NP, and computers that help prove theorems

This ungraded knowledge check assesses your understanding of how mathematicians measure what's hard to compute and how computers take part in proof. You'll be asked about growth rates of algorithms, P versus NP, computer-assisted proof and proof assistants, and AI systems in research mathematics.

Note: Use this to test yourself, review the feedback on any questions you miss, and retry until you feel confident before moving forward.

5 questions · ungraded · retry as often as you like

Graded Quiz 30 min Done

Computation

This graded quiz assesses your understanding of what algorithms can and can't do and how computers now take part in proof. You'll be asked about the history of algorithms, what makes something an algorithm, Turing machines, the halting problem, growth rates, P versus NP, proof assistants, and AI in mathematics.

Note: Aim for a score of 80 percent or higher. If you score lower, use the feedback to review the topics you missed, then retake the quiz.

10 questions · target score 80% · 3 forms, rotated on each attempt