127 of 127 declarations
∎
Select a declaration
Every theorem shows its informal proof from the paper, with the exact Lean proof one click away — and clickable dependencies between them.
Well-founded induction, formalized twice: on paper and in Lean 4
127 of 127 declarations