You can certainly build up a collection of probably-true-statements. That makes sense. Encoding them as logical formula makes sense. That's basically what you are describing. But OP wanted to then additionally put those formula into Lean, and that's where I disagree. Because he will likely have inconsistent statements in his collection and then he can prove all sorts of absurdities (principle of explosion).
So IIUC like if an article is covering a debate, 3 sources assert "A", and another 3 assert "~A", then the heuristic "3 sources assert means it's true", gives you a logical setup with "A ^ ~A"?
If so, then yes that's a bug in that heuristic. Like I said in my first comment, what OP is describing is impossible the way they're describing it. So I think in that sense we're in agreement.
But on the other hand, maybe OP will end up hacking together a thing that resembles probabilistic modal logic.
At the time I wrote that comment OP was being downvoted and there were no encouraging responses, which I felt wasn't representative of the math community as I know it. Now there is a good discussion of the problem space and some suggestions to check out different kinds of logic, so I'm glad to see all that going on!