A proof net is just a representation of a proof. It uses geometrical methods to eliminate irrelevant distractions in proofs that may convince you of their inequivalency. In particular it removes the order of rules applied, and syntax features. > They were introduced by [J.-Y. Girard](https://ncatlab.org/nlab/show/Jean-Yves+Girard) in 1987 in order to remove spurious notational redundancies introduced by sequential rule application or indeterminacy of [cut elimination](https://ncatlab.org/nlab/show/cut+elimination) and can be viewed as graphical normal forms of proofs freed from ‘the bureaucracy of syntax’ (Girard). [ncatlab](https://ncatlab.org/nlab/show/proof+net) For more info: https://ncatlab.org/nlab/show/proof+net