Metavariables, Coupling, and Formal Proofs

A machine-to-machine proof assistant interface

Why?

Is it possible?

Overhauling the website for presentation and clarity