Semi-formal proofs

Stream: general

[Martin Dvořák]

What do you think about writing mathematical proofs semi-formally such as my following document?
https://raw.githubusercontent.com/madvorak/duality/main/nonLean/Proof_finFarkasBartl_simplified.pdf
Would you be happy to read an entire book written in this style (assuming there is a public repo that contains full formal proofs) potentially in the future?

[Antoine Chambert-Loir]

I don't see the point. It's not so useful for the formal text which you can't copy-paste, not for the vernacular one which is cluttered with a lot of symbols.

[Antoine Chambert-Loir]

However, if a software could allow to navigate at the same time in a formal/vernacular text, and that will arise, it could become interesting. I see your trial as a first step towards this goal.

[Yury G. Kudryashov]

I would prefer the future where people explain the ideas in English omitting details if they stay in the way + supply formal proofs in (commented) Lean, not the future where people submit proofs that mix English with Lean.

[Aaron Anderson]

Personally, I find it very difficult to read code embedded in paragraph-format text - its only advantage over full sentences in legibility is the ability to poke around and interact with something like the Infoview.

[Aaron Anderson]

If you find that this style works for you to express your ideas, then I would really encourage you to format the full-line code in something that pops out more visually, at the least a theorem-style environment, ideally something with an outline and color-coding, so that eyes like mine could more easily separate it from the text.

[Xiyu Zhai]

I believe Mathematics typically studies things that can be very neatly stated in terms of nature languages and formula. So just English with possibly Lean as annotations will be good enough.

[Martin Dvořák]

I'm surprised by how many Lean users find $math$ more readable than Lean.

[Philippe Duchon]

My guess is that the vast majority of Lean users (or at least, Mathlib users) have been speaking math for way longer than they have been speaking Lean. So, in a sense, it's closer to a natural language.

(Plus, some have been trying to learn Coq as well as Lean. And personally, I'm still very bad at making the difference between British English and American English.)

[Edward van de Meent]

i think continually interjecting the lean code between definitions might make it a bit more difficult to read... i think i'd prefer to have the informal and formal parts grouped, be it per page or per chapter or something like that. i think that just like switching or translating languages, switching continually between reading lean and reading "conventional" maths can take up some valueable processing power.

[Somo S.]

I think this would be really cool if it was an interactive book rather than a static html or pdf.. The interactivity would allow for simplifying various assumptions for experimentation and exploring one's understanding ... or digging deeper into a proof details that in typical style of pen-paper proof writing, would be skipped or hand woven over (since there is an assumption your audience already knows what is missing). I look forward to a future where lean, is just "standard issue" in learning and exposing mathematics