*Short answer - no, but it can be done, and we welcome PRs that would enable proof term rendering in Paperproof.*

There are two ways in which a Lean proof can be written - a proof term (without the `by`

keyword) and a sequence of tactics (with the `by`

keyword).

Many theorems in Mathlib are written as proof terms. When you try to check them in Paperproof, you get a *"Not within theorem"* notification.

At the moment, **Paperproof** cannot render proof term proofs - **Paperproof** only renders parts of the proof that start with `by`

, meaning some theorems from Mathlib, like the one above, are not even detected as theorems by **Paperproof**.

Any such theorem can be rewritten into a sequence of fake `apply`

s and `intro`

s, so that it looks something like this:

```
theorem norm_image_sub_le_of_norm_deriv_le {C : ℝ} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ x ∈ s, ‖deriv f x‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s)
: ‖f y - f x‖ ≤ C * ‖y - x‖ := by
apply hs.norm_image_sub_le_of_norm_hasDerivWithin_le
intros x hx
let smth := hf x hx
apply DifferentiableAt.hasDerivAt at smth
apply HasDerivAt.hasDerivWithinAt (f' := deriv f x) at smth
exact smth
exact bound
exact xs
exact ys
```

Which then can be rendered as follows:

Which immediately makes the theorem much more readable.