Readings shared September 25, 2024. jaalonso.github.io/vestigium/post… #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming

The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. github.com/eric-wieser/le… #ITP #LeanProver #Lean4 #Mathlib #Math

Cambridge combinatorics in Lean (Formalisation of the Cambridge combinatorics courses). ~ Yaël Dillies. yaeldillies.github.io/LeanCamCombi/ #ITP #LeanProver #Lean4 #Math

M2Lyon2425: Sets and functions (1). ~ Filippo A. E. Nuccio. github.com/faenuccio-teac… #ITP #LeanProver #Lean4 #Math

Readings shared September 23, 2024. jaalonso.github.io/vestigium/post… #ITP #LeanProver #Coq #IsabelleHOL #Math #ITP #Haskell #FunctionalProgramming #AI #LLMs

Lean Tutorial in Vienna. ~ Pietro Monticone et als. github.com/pitmonticone/L… #ITP #LeanProver #Math

Tips and tricks for beginners using Mathlib/Lean. ~ Moritz Firsching. docs.google.com/presentation/d… #ITP #LeanProver

Introduction to Lean. ~ Markus Himmel. raw.githubusercontent.com/pitmonticone/L… #ITP #LeanProver #Math

Scientific computing in Lean. ~ Tomáš Skřivan. slides.com/lecopivo/scien… #ITP #LeanProver #Math

Readings shared September 22, 2024. jaalonso.github.io/vestigium/post… #ITP #LeanProver #Lean3 #Lean4 #Logic #Math

A tutorial introduction of dependently-typed programming (and the Lean4 theorem prover). ~ Frédéric Peschanski. gitlab.com/fredokun/agreg… #ITP #LeanProver #Lean4 #Math

Formalisation of mathematics and dependent-type programming (A tutorial introduction using the Lean4 theorem prover). ~ Frédéric Peschanski. gitlab.com/fredokun/tmc-s… #ITP #LeanProver #Lean4 #Math

A Lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms. ~ Mattchen. github.com/cymcymcymcym/U… #ITP #LeanProver #LEan4 #Math

Formalization of Riemann-Stieltjes integral in Lean4. ~ Marc Masdeu (Marc) et als. github.com/mmasdeu/stielt… #ITP #LeanProver #Lean4 #Math

Source of the "The Topology Game". ~ Marc Masdeu et als. github.com/mmasdeu/topolo… #ITP #LeanProver #Lean3 #Math

The Topology Game (Learn topology with Lean!). ~ Barcelona Lean Seminar. mmasdeu.github.io/topologygame/ #ITP #LeanProver #Math

Lean proofs of (some) problems from the book "102 combinatorial problems". ~ Musab Guma'a et als. github.com/mgsium/102_com… #ITP #LeanProver #Lean4 #Math

"A concise introduction to mathematical logic" in Lean4. ~ Enrico Borba. github.com/enricozb/logic #ITP #LeanProver #Lean4 #Logic #Math

Lean-Intro-Topology: Introduction to topology with Lean. ~ Rafael Grenier. github.com/rafaelgrenier/… #ITP #LeanProver #Lean4 #Math

Using Lean theorem prover to teach formal mathematics: Lean-Intro-Topology library. ~ Rafael Grenier. raw.githubusercontent.com/rafaelgrenier/… #ITP #LeanProver #Lean4 #Math