> The inductive invariant IC3PO produced for Paxos in under an hour identically matches the human-written one previously derived with significant manual effort using a technique called interactive theorem proving. On top of speeding the process up, it also produces a proof with very succinct and digestible documentation.

Is there anything actually different between "interactive theorem proving" in a sufficiently advanced language (say Coq) and what they've done here? Honest question, I had to drop out of my college Coq class on account of a broken leg (and lack of willpower).