AI for scienceMiddleLesson 2556 min read

AI and mathematics

Proof assistants like Lean check every step of a proof by machine. AI can help find proofs, spot patterns and suggest conjectures, and the checker keeps it honest.

✦ Ask the tutor🧪 Lab · 25 min📝 Lesson test
Lesson in motion

In 60 seconds

AI and mathematics

Proof assistants like Lean check every step of a proof by machine. AI can help find proofs, spot patterns and suggest conjectures, and the checker keeps it honest.

1/5
In simple words
When you solve a maths problem, your teacher checks each step. What if a very strict, very patient checker looked at every tiny step and never got tired? That is a proof assistant. It does not care who wrote the proof, a student, a professor or an AI. It only cares whether each step is correct.

Proofs, conjectures and checking

In mathematics, a conjecture is a statement people think is true but have not proved. A proof is a chain of logical steps that shows it must be true. Examples are not enough: a pattern can hold for many cases and then fail.
Look at n × n + n + 41. For n = 0, 1, 2 and many more, it gives a prime number. It is tempting to guess "always prime". But at n = 40 it gives 1681, which is 41 × 41. One counter-example breaks the pattern. The lab lets you see this yourself.

What a proof assistant is

A proof assistant is software where you write mathematics in a precise language, and the computer checks every step. Lean is a widely used proof assistant. Its community has built a large shared library of formal mathematics called mathlib.
Two tiny statements checked by Lean 4lean
-- Lean checks that 2 + 2 really equals 4.
example : 2 + 2 = 4 := rfl

-- For every natural number n, n + 0 = n.
theorem add_zero_example (n : Nat) : n + 0 = n := rfl
If a step is wrong, Lean refuses to accept the proof. This makes the checking very reliable. It is only as good as the statement you wrote, though: if you state the wrong theorem, Lean will happily check a proof of the wrong thing.

How AI helps mathematicians

TaskWhat AI doesWhat keeps it honest
Finding proofsA language model suggests the next proof step or a whole proof in Lean.Lean checks it. Wrong steps are rejected.
Searching the libraryAI helps find a lemma in a big library that fits the current step.The step must still check.
Spotting patternsMachine learning looks at lots of mathematical data and finds links a person might miss.Mathematicians must then prove the pattern.
Explaining and writingAI explains a proof in simpler words or drafts a write-up.A human must read it critically. Explanations can contain errors.
Researchers have shown that AI systems can solve some hard competition problems, with proofs checked by a formal system. Researchers have also used machine learning to spot patterns that led mathematicians to new conjectures and proofs. Progress is fast, and details change, so read the original papers before repeating claims.

The key idea: generate, then verify

  1. 1

    Propose

    A model suggests a proof, a step or a conjecture. It may be wrong.
  2. 2

    Check

    Lean checks a formal proof. Tests or counter-example searches check a conjecture.
  3. 3

    Keep or reject

    Only checked proofs are kept. Failed attempts give feedback for the next try.
  4. 4

    Understand

    Mathematicians read and explain the result, so people learn why it is true.
Note
This is why maths is a special area for AI. In most science, checking a prediction needs a slow experiment. In formal maths, a computer can check a proof quickly and with great reliability. A reliable checker makes AI suggestions much safer to use.
Risky use
  • Copying a chatbot's proof into homework without checking
  • Trusting a pattern because it held for 100 cases
  • Accepting a proof of a statement you did not read carefully
Good use
  • Asking AI for hints, then writing and checking the proof yourself
  • Searching for counter-examples, then trying to prove it
  • Checking that the formal statement says what you mean
Try this. Think of a pattern you noticed in maths class, such as "the sum of two odd numbers is even". Can you explain why it is always true, not just for the examples you tried?

Watch and read more

Lean programming language and theorem proverLean · reading

Lab

A small Python search that tests a tempting conjecture, and a written reflection on examples versus proof.

~25 min

The problem

You will test two conjectures by searching for counter-examples.

  1. Run the starter code. It tests "n × n + n + 41 is always prime" for n from 0 to 50. At which n does it first fail?
  2. Change the code to test a second conjecture: "the sum of the first n odd numbers is n × n". Check n from 1 to 1000. Does it ever fail?
  3. For the second conjecture, try to explain in your own words (or with a picture of squares) why it is always true. This is the start of a proof.
  4. Write three sentences on the difference between "checked for 1000 cases" and "proved".

Practice lab

Edit the code and run it. Python runs in your browser — nothing is sent to our server.

Output

No output. Add print(...) to see values.

You are done when

Hard questions

Try to answer before you reveal. If you can answer these, you understood the lesson.

Q1If a computer checks a conjecture for a billion cases with no counter-example, is that a proof?Reveal

No. The statement is about infinitely many numbers, and a billion is still a finite number of cases. Some famous conjectures held for enormous ranges before a counter-example was found. Large checks are good evidence and can guide mathematicians, but a proof must cover every case by logic.

Q2An AI writes a Lean proof that is accepted, but the mathematicians do not understand why it works. Is that a problem?Reveal

The result is still correct: Lean has checked it. But mathematics is also about understanding. A proof no one understands teaches less and is harder to build on. Mathematicians may then study the proof to extract the key idea, or look for a clearer one. Correctness and understanding are both valued.

Please sign in to continue.

Questions people ask

Can a chatbot's written proof be trusted?

Not by itself. A chatbot can write a proof that sounds convincing but has a gap or a wrong step. Check it carefully yourself, or use a proof assistant. A formal proof checked by Lean is much more trustworthy than prose.

Is Lean hard to learn?

It takes practice, like any precise language. There are free beginner tutorials and interactive games linked from lean-lang.org and the Lean community. School algebra is enough to start with the simplest ones.

Will AI replace mathematicians?

AI is becoming a strong helper for finding and checking proofs. But choosing important questions, building new ideas and explaining why things are true are deeply human parts of mathematics. Many mathematicians see AI as a new kind of collaborator and tool.

What if the statement given to Lean is wrong?

Then Lean may check a correct proof of the wrong statement. This is a real risk. People must read the formal statement carefully and make sure it matches what they meant. The checker verifies the proof, not your intention.

Lesson test

5 questions. Get 3 right (60%) to pass and complete this lesson.

Sign in to take the test and save your progress