Can AI check your maths proofs? Yes, if you ask it the right question

AI is good enough to check most undergraduate maths exercises, but only if you ask it a narrow question. If you paste a proof and ask "is this correct?", the model will quite often say yes, tidy up your wording and hand it back. You read the tidy version, it looks fine, and the gap is still there.

So I'd ask something narrower: "Quote the first line that doesn't follow from the lines before it, and say what's missing." That gives you one specific thing to fix. It also stops the model rewriting the proof for you, which is the version you'd be tempted to just read and accept.

Test it on a proof you've broken on purpose

Before you trust any checker, give it something you know is wrong and see whether it notices. Quantifier order is a good place to plant the error, because it's where most self-taught analysis proofs go wrong in my experience, and a model can miss it as well.

The definition of a limit says that $a_n \to L$ when

$$\forall \varepsilon > 0 \;\; \exists N \;\; \forall n \ge N : \; |a_n - L| < \varepsilon.$$

Swap the first two quantifiers and you get

$$\exists N \;\; \forall \varepsilon > 0 \;\; \forall n \ge N : \; |a_n - L| < \varepsilon,$$

which says something much stronger. A single N works for every epsilon, so $|a_n - L|$ is smaller than every positive number, which means $a_n = L$ exactly from N onwards. The sequence 1/n tends to 0 but never equals 0, so it satisfies the first statement and fails the second.

Here is a short broken proof you can paste in as a test:

Claim: 1/n -> 0.
Proof. Let eps > 0. Take N = n + 1. Then for n >= N we have 1/n < eps. QED.

The error is that N depends on n, while the definition needs N to be chosen from epsilon alone, before n is fixed. A correct choice is any whole number $N > 1/\varepsilon$ , so that $n \ge N$ gives $1/n \le 1/N < \varepsilon$ . If the model calls the broken version fine, you've learnt something about how far to trust it on your real work.

Write the reason next to every step

The other habit that helps is writing, next to each line, which definition or earlier result it uses: "by the triangle inequality", "by Lemma 2", "since N was chosen so that 1/N < eps". If you can't name the reason for a line, that's usually where the gap is, and you'll often find it before the AI does.

Also, this makes the AI's job easier. "Line 4 uses the triangle inequality, is that applied correctly?" is a question it answers far more reliably than "is this proof right?".

When you want a checker that can't be talked round

A language model can be persuaded. A proof assistant can't. Once you've worked through a chapter of an analysis book this way, Lean is a good next step, because it won't accept a line that doesn't follow. Terence Tao has published a Lean companion to his Analysis I, which follows the book chapter by chapter, so you can formalise the same exercises you've already done on paper.

For proof-style exam questions to practise this on, the STEP questions with full worked solutions at https://geodesicpartners.co.uk/oxbridge-maths-questions-step are a good set. Each one needs a short argument written out properly, which is exactly what this kind of checking is for.