Mathlib Alternatives
Similar projects and alternatives to mathlib
-
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
MathInspector
A visual programing environment for scientific computing with python
-
-
-
-
-
-
-
Scout APM
Scout APM: A developer's best friend. Try free for 14-days. Scout APM uses tracing logic that ties bottlenecks to source code so you know the exact line of code causing performance issues and can get back to building a great product faster.
-
Reviews and mentions
-
Why is simplicity so unreasonably effective at scientific explanation?
No, they really are - you've just internalized the vast majority of the content already. This is what a moderately careful (Lean makes some mildly questionable compromises regarding quotients) attempt at building up calculus from first principles looks like. And this is still assuming quite a bit of foundation. Human beings are much better at math than a bunch of apes barely down from the trees have any right to be - but that doesn't make math any smaller.
-
This is just an attempt I'm trying to get better at writing proofs I know I'm an idiot so please be constructive if you are criticizing
So I guess my thought is if you're going to practice writing proofs, start here: https://leanprover-community.github.io/
-
Tongue-in-cheek summaries of areas of mathematics
If you're into programming, Lambda calculus, and type theory, you might want to check out the LEAN project.
-
Galois Groups and the Symmetries of Polynomials
Hey this is really cool. I want to start doing the same thing.
Visual group theory is a really nice book for intuition. Also, the YouTube series "Essence of Group Theory" can help in this same line.
What I also want to do while self learning is formalizing some theorems and definitions in Lean. Even just looking at how they're already defined in mathlib [1] can be of great help when internalizing the concepts.
https://github.com/leanprover-community/mathlib/blob/292e3fa...
-
Is Haskell a good language for CAS/numerical analysis?
This is normal math, however this is not CAS territory but formal proof territory. Things like the intermediate value theorem are already formalized in Mathlib in using Lean v3.
-
Is there a program/website that can create and organize lists of mathematical theorems?
I'm not sure how useful this will be, since the question asks for a simple program, but maybe the LEAN theorem prover can be used to type in theorem statements. The theorems can be categorised by placing different theorems in different files (say one for algebra, another for analysis, and so on). Searching for specific theorems can be done by searching ("grepping", in Linux lingo) for the relevant text in the folder containing all the files.
-
Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
If you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/
Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ in the #new members stream.
Mathlib has plenty of contributions from interested undergrads :)
-
Learn coq or agda before diving into idris2?
Lean’s mathlib has quite nice formalization of category theory. For HoTT probably cubical Agda (though this link doesn’t cover cubical paths)
- ITS MOCHIZUKI TIME
-
Is there a book like Russell's Principia Mathematica but for modern day mathematics?
As such, if you want some body of work similar to PM, the spiritual successor of that effort is formal proof libraries, such as metamath or Lean. You won't find this stuff in any printed book, because the nature of software verified proofs is that they're supposed to be checked and verified digitally by computer.
-
Math Inspector: A Visual Programming Environment for Scientific Computing
I would be interested in something like this to visualize and inspect the structure of proofs, for example those contained in the Lean mathematical components library https://github.com/leanprover-community/mathlib
Stats
leanprover-community/mathlib is an open source project licensed under Apache License 2.0 which is an OSI approved license.
Popular Comparisons
Are you hiring? Post a new remote job listing for free.