Let me share a story about research in mathematics.

With a fresh PhD in my hand I worked with my advisor, Dana Scott, on a question in domain theory. In case you don't know, Dana Scott invented domain theory. We were at the Mittag-Lefler Institute in Sweden. I was stuck and couldn't solve a rather technical problem.

I announced that I'd cook a dinner to anyone who could solve the problem. After a couple of days, Yuri Ershov, the Russian inventor of domain theory, came to me with a solution. It was a fine dinner with a very good bottle of wine.

Then I found a mistake in Ershov's argument. I fixed it and presented the results at a conference. When I returned home I found a mistake in my fix.

I worked on it more and fixed the fix. I presented the results at another conference, and apologized for the mistakes. Gordon Plotkin, a major domain theorist, walked up to me and explained that my fix of the fix was still flawed.

We corresponded a bit and he produced a fix of the fix of the fix of the original argument. I was pretty happy and stated writing it all up very carefully.

While doing so I found a mistake in the fix of the fix of the fix. But we did not give up! My advisor also chimed in. I was determined to get to the bottom of this thing.

After several meeting between us and a lot of very, very careful checking, we had a fix of the fix of the fix of the fix. It was published in https://doi.org/10.1016/j.tcs.2014.02.042

Is the paper correct? Who knows. This experience pushed me toward research in formalized mathematics.