← Back to context Comment by mattmar96 1 day ago I believe that is the goal of MathLib, to transcribe all math into a big Lean library.https://lean-lang.org/use-cases/mathlib/ 1 comment mattmar96 Reply 7373737373 1 day ago Mathlib 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 :)
7373737373 1 day ago Mathlib 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 :)
Mathlib 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 :)