The person suggesting it had simple heuristics like "this proposition was asserted by three sources". This has obvious flaws (e.g. I can cite three lying sources). But even on Wikipedia, there is no automatic checking that sources say what's claimed. So it wouldn't be useless despite having obvious flaws.

But anyway, if you have heuristics like this you can make them propositions and do inference with them. Instead of thinking of it as "I've proved this false" or "the citations are correct" perhaps think of it more like a lint that runs against your code base and tells you whether you've done something that falls below expectations.

A more natural way to model it would be something like a Bayesian system where you assign probabilities, build up a hierarchical model, and flow probabilities through the model. But there's something nice about a simpler system that doesn't pretend to do more than it can.

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).