re: lean proofs and what it means to know things. I think the problem that is hard to make good analogies for is that the translation of problems into lean is non-trivial. For important questions it probably matters that a trustworthy person understands it
