There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine):
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
[1] https://ceur-ws.org/Vol-448/paper10.pdf
[2] https://isarmathlib.org/UniformSpace_ZF_1.html
[3] https://mathoverflow.net/questions/513742/are-we-stuck-with-...