ただ、実際の数学の教科書の証明を見ていると「○○の定理より〜」みたいな感じで、既存の定理を推論規則として使っている場面が良くあって、定理をただコピーするだけじゃなくて、推論規則として使えるようにするみたいな仕組みもあった方が便利そうなのだけど、定理が推論規則になるっていう状況があまりきちんと定義されていないような気がする

証明を static な木として記述させるとして、証明済みの定理をどうやって適用させるかがなかなか悩ましい。一番単純にいくなら、証明済みの定理をそのままコピーすることのみを許可する方法かな・・・

NORQAIN って全然ピンとくる時計がない。その割に OMEGA ぐらいの値付けがされてて、全然理解が出来ない

Many books try to capture a proof as a sequence of inferences on statements. It looks natural at first because it is similar to how we make arguments in natural languages, but it is not natural as it looks.

If you try to formalize a proof in that way, the proof internally have to have a lot of backward references to indicate what inference uses what statements. This backward reference structure instantly becomes hugely convoluted, and it makes the proof cluttered and unreadable.

A proof should be considered as a static tree, instead of a series of dynamic operations on statements.