Incremental or "wholesale" development?

Stream: general

[Victor Porton]

I am verifying a theorem (my Navier-Stokes proof).

For proofs I almost entirely rely on AI.

Is it a good idea to ignore errors for now and later, when I already write much, tell AI to fix errors? Or is it better to add one theorem at a time and tell AI to fix the entered theorem proof errors before starting to write the next theorem?

[Michael Rothgang]

If you want a working proof in the end, making sure what you're building does not error seems sensible. (It is possible to get stuck in an unprovable state otherwise, because a previous statement you had was actually slightly wrong. Proving it will protect against this.)