Hacker GitHub

← All repos

leanprover-community/mathlib3

View on GitHub ↗ ★ 1,667 Lean archived

Lean 3's obsolete mathematical components library: please use mathlib4

19 mentions on Hacker News by 15 people: 0 stories, 19 comments · first 2019-09-30 · latest 2023-12-09

Mentions per year 19 mentions · busiest year 2023 (8)
20082026
AllStoriesComments NewestTopOldest
  1. …: AlphaZero self-play , LLMs and Lean, "Q: LLM and/or an RL agent trained on mathlib and tests" https://github.com/leanprover-community/mathlib/issues/17919... -> Proof Assistance SE: https://proofassistants.stackexchange.com/ Perhaps to…
    comment by westurner · 2023-12-09 · in 'A-team' of math proves a critical link between addition and sets
  2. …"Q: LLM and/or an RL agent trained on [Lean mathlib] and tests" https://github.com/leanprover-community/mathlib/issues/17919
    comment by westurner · 2023-12-04 · in An easy-sounding problem yields numbers too big for our universe
  3. …and its documentation makes for a big corpus to learn by example from. Not ideal but it helps. https://github.com/leanprover-community/mathlib
    comment by brohee · 2023-09-08 · in Lean 4.0
  4. https://github.com/leanprover-community/mathlib https://1lab.dev/ You can watch the next generation, or participate, right now.
    comment by Ericson2314 · 2023-07-18 · in It's not mathematics that you need to contribute to (2010)
  5. 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.…
    comment by giraj · 2023-06-30 · in Will Computers Redefine the Roots of Math?
  6. …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
    comment by westurner · 2023-06-24 · in Ask HN: Did studying proof based math topics make you a better programmer?
  7. Is this what you're looking for? https://github.com/leanprover-community/mathlib
    comment by arlort · 2023-05-29 · in Functional Programming in Lean
  8. …proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics. [0] https://github.com/leanprover-community/mathlib
    comment by agentultra · 2023-01-20 · in Lean – Theorem Prover
  9. ….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]:…
    comment by deadbeef57 · 2022-12-24 · in The Mathematical Hacker (2012)
  10. 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.
    comment by zozbot234 · 2022-11-05 · in Mathics: A free, open-source alternative to Mathematica
  11. …would be the Lean community group and the Math lib project: https://arxiv.org/pdf/1910.09336.pdf https://github.com/leanprover-community/mathlib
    comment by mbrodersen · 2022-04-20 · in There’s more to mathematics than rigour and proofs (2007)
  12. …for symbolic expression trees without human-readable comments or symbol names? Lean mathlib: https://github.com/leanprover-community/mathlib , and then reasoning about concurrent / distributed systems (with side channels in actual physical…
    comment by westurner · 2021-09-11 · in Interpretable Model-Based Hierarchical RL Using Inductive Logic Programming
  13. …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...
    comment by zant · 2021-08-04 · in Galois Groups and the Symmetries of Polynomials
  14. …even sheaves and toposes. [0] https://leanprover.github.io/programming_in_lean/#01_Introdu... [1] https://github.com/leanprover-community/mathlib/blob/master/...
    comment by hiker · 2021-06-26 · in Functors and Monads for People Who Have Read Too Many “Tutorials”
  15. …the structure of proofs, for example those contained in the Lean mathematical components library https://github.com/leanprover-community/mathlib
    comment by fspeech · 2021-02-01 · in Math Inspector: A Visual Programming Environment for Scientific Computing
  16. …illustration: [1] introduces these instances to the file and [2] implicitly uses the instance. [1] https://github.com/leanprover-community/mathlib/blob/master/... [2] https://github.com/leanprover-community/mathlib/blob/master/...
    comment by kmill · 2020-11-21 · in Why is dependent type theory more suitable than set theory for proof assistants?
  17. …formalization, so it might be interesting adding a quandle instance for your operation. [1] https://github.com/leanprover-community/mathlib/blob/master/...
    comment by kmill · 2020-10-05 · in Lambda Calculus Diagrams (2015)
  18. …I think the most promising is maybe Lean these days (Coq still might take too long to learn): https://github.com/leanprover-community/mathlib
    comment by smt1 · 2020-07-08 · in SymPy - a Python library for symbolic mathematics
  19. …nature. which due to performance concerns usually aren't written in languages running in VMs. [0] https://github.com/leanprover-community/mathlib [1] https://github.com/leanprover-community/mathlib/blob/master/...
    comment by dpah · 2019-09-30 · in Theorem Proving in Lean [pdf]