@lean-samaritan.bsky.social That’s pretty good… basically Knuth’s literate style programming, but for proofs, which I think is the right mix. I still think we need better syntax for the actual proof parts though. A “goal” is to make standard writing almost the same as the formal statements.