My intuition tells me that if we manage to entirely formalize correct reasoning, the result will have a sort of adversarial quality: you can "prove" statements, but these proofs can be overturned by stronger disproofs.

That... doesn't sound right at all. It does sound like how people intuitively think about proof/reasoning (even people smart enough to be thinking about things like, say, set theory, trying to overturn Cantor's diagonal argument with a counterexample without actually discovering a flaw in the theorem), and how we think about debates (the guy on the left half of the screen says something, the guy on the right says the opposite, and they go back and forth taking turns making Valid Points until the CNN anchor says "We'll have to leave it there" and the viewers are left agreeing with (1) whoever agreed with their existing beliefs, or, if neither, (2) whoever spoke last). But even if our current formal understanding of reasoning is incomplete, we know it's not going to resemble that. Yes, Bayesian updating will cause your probability estimates to fluctuate up and down a bit as you acquire more evidence, but the pieces of evidence aren't fighting each other, they're collaborating on determining what your map should look like and how confident you should be.

Of course, for this to work . . . no AGI could be so much smarter than the others that it could find tons of evidence in favor of its pet truths and have the database favor them despite that they're false.

Why would we build AGI to have "pet truths", to engage in rationalization rather than rationality, in the first place?