A small experiment: take a formal Metamath proof and animate the meaning—step by step—so a human brain can follow it without losing rigor.
A2I is an implication theorem. The animation shows ax-mp “binding” concrete lines of the proof into the schema (φ, ψ, (φ→ψ), ⇒ψ), then collapsing the scaffolding until only the conclusion remains.