"zero-knowledge proof" is what happens when I manage to prove a statement in Lean by repeatedly applying standard tactics without having any actual understanding of the problem domain