TY  - RPRT
TI  - Lean4Lean: Verifying a Typechecker for Lean, in Lean
AU  - Mario Carneiro
PY  - 2025
UR  - https://arxiv.org/abs/2403.14064
ID  - 2403.14064
ER  -