alt Hacker NewsYou can structure your proofs in Lean to reason forward, but proofs in Mathlib still primarily do backward proof, because it is more compact and performant.
Replies
derdi • 08/01/2025
Maybe you could show a simple example so the OP can get an idea if that is what they are looking for.
➕ show 1 reply
Declarative proof languages support backward proof, typically phrased as: "suffices <statement> by ... " i.e. it suffices to show <statement>, and the current goal follows.