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.