[zozbot234]

Structured proofs as advocated for by Leslie Lamport are more reminiscent of natural deduction. One obvious difference with sequent calculus is that natural deduction only admits of a single goal for each proof step (though with multiple antecedents or conditions), whereas sequent calculus generalizes this to multiple goals which are understood disjunctively i.e. "at least one" has to be true. (The latter works well with the inherent duality of some types of logic, such as ordinary classical logic or linear logic. It doesn't seem to come up all that much when doing math practically, especially in areas close to CS where "direct" proofs are generally preferred.)