Comment by david-gpu

I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address.

He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do.

I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.