I can only hope that the hard github dependency can be chalked up to just "this was the easiest way to get this out the door". Its not a good solution in the lo

I can only hope that the hard github dependency can be chalked up to just "this was the easiest way to get this out the door". Its not a good solution in the long term, (single point of failure, github is increasingly unreliable and disliked, what about people already on a different forge or repository source) but it does solve at least a few problems that would otherwise be thorny (minimum bar for submission, outsourcing identity and spam management to github, etc.) And since the bar for validation is expressly stated to be rather weak, I guess this would be best conceptualized as a specialized search engine that can weed out the <80th percentile of mediocre formalized proofs, with a target audience of professional mathematicians who have the ability to make determinations on the final 20% themselves. Maybe also something I'd wanna skim over at some point, as a non-mathmatician who just thinks lean is neat. Its not useful to me but its fun to learn about.