← Back to context Comment by 7373737373 21 hours ago Oh? Where can i read more about that? It appears the sole focus so far was solving open problems 2 comments 7373737373 Reply mattmar96 21 hours 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/ 7373737373 20 hours 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 :)
mattmar96 21 hours 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/ 7373737373 20 hours 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 20 hours 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 :)
I believe that is the goal of MathLib, to transcribe all math into a big Lean library.
https://lean-lang.org/use-cases/mathlib/
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 :)