Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently)
[1] http://mizar.org/
[2] https://isarmathlib.org/
[3] http://ceur-ws.org/Vol-2634/FMM4.pdf
But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.
Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently) [1] http://mizar.org/ [2] https://isarmathlib.org/ [3] http://ceur-ws.org/Vol-2634/FMM4.pdf