@antoinechambertloir I'm not sure I understand the issue in 1): the conjectures listed in this database are all drawn from public sources, and are already part of the scientific commons. I see no reason why a private company should not be allowed to access this common resource, or to use that resource to build databases in a fashion that is non-exclusionary to other parties (in particular, the existence of this database does not prohibit other researchers from working with these conjectures without using the database).
2) Actually in recent years the fraction of mathematics that can be formalized in Lean's Mathlib has expanded significantly. Just to give one example, the notion of a perfectoid space was formalized back in 2019: https://leanprover-community.github.io/lean-perfectoid-spaces/ . While formalizing the _proofs_ of the core theory of mathematics is still far from reality, the goal of formalizing the majority of the _statements_ of key concepts and conjectures seems quite feasible to me within a few years (particularly with AI assistance).
In general, I would view these developments in positive-sum terms rather than zero-sum terms. If a contribution to mathematics is positive across all subfields, but has a stronger positive contribution in one subfield than in another, I would still view this as a net positive for mathematics, especially given that in time the subfields which could not immediately utilize the contribution can eventually figure out how to do so after interacting with those subfields that could initially benefit from it.