You might find The Hitchhiker's guide to reading Lean 4 Theorems useful - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...

Excerpt:

The Rosetta Stone

Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.

A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."