Arithmetic geometry and elliptic curves

On $E: y^2 = x^3 + 1$ the point $P = (2, 3)$ has order $6$, and $2P = (0, 1)$. What is the order of the point $(0, 1)$?

Count the points of $E: y^2 = x^3 + 2$ over $\mathbb{F}_7$, including the point at infinity. (The non-zero squares mod $7$ are $1, 2, 4$.)

For $E: y^2 = x^3 + x + 1$ over $\mathbb{F}_5$ we found $\#E(\mathbb{F}_5) = 9$, so $a = 5 + 1 - 9 = -3$. Use $\#E(\mathbb{F}_{q^n}) = q^n + 1 - \alpha^n - \beta^n$, where $\alpha, \beta$ are the roots of $T^2 - aT + q$, to find $\#E(\mathbb{F}_{25})$.

Let $E: y^2 = x^3 + 1$, so $a = 0$, $b = 1$ and $4a^3 + 27b^2 = 27$. By the Nagell–Lutz theorem, a torsion point $(x, y) \neq O$ has integer coordinates with $y = 0$ or $y^2 \mid 27$. List every integer $y$ that is allowed.

In the proof of Hasse's theorem we showed $m^2 - a\,mn + q\,n^2 = \deg(m - n\phi) \ge 0$ for all integers $m, n$, and concluded $a^2 \le 4q$. Which justification of the last step is correct?

Let $E: y^2 = x^3 - 2$. For which fields $K$ is $E(K)$ not finitely generated? (Choose all that apply.)

The lesson's Lean theorem chord_third_point has hypotheses h₁ : y₁ ^ 2 = x₁ ^ 3 + a * x₁ + b, h₂ : y₂ ^ 2 = x₂ ^ 3 + a * x₂ + b, hx : x₁ ≠ x₂ and hℓ : y₂ - y₁ = ℓ * (x₂ - x₁). What would go wrong if we deleted hx?

Write count_points(p, a, b) returning $\#E(\mathbb{F}_p)$ for $y^2 = x^3 + ax + b$ over $\mathbb{F}_p$ ($p$ an odd prime), including the point at infinity. Then use it to check the Hasse bound for every curve over $\mathbb{F}_p$, $p \lt 50$.

Which of these statements about elliptic curves $E$ over $\Q$ are proved theorems (as of this lesson)? Choose all that apply.