Comment by 7373737373
21 hours ago
It may be useful to publish a formalization of ALL known mathematics at this point. Like every book ever printed, every paper on arXiv etc.
How many Gigabytes would that be, compressed? Wikipedia once fit on a DVD
This might also allow for some interesting meta-mathematics
This is what they are trying to do with Lean
More specifically, a combination of mathlib (human, expert curated) and projects like TauCeti (AI-welcome complement to mathlib). See: https://github.com/TauCetiProject/TauCeti
Oh? Where can i read more about that? It appears the sole focus so far was solving open problems
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 reply →