{"course":{"slug":"ai-for-students","title":"AI for Students","url":"https://addaly.com/learn/ai-for-students","level":"beginner","track":"work"},"lesson":{"slug":"proofs-and-reasoning","title":"Proofs, and the step that looks fine","url":"https://addaly.com/learn/ai-for-students/proofs-and-reasoning","position":30,"of":73,"minutes":8,"answer":"Generated proofs fail by making one unjustified move inside otherwise correct working, so read upward from the conclusion asking what licenses each step, and check the seven standard illegal moves.","keyIdea":"Generated proofs fail by making one unjustified move inside otherwise correct working, so read upward from the conclusion asking what licenses each step, and check the seven standard illegal moves."},"body":{"format":"markdown","text":"## A proof is a chain with no weak links permitted\n\nMost writing tolerates a slightly loose sentence. A proof does not. One unjustified step and the whole thing is worth nothing, however correct the conclusion happens to be. This makes proof the subject where generated text is most dangerous, because a model produces *proof-shaped* text extremely well.\n\nThe characteristic failure is not gibberish. It is a proof that is correct for six lines, makes one move that is not justified, and continues correctly to the right answer. Everything reads normally. Markers find these instantly, because an unjustified step is exactly what they are trained to look for, and it is the thing being examined.\n\n## The moves that go wrong\n\nA short list covers most of them:\n\n- **Dividing by something that might be zero.** The classic, and it appears constantly.\n- **Assuming what is being proved**, usually several lines in and rephrased so it does not look like it.\n- **Swapping quantifiers.** *For all x there exists y* is not *there exists y for all x*, and the difference is the content of half of analysis.\n- **Using a theorem outside its hypotheses.** Applying a result about continuous functions to one that is not, or a result about finite sets to an infinite one.\n- **Taking a limit inside something** (a sum, an integral, an expectation) where that requires justification.\n- **Induction with a broken step.** The base case is checked, the inductive step quietly assumes the statement for all smaller n when the induction was set up for n minus one only.\n- **Special case treated as general.** Verifying three examples and writing *hence in general*.\n\nRead any generated proof looking specifically for these seven, in this order. It takes two minutes and catches most of what goes wrong.\n\n## Read it backwards\n\nA technique from mathematicians that works especially well on generated text. Start at the conclusion and work upward, asking of each line: *what exactly justifies this from the line above?* Forward reading rides the momentum of a plausible narrative. Backward reading breaks it, because you are forced to supply the justification yourself rather than accepting that one was implied.\n\nIf you cannot name the rule that licenses a step, that step is not proved, whatever it says.\n\n## Where a model is actually useful in proof work\n\n- **Proof strategy.** *Is this more likely to be direct, contrapositive, contradiction, or induction, and why?* This is good advice most of the time, and choosing the strategy is where beginners get stuck.\n- **Finding a counterexample** to a statement you suspect is false. Then verify the counterexample yourself, which is easy: checking a counterexample is much cheaper than finding one.\n- **Explaining a step in a proof from your textbook** that you cannot follow. Grounded on a real proof, this is safe and very useful.\n- **Asking what the theorem is doing**: which hypothesis is load-bearing, what fails without it. Excellent for building intuition.\n- **Generating similar exercises** once you can do one.\n\nNotice the pattern: the model is good at the meta-level (strategy, intuition, explanation of an existing proof) and unreliable at producing a valid new proof.\n\n> Figure: What a model is for in proof work, and what it is not. Good: the meta-level: Which strategy this is, and why: direct, contrapositive, contradiction, induction; A counterexample to a statement you suspect is false, which you then check yourself; Explaining a step in your textbook's proof that you cannot follow; Which hypothesis is load-bearing, and what fails without it; Similar exercises, once you can already do one. Unreliable: producing a valid new proof: Dividing by something that might be zero; Assuming what is being proved, rephrased so it does not look like it; Swapping quantifiers, which is the content of half of analysis; Using a theorem outside its hypotheses; Verifying three examples and writing hence in general. The characteristic failure is not gibberish. It is six correct lines, one unjustified move, and the right conclusion. Read upward from the conclusion asking what licenses each step: forward reading rides the momentum of a plausible narrative, and backward reading breaks it because you have to supply the justification yourself. If you cannot name the rule, that step is not proved.\n\n## Proof assistants, and the free path\n\nIf you want a machine that cannot accept an invalid step, that exists and is free: **Lean** (with its mathlib library), **Coq**, and **Isabelle** are proof assistants that check every inference mechanically. They are hard to learn and out of scope for most undergraduate courses, but the existence of the distinction is worth knowing: a language model produces text that resembles a proof, and a proof assistant verifies a proof. Those are different categories of thing, and confusing them is the error underneath every story about an AI-generated proof that turned out to be wrong.\n\nLean has an active community and a free online textbook, *Mathematics in Lean*. If you are heading towards pure maths, an afternoon with it will permanently change how you read a proof, because it forces you to notice every step you had been waving at.\n\n## Writing proofs for assessment\n\nThe honest position: reading generated proofs teaches you the shape of proof writing and does not teach you to construct one, for the same reason reading worked examples does not teach you to solve problems. If your assessment includes proofs, the unaided check from Module 3 is not optional. Write one from blank paper, weekly, timed.\n\nAnd when you are stuck, use the hint ladder rather than the solution. *What kind of proof is this likely to be?* is rung two. *What is the first line?* is rung three. The rung that gives you the whole argument is the one that teaches you nothing at all."},"check":{"question":"Why does reading a generated proof backwards from the conclusion catch errors that forward reading misses?","options":[{"text":"Because errors are more likely near the end of generated text, where the model has more context to be distracted by.","correct":false,"tempting":"Invents a positional claim; unjustified steps appear wherever the difficulty of the argument sits, which is usually in the middle."},{"text":"Because a proof read backwards is logically equivalent to its contrapositive, which is easier to verify.","correct":false,"tempting":"Confuses a reading order with a logical transformation; nothing about reading upward changes the statement being proved."},{"text":"Because forward reading rides a plausible narrative; upward reading makes you supply each justification.","correct":true},{"text":"Because the conclusion is the only line whose correctness you can check independently, so verification must start there.","correct":false,"tempting":"Treats the conclusion as an anchor, but a correct conclusion is exactly what an invalid proof usually reaches; its correctness proves nothing about the chain."}]},"prev":{"slug":"maths-and-arithmetic","title":"Maths, and the arithmetic problem","url":"https://addaly.com/learn/ai-for-students/maths-and-arithmetic"},"next":{"slug":"programming-and-cs","title":"Code that runs and is wrong","url":"https://addaly.com/learn/ai-for-students/programming-and-cs"},"authorship":"Founder and series editor: Dr Mustafa Mun. Written by AI models to a written standard. Exam keys checked blind by a second model: 3,665 of 3,666 agreed. Academic review invited.","review":{"status":"Draft, open for academic review"},"cite":"Addaly (2026) 'Proofs, and the step that looks fine', in AI for Students. Edited by M. Mun. Addaly. Available at: https://addaly.com/learn/ai-for-students/proofs-and-reasoning (Accessed: 13 October 2026).","licence":{"name":"CC BY-NC-SA 4.0","url":"https://creativecommons.org/licenses/by-nc-sa/4.0/"},"reader":{"schema":1,"title":"Proofs, and the step that looks fine","courseTitle":"AI for Students","module":{"index":4,"slug":"subject-by-subject","title":"Subject by subject"},"answer":null,"keyIdea":"Generated proofs fail by making one unjustified move inside otherwise correct working, so read upward from the conclusion asking what licenses each step, and check the seven standard illegal moves.","hero":{"kind":"figure","figure":{"t":"figure","label":"Figure","figure":{"left":{"title":"Good: the meta-level","items":["Which strategy this is, and why: direct, contrapositive, contradiction, induction","A counterexample to a statement you suspect is false, which you then check yourself","Explaining a step in your textbook’s proof that you cannot follow","Which hypothesis is load-bearing, and what fails without it","Similar exercises, once you can already do one"]},"type":"compare","right":{"title":"Unreliable: producing a valid new proof","items":["Dividing by something that might be zero","Assuming what is being proved, rephrased so it does not look like it","Swapping quantifiers, which is the content of half of analysis","Using a theorem outside its hypotheses","Verifying three examples and writing hence in general"]},"title":"What a model is for in proof work, and what it is not","caption":"The characteristic failure is not gibberish. It is six correct lines, one unjustified move, and the right conclusion. Read upward from the conclusion asking what licenses each step: forward reading rides the momentum of a plausible narrative, and backward reading breaks it because you have to supply the justification yourself. If you cannot name the rule, that step is not proved."},"alt":"Figure: What a model is for in proof work, and what it is not. Good: the meta-level: Which strategy this is, and why: direct, contrapositive, contradiction, induction; A counterexample to a statement you suspect is false, which you then check yourself; Explaining a step in your textbook’s proof that you cannot follow; Which hypothesis is load-bearing, and what fails without it; Similar exercises, once you can already do one. Unreliable: producing a valid new proof: Dividing by something that might be zero; Assuming what is being proved, rephrased so it does not look like it; Swapping quantifiers, which is the content of half of analysis; Using a theorem outside its hypotheses; Verifying three examples and writing hence in general. The characteristic failure is not gibberish. It is six correct lines, one unjustified move, and the right conclusion. Read upward from the conclusion asking what licenses each step: forward reading rides the momentum of a plausible narrative, and backward reading breaks it because you have to supply the justification yourself. If you cannot name the rule, that step is not proved."}},"blocks":[{"t":"h2","id":"a-proof-is-a-chain-with-no-weak-links-permitted","runs":[{"text":"A proof is a chain with no weak links permitted"}]},{"t":"p","runs":[{"text":"Most writing tolerates a slightly loose sentence. A proof does not. One unjustified step and the whole thing is worth nothing, however correct the conclusion happens to be. This makes proof the subject where generated text is most dangerous, because a model produces "},{"text":"proof-shaped","i":true},{"text":" text extremely well."}]},{"t":"p","runs":[{"text":"The characteristic failure is not gibberish. It is a proof that is correct for six lines, makes one move that is not justified, and continues correctly to the right answer. Everything reads normally. Markers find these instantly, because an unjustified step is exactly what they are trained to look for, and it is the thing being examined."}]},{"t":"h2","id":"the-moves-that-go-wrong","runs":[{"text":"The moves that go wrong"}]},{"t":"p","runs":[{"text":"A short list covers most of them:"}]},{"t":"ul","items":[[{"text":"Dividing by something that might be zero.","b":true},{"text":" The classic, and it appears constantly."}],[{"text":"Assuming what is being proved","b":true},{"text":", usually several lines in and rephrased so it does not look like it."}],[{"text":"Swapping quantifiers.","b":true},{"text":" "},{"text":"For all x there exists y","i":true},{"text":" is not "},{"text":"there exists y for all x","i":true},{"text":", and the difference is the content of half of analysis."}],[{"text":"Using a theorem outside its hypotheses.","b":true},{"text":" Applying a result about continuous functions to one that is not, or a result about finite sets to an infinite one."}],[{"text":"Taking a limit inside something","b":true},{"text":" (a sum, an integral, an expectation) where that requires justification."}],[{"text":"Induction with a broken step.","b":true},{"text":" The base case is checked, the inductive step quietly assumes the statement for all smaller n when the induction was set up for n minus one only."}],[{"text":"Special case treated as general.","b":true},{"text":" Verifying three examples and writing "},{"text":"hence in general","i":true},{"text":"."}]]},{"t":"p","runs":[{"text":"Read any generated proof looking specifically for these seven, in this order. It takes two minutes and catches most of what goes wrong."}]},{"t":"h2","id":"read-it-backwards","runs":[{"text":"Read it backwards"}]},{"t":"p","runs":[{"text":"A technique from mathematicians that works especially well on generated text. Start at the conclusion and work upward, asking of each line: "},{"text":"what exactly justifies this from the line above?","i":true},{"text":" Forward reading rides the momentum of a plausible narrative. Backward reading breaks it, because you are forced to supply the justification yourself rather than accepting that one was implied."}]},{"t":"p","runs":[{"text":"If you cannot name the rule that licenses a step, that step is not proved, whatever it says."}]},{"t":"h2","id":"where-a-model-is-actually-useful-in-proof-work","runs":[{"text":"Where a model is actually useful in proof work"}]},{"t":"ul","items":[[{"text":"Proof strategy.","b":true},{"text":" "},{"text":"Is this more likely to be direct, contrapositive, contradiction, or induction, and why?","i":true},{"text":" This is good advice most of the time, and choosing the strategy is where beginners get stuck."}],[{"text":"Finding a counterexample","b":true},{"text":" to a statement you suspect is false. Then verify the counterexample yourself, which is easy: checking a counterexample is much cheaper than finding one."}],[{"text":"Explaining a step in a proof from your textbook","b":true},{"text":" that you cannot follow. Grounded on a real proof, this is safe and very useful."}],[{"text":"Asking what the theorem is doing","b":true},{"text":": which hypothesis is load-bearing, what fails without it. Excellent for building intuition."}],[{"text":"Generating similar exercises","b":true},{"text":" once you can do one."}]]},{"t":"p","runs":[{"text":"Notice the pattern: the model is good at the meta-level (strategy, intuition, explanation of an existing proof) and unreliable at producing a valid new proof."}]},{"t":"h2","id":"proof-assistants-and-the-free-path","runs":[{"text":"Proof assistants, and the free path"}]},{"t":"p","runs":[{"text":"If you want a machine that cannot accept an invalid step, that exists and is free: "},{"text":"Lean","b":true},{"text":" (with its mathlib library), "},{"text":"Coq","b":true},{"text":", and "},{"text":"Isabelle","b":true},{"text":" are proof assistants that check every inference mechanically. They are hard to learn and out of scope for most undergraduate courses, but the existence of the distinction is worth knowing: a language model produces text that resembles a proof, and a proof assistant verifies a proof. Those are different categories of thing, and confusing them is the error underneath every story about an AI-generated proof that turned out to be wrong."}]},{"t":"p","runs":[{"text":"Lean has an active community and a free online textbook, "},{"text":"Mathematics in Lean","i":true},{"text":". If you are heading towards pure maths, an afternoon with it will permanently change how you read a proof, because it forces you to notice every step you had been waving at."}]},{"t":"h2","id":"writing-proofs-for-assessment","runs":[{"text":"Writing proofs for assessment"}]},{"t":"p","runs":[{"text":"The honest position: reading generated proofs teaches you the shape of proof writing and does not teach you to construct one, for the same reason reading worked examples does not teach you to solve problems. If your assessment includes proofs, the unaided check from Module 3 is not optional. Write one from blank paper, weekly, timed."}]},{"t":"p","runs":[{"text":"And when you are stuck, use the hint ladder rather than the solution. "},{"text":"What kind of proof is this likely to be?","i":true},{"text":" is rung two. "},{"text":"What is the first line?","i":true},{"text":" is rung three. The rung that gives you the whole argument is the one that teaches you nothing at all."}]}],"check":{"question":[{"text":"Why does reading a generated proof backwards from the conclusion catch errors that forward reading misses?"}],"options":[{"text":[{"text":"Because errors are more likely near the end of generated text, where the model has more context to be distracted by."}],"correct":false,"tempting":[{"text":"Invents a positional claim; unjustified steps appear wherever the difficulty of the argument sits, which is usually in the middle."}]},{"text":[{"text":"Because a proof read backwards is logically equivalent to its contrapositive, which is easier to verify."}],"correct":false,"tempting":[{"text":"Confuses a reading order with a logical transformation; nothing about reading upward changes the statement being proved."}]},{"text":[{"text":"Because forward reading rides a plausible narrative; upward reading makes you supply each justification."}],"correct":true,"tempting":null},{"text":[{"text":"Because the conclusion is the only line whose correctness you can check independently, so verification must start there."}],"correct":false,"tempting":[{"text":"Treats the conclusion as an anchor, but a correct conclusion is exactly what an invalid proof usually reaches; its correctness proves nothing about the chain."}]}],"order":[0,3,2,1],"why":null},"prev":{"slug":"maths-and-arithmetic","title":"Maths, and the arithmetic problem","minutes":9},"next":{"slug":"programming-and-cs","title":"Code that runs and is wrong","minutes":9}}}