Can Paperproof render proof terms?

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 applys and intros, 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.