mathlib
principia
Our great sponsors
mathlib | principia | |
---|---|---|
36 | 10 | |
1,619 | 197 | |
0.2% | - | |
9.3 | 2.7 | |
4 days ago | 8 months ago | |
Lean | TeX | |
Apache License 2.0 | GNU General Public License v3.0 only |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
mathlib
-
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/leanprover-community/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://leanprover-community.github.io/) if you want a theorem prover with a strong mathematics community. Or if you don't, Lean is cool.
-
Mathics: A free, open-source alternative to Mathematica
Check out https://github.com/leanprover-community/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 bachelors-level math knowledge.
principia
-
Principia Mathematica in modern notation.
Not exactly modern notation, but Coq notation, which could easily be machine-translated into modern notation: https://www.principiarewrite.com/
You can check it out here: https://www.principiarewrite.com/
-
Ask HN: Would prog. language look like if that was designed by no-programmer
Principia
A work from the early 20th century, mathematics, logic.
I think some expert called Bertrand Russell's and A.N. Whitehead's "Principia Mathematica" initiative a "bizarre" piece of work, when seen from the perspective of a programming language designer.
I can't make a qualified statement about this, as I am neither a mathematician nor a language designer. And I cannot find the exact quote on the internet, sorry. Just saying.
In code? See for yourself :
-
Hacker News top posts: Dec 6, 2021
Whitehead and Russell’s Principia rewritten in Coq\ (44 comments)
What are some alternatives?
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.
Coq-Equations - A function definition package for Coq
mathquill - Easily type math in your webapp
polynomial-algebra - polynomial-algebra Haskell library
lean-liquid - 💧 Liquid Tensor Experiment
fricas - Official repository of the FriCAS computer algebra system
natural_number_game - Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
hott3 - HoTT in Lean 3
CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
symmetric-polynomials - Symmetric polynomials in Haskell
Coq-HoTT - A Coq library for Homotopy Type Theory