> I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.

You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.

How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;

1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).

2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.

3) Clear definitions/assumptions/statements of the problem/theorem to be proved.

4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.

5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.

All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).

The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".

Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);

1) Did you prove it? - https://leanprover-community.github.io/did_you_prove_it.html

2) Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/

3) Is there a way to guarantee that Lean 4 proofs cannot be adversarially tricked? - https://proofassistants.stackexchange.com/questions/6517/is-...

What mathematicians should know about the Lean Theorem Prover: reliability & AI