LearnThisRepo lets you learn 300+ open source repos including Postgres, Langchain, VS Code, and more by chatting with them using AI! Learn more →
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 semiinteractive development of machinechecked proofs.


LearnThisRepo.com
Learn 300+ open source libraries for free using AI. LearnThisRepo lets you learn 300+ open source repos including Postgres, Langchain, VS Code, and more by chatting with them using AI!






WorkOS
The modern API for authentication & user identity. The APIs are flexible and easytouse, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.




MathInspector
A visual programing environment for scientific computing with python








learnxinyminutesdocs
Code documentation written as code! How novel and totally my idea!


InfluxDB
Power RealTime Data Analytics at Scale. Get realtime insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in realtime with unbounded cardinality.
mathlib reviews and mentions

Lean 4.0.0, first official lean4 release
Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.

If given a list of properties/definitions and relationship between them, could a machine come up with (mostly senseless, but) true implications?
Still, there are many useful tools based on these ideas, used by programmers and mathematicians alike. What you describe sounds rather like Datalog (e.g. Soufflé Datalog), where you supply some rules and an initial fact, and the system repeatedly expands out the set of facts until nothing new can be derived. (This has to be finite, if you want to get anywhere.) In Prolog (e.g. SWI Prolog) you also supply a set of rules and facts, but instead of a fact as your starting point, you give a query containing some unknown variables, and the system tries to find an assignment of the variables that proves the query. And finally there is a rich array of theorem provers and proof assistants such as Agda, Coq, Lean, and Twelf, which can all be used to help check your reasoning or explore new ideas.

Will Computers Redefine the Roots of Math?
For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprovercommunity/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it.

Which proof assistant is the best to formalize real analysis/probability/statistics?
At this point I would go with Lean because of mathlib. Mathlib's goal is to formalize modern mathematics, so many of the theorems you would need for analysis should already be there for you.

Is there a paid service where someone can explain a paper to me like I am 15?
It's been around since 2013, although there are LLM that interact with Lean to do automated theorem proving. Anyway, you can learn more about Lean here. I enjoyed their natural numbers game (which reminds, me I should finish the last two levels)

Lean – Theorem Prover
I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics.
 The Mathematical Hacker

Thoughts on proof assistants?
Check out Lean (https://leanprovercommunity.github.io/) if you want a theorem prover with a strong mathematics community. Or if you don't, Lean is cool.

Mathics: A free, opensource alternative to Mathematica
Check out https://github.com/leanprovercommunity/mathlib . Sure, it's not really a CAS but CAS algorithms could be added to it where applicable, since Lean is a constructive system and can thus express formally verified computations.

Principia Mathematica in modern notation.
If you're really interested in formalization of mathematics, there's a lot to do otherwise. I think there's lots of work to do on Mathlib that you don't need a PhD to do, just programming experience and bachelorslevel math knowledge.

A note from our sponsor  LearnThisRepo.com
learnthisrepo.com  22 Feb 2024
Stats
leanprovercommunity/mathlib is an open source project licensed under Apache License 2.0 which is an OSI approved license.
The primary programming language of mathlib is Lean.