More specifically, a combination of mathlib (human, expert curated) and projects like TauCeti (AI-welcome complement to mathlib). See: https://github.com/TauCetiProject/TauCeti
replyOh? Where can i read more about that? It appears the sole focus so far was solving open problems
replyI believe that is the goal of MathLib, to transcribe all math into a big Lean library.
replyMathlib is expert reviewed, but only contains a tiny fraction of all mathematics. So this seems to be a quantity of work a "10,000 agents" approach would be applicable to. Like Navier-Stokes, something to spend a couple million in compute on :)
reply