I'm sorry if I've misinterpreted you, but:

1. In OpenAI's case, they dumped 1.8 GiB of Lean proofs on the world. I don't think they've done anything ethically wrong by doing that, but it's the exact opposite of "commit by commit". In fact, I'd say human mathematics has been much closer to "commit by commit", usually using smaller results as stepping stones.

2. You can have "commit by commit" without formal provers like Lean. Just keep your text in a Git repo.

My point is that if a proof is wrong or incompletely stated, we can just revise it and fix it. Commit by commit, build out a complete proof. This differs completely from the way that mathematicians have historically operated: check the work endlessly and privately email it to your friends until you’re sure it’s correct and then submit it to a journal.

It’s better to just publish something that you think is correct and if you find out it’s incorrect, try to fix it later.

My point is just that if a handful of these proofs are later revised or retracted, it’s really not a big deal.