Introduction - Bogdan

Stream: new members

[Bogdan]

Hi, I'm Bogdan. I come from a programming and ML background.
I've always been envious of the density and brevity of standard math notation, so I expected formal tools to act more like a semantic interface over that logic (for example, interactive demos like http://logitext.mit.edu/tutorial).
Instead, I found that the workflow in Lean relies heavily on writing tactic scripts in a text editor.
I'm trying to understand the cognitive workflow here: do you find that this text-based environment eventually becomes a place where you can reason and explore mathematical structures directly, or does most of the reasoning happen on paper, with Lean serving mainly as a tool for formalization and verification?