数学の証明を書くとき，長くなってくると全体像が掴みにくくなります．
そこで，プログラミングにおけるコードの書き方を参考にして，わかりやすい証明の書き方を考えてみます．
提案
予告コメント
数学の証明において，「○○を示したい」と先にこれから示す内容を予告したいことがあります．
予告の内容は論証とは関係がありませんので，プログラムでいうコメントアウトに相当するものと言えるでしょう．
そこで，コメントアウトに似せて予告を書きます．例を挙げると，こんな感じです．
// $A$ を示したい
なんやかんやで
$A$ であることがわかった
実際に予告された内容を示している箇所をインデントにより示します．
文字色は forestgreen にしています．シンタックスハイライトでコメントは緑色であることが多いからです．
含意 $\Rightarrow$ の導入
数学では $A \Rightarrow B$ を証明するのに，$A$ を仮定して $B$ を示すということをやります．
$A$ を仮定すれば $B$ が示せるということと，$A \Rightarrow B$ が成り立つということは証明論的には微妙に異なることであり，前者から後者を導いてよいという規則のことを $\Rightarrow$ の導入規則と言います．
$A$ を仮定して $B$ を示している時点では，$B$ は $A$ に依存していますが，結論 $A \Rightarrow B$ はもはや仮定 $A$ に依存していません．
そこでインデントによって仮定 $A$ に依存している範囲を明示することにします．
Assume $A$ と仮定する
なんやかんやで
$B$ であることがわかる
したがって $A \Rightarrow B$ が結論できる
なお文字色は royalblue にしています．特に意味はありません．緑や黒でさえなければ他の色でも構わないのですが，私は青色にするといい感じだと思っています．
場合分け
場合分けについてはプログラミング言語によくある if 文を流用すればよいでしょう．
if $A$ であるとき then
$C$ である
else
$C$ である
したがって $C$ が成り立つ
疑似コードに合わせて then も書きましたが，実際には then は要らないかもしれません．
背理法
背理法も Assume を使えば表現できますが，証明を読んでいる人間としては, $A \Rightarrow B$ の証明と背理法は区別したいところです．
これは一つの案ですが，インデントを Contradiction で閉じるというのはどうでしょうか？
コメントで何を示したいか書いておくとより丁寧ですが，インデントが深くなってしまうのが気になりますね．
// $A$ を示したい
Assume $A$ でないと仮定する
なんやかんやで矛盾
Contradiction
したがって $A$ である
全称 $\forall$ の導入規則
数学で $\forall x \quad P(x)$ を示すとき，「任意に $x$ が与えられたとする」と仮定して，$P(x)$ を示します．
含意 $\Rightarrow$ の導入と似ていますが，この２つは区別したいですね．
全称導入は $A \subseteq B$ を示すときや，解析学において $ε$-$δ$ 論法で何かを示そうとしているときに頻出し，$A \Rightarrow B$ とは少し毛色が異なる感じがするからです．
そこで Given という構文を用意します．
Given $x$ が与えられたとする．
なんやかんやで
$P(x)$ である
したがって $\forall x \quad P(x)$ が成り立つ
あとがき
証明の中で，問題の仮定をどこで使っているかは読者がとても気にするところです
それを明示するにはどういうルールにするといいか考えているのですが，納得のいくルールが思いつきません．わざわざ構文的に実現する必要がそもそもないのかもしれません．
また，証明の中での参照をどうするかも悩んでいます．式番号を振ればいい気がしますが，構文として実現したい気もしています．
あとは帰納法の扱いですね．背理法がかければ一応同値なことはできますが，背理法専用の書き方を用意しておきたいところです．
ところで正直，こういうことは私が最初に考えたわけではないと思います．
他の案があったら聞いてみたいです．
