The Lumenary · Advanced undergraduate

Mathematical writing

Name: ______________________

Date: ______________________

You will learn to

Rewrite a correct but unclear proof so that its structure, assumptions and key steps are explicit
Define every symbol before use, state every hypothesis, and control quantifier order and scope
Typeset definitions, theorems and proofs in LaTeX with consistent notation, labels and cross-references
Write a short expository note that states precisely which results are proved, which are cited and which are conjectured
Explain what formalisation in a proof assistant forces a writer to make explicit

1.
You prove an auxiliary result whose main purpose is to be used in the proof of your main theorem. What is it conventionally called?
- A.A lemma
- B.A corollary
- C.A conjecture
- D.A remark
2.
A draft says: "If $x^2 = 4$ , then $x = 2$ ." Which revision is a correct, complete statement?
- A."If $x$ is a natural number and $x^2 = 4$ , then $x = 2$ ."
- B."If $x$ is an integer and $x^2 = 4$ , then $x = 2$ ."
- C."Clearly, if $x^2 = 4$ then $x = 2$ ."
- D." $x^2 = 4 \Rightarrow x = 2$ ."
3.
For a function $f : \R \to \R$ , which property does this sentence define? "For every $\varepsilon > 0$ there is $\delta > 0$ such that for all $x, y \in \R$ with $|x - y| < \delta$ we have $|f(x) - f(y)| < \varepsilon$ ."
- A.Uniform continuity
- B.Continuity (at every point)
- C.Lipschitz continuity
- D.Constancy
4.
"Suppose there are finitely many primes $p_1, \dots, p_k$ . (1) Let $N = p_1 \cdots p_k + 1$ . (2) No $p_i$ divides $N$ . (3) Therefore $N$ is prime. (4) But $N$ is larger than every $p_i$ , a contradiction." Read as general facts, which step is false?
- A.Step (3)
- B.Step (2)
- C.Step (1)
- D.Step (4)
5.
Your note proves Proposition 4 using an earlier statement labelled "Conjecture 2" (not proved by anyone). How should Proposition 4 be presented?
- A.As a conditional result: "Assuming Conjecture 2, …", stated in the proposition itself.
- B.As a theorem, since its own proof is complete.
- C.As a conjecture as well.
- D.As a theorem, with the dependence explained in a footnote.
6.
Which of these sentences follow the lesson's guidelines? (Select all that apply.)
- A."Since $n > 2$ , we have $n^2 > 4$ ."
- B." $f$ is continuous, so it attains a maximum on $[0, 1]$ ."
- C."By the extreme value theorem, the continuous function $f$ attains a maximum on the closed bounded interval $[0, 1]$ ."
- D."Obviously $\forall \varepsilon > 0\ \exists N$ with $|a_n - L| < \varepsilon$ ."
- E."We argue by contradiction: suppose that $\sqrt 2 = a/b$ with $a, b$ positive integers having no common factor."
7.
The Lean file records Goldbach's conjecture as def GoldbachConjecture : Prop := ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n and separately proves goldbach_up_to_60. Why not write theorem goldbach : ∀ n : ℕ, 2 < n → … := sorry?
- A.A theorem … := sorry asserts the statement while admitting it is unproved; a def … : Prop merely names the statement, claiming nothing — exactly the difference between "Theorem" and "Conjecture".
- B.Because Lean cannot express statements about all natural numbers.
- C.Because goldbach_up_to_60 already proves the conjecture.
- D.Because sorry makes Lean reject the file.
8.
Model a text as a list of sentences, each a pair (defines, uses) of sets of symbol names. Write used_before_defined(sentences) returning a list of pairs (i, symbol) — in order of i, and alphabetical within a sentence — for each symbol used in sentence i that is not defined in an earlier sentence (or in sentence i itself).
Computational — Practice

Answer key — Mathematical writing

1.
A lemma. Theorem: a principal result. Proposition: a result of lesser importance. Lemma: auxiliary, used to prove others. Corollary: follows quickly from another result. Conjecture: stated but unproved. Remark: commentary.
2.
"If $x$ is a natural number and $x^2 = 4$ , then $x = 2$ ." For integers or reals the right statement is "then $x = 2$ or $x = -2$ ". The Lean file proves the natural-number version and refutes the integer version.
3.
The order is $\forall \varepsilon\, \exists \delta\, \forall x, y$ , so $\delta$ cannot depend on $x$ or $y$ : this is uniform continuity. Continuity is $\forall x\, \forall \varepsilon\, \exists \delta\, \forall y$ . For example $f(x) = x^2$ is continuous but not uniformly continuous on $\R$ .
4.
Step (3). Not being divisible by $p_1, \dots, p_k$ shows only that every prime factor of $N$ lies outside the list. Under the (false) assumption that the list is complete this is already a contradiction; as a standalone claim, " $N$ is prime" is false ( $30031 = 59 \cdot 509$ ). The clean statement is Theorem 1 of the lesson, which avoids contradiction altogether.
5.
What is proved is the implication "Conjecture 2 $\Rightarrow$ Proposition 4", so the proposition should say "Assuming Conjecture 2, …". Results conditional on the Riemann hypothesis are routinely written this way. The blueprint experiment detects such dependencies automatically, even indirect ones.
6.
(a), (c) and (e) are good. (b) starts with a symbol and hides which theorem is used; (d) uses "obviously" instead of a reason, uses logical symbols as prose, and omits "for all $n \ge N$ " — which changes the meaning entirely.
7.
A def … : Prop names a statement without asserting it. A theorem proved by sorry asserts it, flagged as unproved, and everything depending on it inherits the gap. With the definition, a result that needs Goldbach must take GoldbachConjecture as a hypothesis — a conditional theorem, written honestly, exactly as principle 10 recommends.
8.
```
def used_before_defined(sentences):
    problems = []
    defined = set()
    for i, (defines, uses) in enumerate(sentences):
        defined |= defines
        for symbol in sorted(uses - defined):
            problems.append((i, symbol))
    return problems
```
In the test text, sentence 2 uses $p$ , which is only defined in sentence 3 — a forward reference. Real texts are harder: symbols are defined implicitly ("let $p$ be a prime"), reused, and shadowed, which is why principle 1 asks the writer, not a program, to take responsibility.