[Lean] Default proof should report a warning and be treated like `sorry` when it fails

[abentkamp]

Ideally, we would add a CLI command that runs lake build and translates the warning messages into warnings with references to the precise place in the Rust code.