Lean 4.0.0, first official lean4 release

• mathlib4

  10 458 10.0 Lean

  The math library of Lean 4

  

  Is Lean a Category?

  (like much debated: is Hask(ell) a Category)

  "In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework."

  So it seems to be proven that there is a Category Lean!

  https://github.com/leanprover-community/mathlib4/blob/master...

• lean4

  23 3,191 9.5 Lean

  Lean 4 programming language and theorem prover

  

• Onboard AI

  getonboard.dev

  sponsored

  Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.

  

• logical_verification_2023

  1 30 10.0 Lean

  Hitchhiker's Guide to Logical Verification (2023 Edition)

  Me too, I want to follow

  https://github.com/blanchette/logical_verification_2023

  The hitchhiker's guide

• mathlib

  14 1,617 9.7 Lean

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

  

  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

• learnxinyminutes-docs

  48 10,865 0.0 JavaScript

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

• lean4-mode

  2 44 10.0 Emacs Lisp

  Emacs major mode for Lean 4

  

• topos

  1 42 10.0 Lean

  Topos theory in lean (by b-mehta)

  Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)

• InfluxDB

  www.influxdata.com

  sponsored

  Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.

  

Suggest a related project