Accessible open textbooks in math-heavy disciplines

I think the neatest feature would be: the mathematician states the theorem in English (edit: with math symbols as needed), then he states the proof in English.

A post-Processor transform the proof into lean (with any official lib loaded). It is automatically verified. If something is missing, the post processor ask to write in English the missing parts. Iterate like this.

The lean proof is hidden in the final document, and can be displayed if needed. Or even, we get an English version that can be easily retransformed into lean at will.

Bonus point: we can query the document to give more details on part of the proof and it outputs (expanded) lean formatted as nice English.

Note: there is no need to have all the math self contained in the document, he can say to assume some theorem true to do his proof. And this would be reflected in English.

I can’t speak for true mathematicians, but as a (mostly theoretical) physicist I would hate to write my maths in plain English. Notation is used precisely because it’s easier, more efficient (to write and to read) to use it instead of prose. If you’d like an example, I suggest reading texts on solving quadratic equations that predate modern algebraic notation.