What does HackerNews think of mathlib?

Lean mathematical components library

Language: Lean

Lean 4.0 | Sep 2023
Expand Context ↕
Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.

https://github.com/leanprover-community/mathlib
It's not mathematics that you need to contribute to (2010) | Jul 2023
Expand Context ↕
https://github.com/leanprover-community/mathlib

https://1lab.dev/

You can watch the next generation, or participate, right now.
Will Computers Redefine the Roots of Math? | Jun 2023
Expand Context ↕
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.

I'm curious, which field of math do you work in?

Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...
Did studying proof based math topics e.g. analysis make you a better programmer? | Jun 2023
Expand Context ↕
Lean mathlib was originally a type checker proof assistant, but now leanprover-community is implementing like all math as proofs in Lean in the mathlib project.

Lean (proof assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)

"Lean mathlib overview": https://leanprover-community.github.io/mathlib-overview.html

"Where to start learning Lean": https://github.com/leanprover-community/mathlib/wiki/Where-t...

leanprover-community/mathlib: https://github.com/leanprover-community/mathlib
Functional Programming in Lean | May 2023
Expand Context ↕
Is this what you're looking for?

https://github.com/leanprover-community/mathlib
Lean – Theorem Prover | Jan 2023
Expand Context ↕
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.

[0] https://github.com/leanprover-community/mathlib
The Mathematical Hacker (2012) | Dec 2022
Expand Context ↕
Take a look at the Natural Number Game! [1] It does exactly that: "Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax"."

After you get the hang of the system, you can play with the interactive theorem prover behind it: Lean [2]. There's also plenty other interactive theorem provers (Coq, Isabelle, HOL, Mizar, Metamath, ...) but Lean has a lot of traction amongst mathematicians at the moment.

There are no limits to the math you an do with this. There is mathlib [3], the main mathematical library. It covers a lot of undergraduate material [4], and plenty of stuff beyond that [5]. The community has even covered some state of the art research math in Lean [6a, 6b].

You are very welcome to hang out on the leanprover zulip [7]] and ask questions about the Natural Number Game or anything else that is Lean-related.

[1]: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... [2]: https://leanprover-community.github.io/ [3]: https://github.com/leanprover-community/mathlib [4]: https://leanprover-community.github.io/undergrad.html [5]: https://leanprover-community.github.io/mathlib-overview.html [6a]: https://github.com/leanprover-community/lean-liquid [6b]: https://www.nature.com/articles/d41586-021-01627-2 [7]: https://leanprover.zulipchat.com/