Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively.

Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"

Some simple tutorials;

Introduction to Lean for Programmers: The syntax and semantics of mathematics - https://towardsdatascience.com/introduction-to-lean-for-prog...

The hitchhiker's guide to reading Lean 4 theorems - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...