Real-World Problems as Contexts for Proof