Yeah, and a very big difference between Lean and projects such as the LHC or the James Web telescope are that the LHS and the James Web are massive taxpayer-fun

Yeah, and a very big difference between Lean and projects such as the LHC or the James Web telescope are that the LHS and the James Web are massive taxpayer-funded projects, so there is an expectation that their significance is clearly explained to those taxpayers (and scientists want continued funding, so it pays to be clear). Lean started as a small research project hidden away within Microsoft Research, and mathematicians learned about it and have built a community by word of mouth. There is no accountability needed at all for the project, and there's no need to advertise it -- that's not to say that there hasn't been any effort put into advertising it to mathematicians. I just advertised the system myself an hour ago during a talk that explained Lean and Mathlib to a group of mathematicians, computer scientists, and linguists.